proposition: Lemma FirstIncompletenessA : SysPrf T G -> Inconsistent LNT T.
proof: Proof. unfold G; intro H. destruct (FixPointLNT (notH (LNN2LNT_formula codeSysPf)) 0) as [x [H1 H2]]. intro f; apply contradiction with x. - assumption. - apply impE with (notH (substF (notH (LNN2LNT_formula codeSysPf)) 0 (natToTerm (codeFormula x)))). + apply cp2; apply iffE1; apply sysExtend with PA. * assumption. * apply H1. + rewrite (subFormulaNot LNT); apply nnI. change (substF (LNN2LNT_formula codeSysPf) 0 (natToTerm (codeFormula x))) with (box x). apply HBL1; assumption. 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)