proposition: Theorem PAIncomplete : exists f : Formula, (Sentence f) /\ ~(SysPrf PA f \/ SysPrf PA (notH f)).
proof: Proof. assert (H: Expressible NN 1 codePA (substF (primRecFormula 1 (proj1_sig codePAIsPR)) 0 (natToTermLNN 1))). { apply (Representable2Expressible _ closedNN1). simpl. apply nn1. apply primRecRepresentable. } destruct H as [H H0]; simpl in H0. assert (H1: exists f : Formula, (forall v : nat, ~ In v (freeVarF f)) /\ (SysPrf PA f \/ SysPrf PA (notH f) -> Inconsistent LNT PA)). { eapply Rosser'sIncompleteness with (repT := LNN2LNT_formula (substF (primRecFormula 1 (proj1_sig codePAIsPR)) 0 (natToTermLNN 1))) (v0 := 1). - unfold Included; auto. - intros v H1; assert (H2: v <= 1 /\ v <> 0). { apply H. apply LNN2LNT_freeVarF1. apply H1. } destruct v as [| n]. + induction H2 as [H2 H3]. now elim H3. + destruct n. * reflexivity. * lia. - intros f H1; rewrite <- LNN2LNT_natToTerm. eapply impE. + apply iffE1. apply LNN2LNT_subFormula. + apply NN2PA. assert (H2: if codePA (codeFormula f) then LNN.SysPrf NN (substF (substF (primRecFormula 1 (proj1_sig codePAIsPR)) 0 (Succ Zero)) 1 (LNN.natToTerm (codeFormula f))) else LNN.SysPrf NN (notH (substF (substF (primRecFormula 1 (proj1_sig codePAIsPR)) 0 (Succ Zero)) 1 (LNN.natToTerm (codeFormula f))))) by apply H0. clear H0. assert (H0: codePA (codeFormula f) = true) by now apply codePAcorrect3. now rewrite H0 in H2. - intros f H1; rewrite <- LNN2LNT_natToTerm. eapply impE with (LNN2LNT_formula (notH (substF (substF (primRecFormula 1 (proj1_sig codePAIsPR)) 0 (Succ Zero)) 1 (LNN.natToTerm (codeFormula f))))). + simpl; apply cp2. apply iffE2. apply LNN2LNT_subFormula. + apply NN2PA. assert (H2: if codePA (codeFormula f) then LNN.SysPrf NN (substF (substF (primRecFormula 1 (proj1_sig codePAIsPR)) 0 (Succ Zero)) 1 (LNN.natToTerm (codeFormula f))) else LNN.SysPrf NN (notH (substF (substF (primRecFormula 1 (proj1_sig codePAIsPR)) 0 (Succ Zero)) 1 (LNN.natToTerm (codeFormula f))))). * apply H0. * clear H0. assert (H0: codePA (codeFormula f) = false) by now apply codePAcorrect2. now rewrite H0 in H2. - apply PAdec. } clear H H0; decompose record H1 /dr; intros x H0 H2; exists x; split. - assumption. - intro H; unfold Inconsistent in H2. induction PAconsistent. auto. Qed.
imports: Coq(Ensembles) Coq(List) Coq(Arith Lia) hydras.Ackermann(folProp) hydras.Ackermann(folProof) hydras.Ackermann(folReplace) hydras.Ackermann(folLogic3) hydras.Ackermann(subProp) hydras.Ackermann(ListExt) hydras.Ackermann(NNtheory) hydras.Ackermann(NN2PA) Goedel(fixPoint) Goedel(codeSysPrf) hydras.Ackermann(PAtheory) hydras.Ackermann(code) Goedel(PRrepresentable) hydras.Ackermann(expressible) hydras.Ackermann(checkPrf) hydras.Ackermann(codeNatToTerm) hydras(Compat815) hydras.Ackermann(codePA) hydras.Ackermann(PAconsistent)