proposition: Theorem SecondIncompletness : SysPrf T Con -> Inconsistent LNT T.
proof: Proof. intros H; apply FirstIncompletenessA. apply impE with Con; auto. apply cp1; apply impTrans with (box G). - apply cp1; apply impTrans with G. + apply iffE2; apply GS. + apply impI; apply nnI; apply Axm. right; constructor. - unfold Con; apply impI; apply nnI. apply impE with (box (box G)). + apply impE with (box (impH (box G) F)). * apply sysWeaken; apply HBL3. * apply impE with (box G). -- apply impE with (box (impH G (impH (box G) F))). ++ apply sysWeaken; apply HBL3. ++ apply sysWeaken; apply HBL1. apply impTrans with (notH (box G)). ** apply iffE1; apply GS. ** apply impI; apply impI. apply contradiction with (box G). { apply Axm; right; constructor. } { apply Axm; left; right; constructor. } -- apply Axm; right; constructor. + apply impE with (box G). * apply sysWeaken; apply HBL2. * apply Axm; right; constructor. Qed.
imports: Coq(Ensembles) Coq(List) Coq(Arith) hydras.Ackermann(folProp) hydras.Ackermann(folProof) hydras.Ackermann(folReplace) hydras.Ackermann(folLogic3) hydras.Ackermann(subProp) hydras.Ackermann(ListExt) Goedel(fixPoint) hydras.Ackermann(NN2PA) Goedel(codeSysPrf) hydras.Ackermann(PAtheory) hydras.Ackermann(code) hydras.Ackermann(checkPrf) hydras.Ackermann(codeNatToTerm) Goedel(rosserPA)