proposition: Theorem Rosser'sIncompleteness : (forall x : Formula, mem _ T x \/ ~ mem _ T x) -> exists f : Formula, (forall v : nat, ~ In v (freeVarF f)) /\ (SysPrf T f \/ SysPrf T (notH f) -> Inconsistent LNN T).
proof: Proof. intros decide. set (A := forallH 1 (impH codeSysPrf (existH 2 (andH (LT (var 2) (var 1)) (substF codeSysPrfNot 1 (var 2)))))). destruct (FixPointLNN A 0) as [x [H0 H1]]. exists x; split. - intros v H; induction (H1 v) as [H2 H3]. assert (H4: In v (List.remove eq_nat_dec 0 (freeVarF A))) by apply H2, H. unfold A in H4; SimplFreeVar. + assert (H4: v <= 1). { apply (freeVarCodeSysPrf LNN LcodeLNN codeArityLNTF codeArityLNNR codeArityLNTFIsPR codeArityLNNRIsPR repT v0 freeVarRepT). apply H5. } lia. + assert (H4: v <= 1) by (apply freeVarCodeSysPrfN; assumption); lia. - intros [H| H]. + unfold Inconsistent in |- *. intro f; elim H; intros x0 [x1 H2]. induction (searchProof decide _ (notH x) _ x1) as [H3 | H3]. * decompose record H3 /r; intros x2 x3 H4 H6. apply contradiction with x. -- assumption. -- now exists x2, x3. * apply contradiction with (existH 2 (andH (LT (var 2) (natToTerm (codePrf _ _ x1))) (substF (substF codeSysPrfNot 0 (natToTerm (codeFormula x))) 1 (var 2)))). -- apply impE with (existH 2 (andH (LT (var 2) (natToTerm (codePrf x0 x x1))) (substF (substF (substF codeSysPrfNot 0 (natToTerm (codeFormula x))) 1 (var 2)) 1 (natToTerm (codePrf _ _ x1))))). ++ apply iffE1; apply sysExtend with NN. ** apply extendsNN. ** apply (reduceExist LNN). --- apply closedNN. --- apply (reduceAnd LNN). +++ apply iffRefl. +++ apply (subFormulaNil LNN). intro H4; induction (freeVarSubFormula3 _ _ _ _ _ H4). *** now apply (in_remove_neq _ _ _ _ _ H5). *** simpl in H5; decompose sum H5; discriminate H6. ++ replace (LT (var 2) (natToTerm (codePrf _ _ x1))) with (substF (LT (var 2) (var 1)) 1 (natToTerm (codePrf _ _ x1))). ** rewrite <- (subFormulaAnd LNN). apply impE with (existH 2 (substF (andH (LT (var 2) (var 1)) (substF (substF codeSysPrfNot 1 (var 2)) 0 (natToTerm (codeFormula x)))) 1 (natToTerm (codePrf x0 x x1)))). --- apply iffE1; apply sysExtend with NN. +++ apply extendsNN. +++ apply (reduceExist LNN). *** apply closedNN. *** apply (reduceSub LNN). apply closedNN. apply (reduceAnd LNN). apply iffRefl. apply (subFormulaExch LNN). discriminate. intros H4; simpl in H4. decompose sum H4. discriminate H5. apply closedNatToTerm. --- replace (LT (var 2) (var 1)) with (substF (LT (var 2) (var 1)) 0 (natToTerm (codeFormula x))). rewrite <- (subFormulaAnd LNN). +++ replace (existH 2 (substF (substF (andH (LT (var 2) (var 1)) (substF codeSysPrfNot 1 (var 2))) 0 (natToTerm (codeFormula x))) 1 (natToTerm (codePrf x0 x x1)))) with (substF (existH 2 (substF (andH (LT (var 2) (var 1)) (substF codeSysPrfNot 1 (var 2))) 0 (natToTerm (codeFormula x)))) 1 (natToTerm (codePrf x0 x x1))). *** replace (existH 2 (substF (andH (LT (var 2) (var 1)) (substF codeSysPrfNot 1 (var 2))) 0 (natToTerm (codeFormula x)))) with (substF (existH 2 (andH (LT (var 2) (var 1)) (substF codeSysPrfNot 1 (var 2)))) 0 (natToTerm (codeFormula x))). apply impE with (substF (substF codeSysPrf 0 (natToTerm (codeFormula x))) 1 (natToTerm (codePrf _ _ x1))). repeat rewrite <- (subFormulaImp LNN). apply forallE. replace (forallH 1 (substF (impH codeSysPrf (existH 2 (andH (LT (var 2) (var 1)) (substF codeSysPrfNot 1 (var 2))))) 0 (natToTerm (codeFormula x)))) with (substF (forallH 1 (impH codeSysPrf (existH 2 (andH (LT (var 2) (var 1)) (substF codeSysPrfNot 1 (var 2)))))) 0 (natToTerm (codeFormula x))). apply impE with x. apply iffE1. apply sysExtend with NN. apply extendsNN. apply H0. assumption. rewrite (subFormulaForall LNN). induction (eq_nat_dec 1 0) as [a | b]. ---- discriminate a. ---- induction (In_dec eq_nat_dec 1 (freeVarT (natToTerm (codeFormula x)))) as [a | b0]. ++++ elim (closedNatToTerm _ _ a). ++++ reflexivity. ---- now apply codeSysPrfCorrect1. ---- rewrite (subFormulaExist LNN). induction (eq_nat_dec 2 0) as [a | b]. discriminate a. induction (In_dec eq_nat_dec 2 (freeVarT (natToTerm (codeFormula x)))). elim (closedNatToTerm _ _ a). reflexivity. *** rewrite (subFormulaExist LNN). induction (eq_nat_dec 2 1) as [a | b]. discriminate a. induction (In_dec eq_nat_dec 2 (freeVarT (natToTerm (codePrf x0 x x1)))) as [a | b0]. elim (closedNatToTerm _ _ a). reflexivity. +++ unfold LT; rewrite (subFormulaRelation LNN); now simpl. ** unfold LT; rewrite (subFormulaRelation LNN); now simpl. -- apply nExist. set (E := nat_rec (fun _ => Formula) (equal Zero Zero) (fun (n : nat) (rec : Formula) => andH (notH (substF (substF codeSysPrfNot 0 (natToTerm (codeFormula x))) 1 (natToTerm n))) rec) (codePrf x0 x x1)). assert (H4: forall x : nat, ~ In x (freeVarF E)). { unfold E; clear H3 E; induction (codePrf x0 x x1) as [ | n IHn]. - simpl; auto. - intros x2; unfold nat_rec, nat_rect; intro H3. set (Q := (fix F (n : nat) : (fun _ : nat => Formula) n := match n with | O => equal Zero Zero | S n0 => (fun (n1 : nat) (rec : Formula) => andH (notH (substF (substF codeSysPrfNot 0 (natToTerm (codeFormula x))) 1 (natToTerm n1))) rec) n0 (F n0) end) n). SimplFreeVar. + apply (Nat.le_ngt x2 1). apply freeVarCodeSysPrfN. * assumption. * lia. + apply (IHn x2 H3). } apply impE with E. ++ apply sysExtend with NN. apply extendsNN. apply impI. apply forallI. ** intros [x2 [H5 H6]]. induction H6 as [x2 H6| x2 H6]. --- apply (closedNN 2); exists x2; auto. --- induction H6; now apply (H4 2). ** apply nAnd; unfold orH; apply impTrans with (LT (var 2) (natToTerm (codePrf x0 x x1))). --- apply impI, nnE. apply Axm; right; constructor. --- apply impI; apply impE with E. +++ apply impE with (LT (var 2) (natToTerm (codePrf x0 x x1))). do 2 apply sysWeaken. *** apply boundedLT. intros n H5; rewrite (subFormulaImp LNN). rewrite (subFormulaNot LNN). apply impE with (impH E (notH (substF (substF codeSysPrfNot 0 (natToTerm (codeFormula x))) 1 (natToTerm n)))). apply iffE2. apply (reduceImp LNN). apply (subFormulaNil LNN). apply H4. apply (reduceNot LNN). apply (subFormulaTrans LNN). intros H6; SimplFreeVar. apply (Nat.le_ngt 2 1). apply freeVarCodeSysPrfN. assumption. apply Nat.lt_succ_diag_r. unfold E in |- *. clear E H4 H3. apply impI. induction (codePrf x0 x x1). elim (Nat.nlt_0_r _ H5). unfold nat_rec, nat_rect; set (Q := (fix F (n1 : nat) : (fun _ : nat => Formula) n1 := match n1 with | O => equal Zero Zero | S n2 => (fun (n3 : nat) (rec : Formula) => andH (notH (substF (substF codeSysPrfNot 0 (natToTerm (codeFormula x))) 1 (natToTerm n3))) rec) n2 (F n2) end) n0). induction (Compat815.le_lt_or_eq _ _ (Compat815.lt_n_Sm_le _ _ H5)). apply impE with Q. apply sysWeaken. apply impI. apply (IHn0 H3). eapply andE2. apply Axm; right; constructor. rewrite H3. eapply andE1. apply Axm; right; constructor. *** apply Axm; right; constructor. +++ apply Axm; left; right; constructor. ++ unfold E in |- *; clear H4 E. induction (codePrf x0 x x1) as [ | n IHn]. ** simpl; apply eqRefl. ** simpl; apply andI. induction (eq_nat_dec (checkPrf LNN LcodeLNN codeArityLNTF codeArityLNNR (codeFormula (notH x)) n) 0) as [a | b]. --- unfold codeSysPrfNot. apply codeSysPrfNCorrect3. intros A0 p H4; rewrite H4 in a. rewrite (checkPrfCorrect1 LNN LcodeLNN codeArityLNTF codeArityLNNR codeArityLNTFIsCorrect1 codeArityLNNRIsCorrect1) in a; discriminate a. --- decompose record (checkPrfCorrect2 LNN LcodeLNN codeArityLNTF codeArityLNNR codeArityLNTFIsCorrect1 codeArityLNTFIsCorrect2 codeArityLNNRIsCorrect1 codeArityLNNRIsCorrect2 _ _ b) /r; intros x2 H5 x3 x4 H6. rewrite <- H6. assert (H4: x2 = notH x). { eapply codeFormulaInj. - assumption. } cut (code.codePrf x3 x2 x4 = n). +++ generalize x4; clear H6 x4; rewrite H4. intros x4 H6; apply codeSysPrfNCorrect2. eapply H3. apply Nat.lt_lt_succ_r. rewrite <- H6. apply Nat.lt_succ_diag_r. +++ assumption. --- apply IHn; intros B q H4. eapply H3. apply Nat.lt_lt_succ_r. apply H4. + unfold Inconsistent; intros f. elim H; intros x0 [x1 H2]. induction (searchProof decide _ x _ x1) as [H3 | H3]. * decompose record H3 /r; intros x2 x3 H4 H6. apply contradiction with x. -- exists x2, x3; assumption. -- assumption. * apply contradiction with (substF A 0 (natToTermLNN (code.codeFormula x))). -- unfold A; rewrite (subFormulaForall LNN). induction (eq_nat_dec 1 0) as [a | b]. ++ discriminate a. ++ induction (In_dec eq_nat_dec 1 (freeVarT (natToTermLNN (code.codeFormula x)))) as [a | b0]. ** elim (closedNatToTerm _ _ a). ** clear b0 b. set (E := nat_rec (fun _ => Formula) (equal Zero Zero) (fun (n : nat) (rec : Formula) => andH (notH (substF (substF codeSysPrf 0 (natToTerm (codeFormula x))) 1 (natToTerm n))) rec) (S (codePrf _ _ x1))). assert (H4: forall x : nat, ~ In x (freeVarF E)). { unfold E; clear H3 E. induction (S (codePrf x0 (notH x) x1)). - simpl; auto. - intros x2; unfold nat_rec, nat_rect; intros H3. SimplFreeVar. + apply (Compat815.le_not_lt x2 1). * apply (freeVarCodeSysPrf LNN LcodeLNN codeArityLNTF codeArityLNNR codeArityLNTFIsPR codeArityLNNRIsPR repT v0 freeVarRepT). apply H4. * destruct x2 as [| n0]. -- elim H6; reflexivity. -- destruct n0. ++ elim H5; reflexivity. ++ apply Compat815.lt_n_S. apply Nat.lt_0_succ. + apply (IHn _ H3). } apply impE with E. --- set (G := substF (substF codeSysPrfNot 0 (natToTerm (codeFormula x))) 1 (natToTerm (codePrf x0 (notH x) x1))). apply impE with G. +++ apply sysExtend with NN. *** assumption. *** repeat apply impI; apply forallI. unfold not in |- *; intros [x2 [H5 H6]]. induction H6 as [x2 H6| x2 H6]. induction H6 as [x2 H6| x2 H6]. apply (closedNN 1). exists x2. auto. induction H6. unfold G in H5. SimplFreeVar. induction H6. apply (H4 _ H5). rewrite (subFormulaImp LNN). rewrite (subFormulaExist LNN). induction (eq_nat_dec 2 0) as [a | b]. discriminate a. induction (In_dec eq_nat_dec 2 (freeVarT (natToTermLNN (code.codeFormula x)))). elim (closedNatToTerm _ _ a). clear b0 b. rewrite (subFormulaAnd LNN). replace (substF (LT (var 2) (var 1)) 0 (natToTermLNN (code.codeFormula x))) with (LT (var 2) (var 1)). apply orE with (orH (LT (var 1) (natToTerm (codePrf x0 (notH x) x1))) (equal (var 1) (natToTerm (codePrf x0 (notH x) x1)))) (LT (natToTerm (codePrf x0 (notH x) x1)) (var 1)). repeat simple apply sysWeaken. apply impE with (orH (LT (var 1) (natToTerm (codePrf x0 (notH x) x1))) (orH (equal (var 1) (natToTerm (codePrf x0 (notH x) x1))) (LT (natToTerm (codePrf x0 (notH x) x1)) (var 1)))). apply impI. apply orSys. apply orI1. apply orI1. apply Axm; right; constructor. apply orSys. apply orI1. apply orI2. apply Axm; right; constructor. apply orI2. apply Axm; right; constructor. apply nn9. apply impI. apply impE with G. apply impE with E. apply impE with (LT (var 1) (natToTerm (S (codePrf x0 (notH x) x1)))). repeat simple apply sysWeaken. apply boundedLT. intros n H5; repeat apply impE. repeat rewrite (subFormulaImp LNN). repeat apply impI. fold codeFormula. apply contradiction with (substF (substF codeSysPrf 0 (natToTermLNN (codeFormula x))) 1 (natToTerm n)). apply Axm; right; constructor. apply sysWeaken. apply impE with E. repeat simple apply sysWeaken. apply impI. clear H3 H4. induction (S (codePrf x0 (notH x) x1)). elim (Nat.nlt_0_r _ H5). induction (Compat815.le_lt_or_eq _ _ (Compat815.lt_n_Sm_le _ _ H5)). unfold E; apply impE with (nat_rec (fun _ : nat => Formula) (equal Zero Zero) (fun (n : nat) (rec : Formula) => andH (notH (substF (substF codeSysPrf 0 (natToTerm (codeFormula x))) 1 (natToTerm n))) rec) n0). apply sysWeaken. repeat apply impI. apply IHn0. assumption. simpl; eapply andE2. apply Axm; right; constructor. unfold E; simpl; rewrite H3. eapply andE1. apply Axm; right; constructor. apply impE with (substF E 1 (natToTerm n)). apply iffE1. apply (subFormulaNil LNN). apply H4. apply Axm; left; right; constructor. apply impE with (orH (LT (var 1) (natToTerm (codePrf x0 (notH x) x1))) (equal (var 1) (natToTerm (codePrf x0 (notH x) x1)))). repeat simple apply sysWeaken. simpl; apply nnPlusNotNeeded. apply Axm; right; constructor. apply Axm; left; right; constructor. apply Axm; do 2 left; right; constructor. repeat apply impI. apply sysWeaken. apply existI with (natToTerm (codePrf x0 (notH x) x1)). rewrite (subFormulaAnd LNN). apply andI. unfold LT in |- *. rewrite (subFormulaRelation LNN). simpl in |- *. apply Axm; right; constructor. apply sysWeaken. apply sysWeaken. apply impE with (substF (substF codeSysPrfNot 0 (natToTerm (codeFormula x))) 1 (natToTerm (codePrf x0 (notH x) x1))). apply sysWeaken. apply iffE2. fold codeFormula; apply iffTrans with (substF (substF (substF codeSysPrfNot 0 (natToTermLNN (codeFormula x))) 1 (var 2)) 2 (natToTerm (codePrf x0 (notH x) x1))). repeat (apply (reduceSub LNN); [ apply closedNN | idtac ]). apply (subFormulaExch LNN). discriminate. unfold not in |- *; intros; SimplFreeVar. discriminate H6. apply closedNatToTerm. apply (subFormulaTrans LNN). intros H5; SimplFreeVar. apply (Compat815.le_not_lt 2 1). apply freeVarCodeSysPrfN. assumption. apply Nat.lt_succ_diag_r. apply Axm; right; constructor. unfold LT; rewrite (subFormulaRelation LNN). reflexivity. +++ unfold G; now apply codeSysPrfNCorrect1. --- clear H4; unfold E; clear E. induction (S (codePrf x0 (notH x) x1)) as [| n IHn]. +++ simpl; apply eqRefl. +++ simpl; apply andI. induction (eq_nat_dec (checkPrf _ LcodeLNN codeArityLNTF codeArityLNNR (codeFormula x) n) 0) as [a | b]. *** unfold codeSysPrf, codeFormula; apply codeSysPrfCorrect3. intros A0 p H4; rewrite H4 in a. rewrite (checkPrfCorrect1 LNN LcodeLNN codeArityLNTF codeArityLNNR codeArityLNTFIsCorrect1 codeArityLNNRIsCorrect1) in a. discriminate a. *** decompose record (checkPrfCorrect2 LNN LcodeLNN codeArityLNTF codeArityLNNR codeArityLNTFIsCorrect1 codeArityLNTFIsCorrect2 codeArityLNNRIsCorrect1 codeArityLNNRIsCorrect2 _ _ b) /r; intros x2 H5 x3 x4 H6. rewrite <- H6. assert (H4: x2 = x). { eapply (codeFormulaInj LNN). assumption. } rewrite <- H4. apply codeSysPrfCorrect2. rewrite <- H4 in H3. apply H3 with x4. rewrite <- H6. apply Nat.lt_succ_diag_r. *** apply IHn. intros B q H4; eapply H3. apply Nat.lt_lt_succ_r. apply H4. -- apply impE with (notH x). +++ apply cp2. apply iffE2. apply sysExtend with NN. *** apply extendsNN. *** assumption. +++ assumption. 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) Goedel(fixPoint) Goedel(codeSysPrf) hydras.Ackermann(NNtheory) hydras.Ackermann(code) Goedel(PRrepresentable) hydras.Ackermann(expressible) hydras.Ackermann(checkPrf) hydras.Ackermann(codeNatToTerm) hydras(Compat815)