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 LNT 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 (FixPointLNT (LNN2LNT_formula 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 (LNN2LNT_formula A)))) by (apply H2; assumption). cut (In v (List.remove eq_nat_dec 0 (freeVarF A))). + clear H4. intros H4; unfold A in H4; SimplFreeVar. assert (H4: v <= 1). { apply (freeVarCodeSysPrf LNT LcodeLNT codeArityLNTF codeArityLNTR codeArityLNTFIsPR codeArityLNTRIsPR (LNT2LNN_formula repT) v0 freeVarRepT'). apply H5. } * lia. * assert (H4: v <= 1) by now apply freeVarCodeSysPrfN. lia. + eapply in_in_remove. * eapply in_remove_neq, H4. * apply LNN2LNT_freeVarF1. eapply in_remove, H4. - intros [H| H]; unfold Inconsistent. + intros f; elim H. intros x0 H2; induction H2 as [x1 H2]. induction (searchProof decide _ (notH x) _ x1). * decompose record H3 /r; intros x2 x3 H4 H6. apply contradiction with x. -- assumption. -- exists x2, x3; assumption. * apply contradiction with (existH 2 (andH (LNN2LNT_formula (LT (var 2) (natToTermLNN (codePrf _ _ x1)))) (substF (substF (LNN2LNT_formula codeSysPrfNot) 0 (natToTerm (codeFormula x))) 1 (var 2)))). -- apply impE with (existH 2 (andH (LNN2LNT_formula (LT (var 2) (natToTermLNN (codePrf x0 x x1)))) (substF (substF (substF (LNN2LNT_formula codeSysPrfNot) 0 (natToTerm (codeFormula x))) 1 (var 2)) 1 (natToTerm (codePrf _ _ x1))))). ++ apply iffE1. apply sysExtend with PA. ** apply extendsPA. ** apply (reduceExist LNT). --- apply closedPA. --- apply (reduceAnd LNT). +++ apply iffRefl. +++ apply (subFormulaNil LNT). intros H4; induction (freeVarSubFormula3 _ _ _ _ _ H4). *** now apply (in_remove_neq _ _ _ _ _ H5). *** simpl in H5; decompose sum H5. discriminate H6. ++ replace (LT (var 2) (natToTermLNN (codePrf _ _ x1))) with (substF (LT (var 2) (var 1)) 1 (natToTermLNN (codePrf _ _ x1))). ** apply impE with (existH 2 (andH (substF (LNN2LNT_formula (LT (var 2) (var 1))) 1 (natToTerm (codePrf x0 x x1))) (substF (substF (substF (LNN2LNT_formula codeSysPrfNot) 0 (natToTerm (codeFormula x))) 1 (var 2)) 1 (natToTerm (codePrf x0 x x1))))). --- apply iffE1. apply sysExtend with PA. +++ apply extendsPA. +++ apply (reduceExist LNT). *** apply closedPA. *** apply (reduceAnd LNT). apply iffSym. rewrite <- LNN2LNT_natToTerm. apply LNN2LNT_subFormula. apply iffRefl. --- rewrite <- (subFormulaAnd LNT). apply impE with (existH 2 (substF (andH (LNN2LNT_formula (LT (var 2) (var 1))) (substF (substF (LNN2LNT_formula codeSysPrfNot) 1 (var 2)) 0 (natToTerm (codeFormula x)))) 1 (natToTerm (codePrf x0 x x1)))). +++ apply iffE1. apply sysExtend with PA. *** apply extendsPA. *** apply (reduceExist LNT). apply closedPA. apply (reduceSub LNT). apply closedPA. apply (reduceAnd LNT). apply iffRefl. apply (subFormulaExch LNT). 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 (natToTermLNN (codeFormula x))). *** apply impE with (existH 2 (substF (andH (substF (LNN2LNT_formula (LT (var 2) (var 1))) 0 (natToTerm (codeFormula x))) (substF (LNN2LNT_formula (substF codeSysPrfNot 1 (var 2))) 0 (natToTerm (codeFormula x)))) 1 (natToTerm (codePrf x0 x x1)))). apply iffE1. apply sysExtend with PA. apply extendsPA. apply (reduceExist LNT). apply closedPA. apply (reduceSub LNT). apply closedPA. apply (reduceAnd LNT). apply iffSym. rewrite <- LNN2LNT_natToTerm. apply LNN2LNT_subFormula. apply (reduceSub LNT). apply closedPA. replace (var 2) with (LNN2LNT_term (var 2)). apply LNN2LNT_subFormula. reflexivity. rewrite <- (subFormulaAnd LNT). replace (existH 2 (substF (substF (andH (LNN2LNT_formula (LT (var 2) (var 1))) (LNN2LNT_formula (substF codeSysPrfNot 1 (var 2)))) 0 (natToTerm (codeFormula x))) 1 (natToTerm (codePrf x0 x x1)))) with (substF (existH 2 (substF (andH (LNN2LNT_formula (LT (var 2) (var 1))) (LNN2LNT_formula (substF codeSysPrfNot 1 (var 2)))) 0 (natToTerm (codeFormula x)))) 1 (natToTerm (codePrf x0 x x1))). replace (existH 2 (substF (andH (LNN2LNT_formula (LT (var 2) (var 1))) (LNN2LNT_formula (substF codeSysPrfNot 1 (var 2)))) 0 (natToTerm (codeFormula x)))) with (substF (existH 2 (andH (LNN2LNT_formula (LT (var 2) (var 1))) (LNN2LNT_formula (substF codeSysPrfNot 1 (var 2))))) 0 (natToTerm (codeFormula x))). apply impE with (substF (substF (LNN2LNT_formula codeSysPrf) 0 (natToTerm (codeFormula x))) 1 (natToTerm (codePrf _ _ x1))). repeat rewrite <- (subFormulaImp LNT). apply forallE. replace (forallH 1 (substF (impH (LNN2LNT_formula codeSysPrf) (existH 2 (andH (LNN2LNT_formula (LT (var 2) (var 1))) (LNN2LNT_formula (substF codeSysPrfNot 1 (var 2)))))) 0 (natToTerm (codeFormula x)))) with (substF (forallH 1 (impH (LNN2LNT_formula codeSysPrf) (existH 2 (andH (LNN2LNT_formula (LT (var 2) (var 1))) (LNN2LNT_formula (substF codeSysPrfNot 1 (var 2))))))) 0 (natToTerm (codeFormula x))). apply impE with x. apply iffE1. apply sysExtend with PA. apply extendsPA. apply H0. assumption. rewrite (subFormulaForall LNT). 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. ---- apply impE with (LNN2LNT_formula (substF (substF codeSysPrf 0 (natToTermLNN (codeFormula x))) 1 (natToTermLNN (codePrf x0 x x1)))). ++++ apply iffE1. apply sysExtend with PA. apply extendsPA. eapply iffTrans. **** apply LNN2LNT_subFormula. **** repeat rewrite <- LNN2LNT_natToTerm. apply (reduceSub LNT). apply closedPA. apply LNN2LNT_subFormula. ++++ apply T'prf2Tprf. apply codeSysPrfCorrect1. assumption. ---- rewrite (subFormulaExist LNT). 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 LNT). induction (eq_nat_dec 2 1). 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). simpl; reflexivity. ** unfold LT; rewrite (subFormulaRelation LNN). simpl; reflexivity. -- apply nExist. set (E := LNN2LNT_formula (nat_rec (fun _ => fol.Formula LNN) (LNT2LNN_formula (equal LNT.Zero LNT.Zero)) (fun (n : nat) rec => andH (notH (substF (substF codeSysPrfNot 0 (natToTermLNN (codeFormula x))) 1 (natToTermLNN 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). - simpl; auto. - intros x2; unfold nat_rec, nat_rect; intro H3. set (Q := (fix F (n : nat) : (fun _ : nat => fol.Formula LNN) n := match n with | O => LNT2LNN_formula (equal LNT.Zero LNT.Zero) | S n0 => (fun (n1 : nat) (rec : fol.Formula LNN) => andH (notH (substF (substF codeSysPrfNot 0 (natToTermLNN (codeFormula x))) 1 (natToTermLNN n1))) rec) n0 (F n0) end) n). assert (H4: In x2 (freeVarF (andH (notH (substF (substF codeSysPrfNot 0 (natToTermLNN (codeFormula x))) 1 (natToTermLNN n))) Q))) by now apply LNN2LNT_freeVarF1. clear H3; SimplFreeVar. ++ apply (Compat815.le_not_lt x2 1). ** apply freeVarCodeSysPrfN. assumption. ** lia. ++ rewrite <- LNT2LNN_natToTerm in H4. rewrite LNT2LNN_freeVarT in H4. apply (closedNatToTerm _ _ H4). ++ rewrite <- LNT2LNN_natToTerm in H4. rewrite LNT2LNN_freeVarT in H4. apply (closedNatToTerm _ _ H4). ++ apply (IHn x2). now apply LNN2LNT_freeVarF2. } apply impE with E. ** apply sysExtend with PA. --- apply extendsPA. --- apply impI. apply forallI. +++ intros [x2 [H5 H6]]; induction H6 as [x2 H6| x2 H6]. *** apply (closedPA 2). exists x2; auto. *** induction H6. apply (H4 2); assumption. +++ apply nAnd; unfold orH; apply impTrans with (LNN2LNT_formula (LT (var 2) (natToTermLNN (codePrf x0 x x1)))). *** apply impI, nnE; apply Axm; right; constructor. *** apply impI; apply impE with E. ---- apply impE with (LNN2LNT_formula (LT (var 2) (natToTermLNN (codePrf x0 x x1)))). do 2 apply sysWeaken. apply PAboundedLT. intros n H5; rewrite (subFormulaImp LNT). rewrite (subFormulaNot LNT). apply impE with (impH E (notH (substF (substF (LNN2LNT_formula codeSysPrfNot) 0 (natToTerm (codeFormula x))) 1 (natToTerm n)))). apply iffE2. apply (reduceImp LNT). apply (subFormulaNil LNT). apply H4. apply (reduceNot LNT). apply (subFormulaTrans LNT). intros H6; SimplFreeVar. apply (Compat815.le_not_lt 2 1). apply freeVarCodeSysPrfN. apply LNN2LNT_freeVarF1. apply H7. apply Nat.lt_succ_diag_r. unfold E; 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 => fol.Formula LNN) n1 := match n1 with | O => LNT2LNN_formula (equal LNT.Zero LNT.Zero) | S n2 => (fun (n3 : nat) (rec : fol.Formula LNN) => andH (notH (substF (substF codeSysPrfNot 0 (natToTermLNN (codeFormula x))) 1 (natToTermLNN n3))) rec) n2 (F n2) end) n0). induction (Compat815.le_lt_or_eq _ _ (Compat815.lt_n_Sm_le _ _ H5)). apply impE with (LNN2LNT_formula Q). apply sysWeaken. apply impI. apply (IHn0 H3). rewrite LNN2LNT_and. eapply andE2. apply Axm; right; constructor. rewrite H3. apply impE with (LNN2LNT_formula (notH (substF (substF codeSysPrfNot 0 (natToTermLNN (codeFormula x))) 1 (natToTermLNN n0)))). apply sysWeaken. apply iffE1. apply iffTrans with (notH (LNN2LNT_formula (substF (substF codeSysPrfNot 0 (natToTermLNN (codeFormula x))) 1 (natToTermLNN n0)))). apply iffRefl. apply (reduceNot LNT). rewrite <- LNN2LNT_natToTerm. rewrite <- LNN2LNT_natToTerm. apply iffTrans with (substF (LNN2LNT_formula (substF codeSysPrfNot 0 (natToTermLNN (codeFormula x)))) 1 (LNN2LNT_term (natToTermLNN n0))). apply LNN2LNT_subFormula. apply (reduceSub LNT). apply closedPA. apply LNN2LNT_subFormula. eapply andE1. rewrite LNN2LNT_and. apply Axm; right; constructor. apply Axm; right; constructor. ---- apply Axm; left; right; constructor. ** unfold E; clear H4 E; induction (codePrf x0 x x1). --- simpl; apply eqRefl. --- unfold nat_rec, nat_rect; rewrite LNN2LNT_and. apply andI. +++ induction (eq_nat_dec (checkPrf LNT LcodeLNT codeArityLNTF codeArityLNTR (codeFormula (notH x)) n) 0) as [a | b]. *** unfold codeSysPrfNot; apply T'prf2Tprf. apply codeSysPrfNCorrect3. intros A0 p H4; rewrite H4 in a. rewrite (checkPrfCorrect1 LNT LcodeLNT codeArityLNTF codeArityLNTR codeArityLNTFIsCorrect1 codeArityLNTRIsCorrect1) in a. discriminate a. *** decompose record (checkPrfCorrect2 LNT LcodeLNT codeArityLNTF codeArityLNTR codeArityLNTFIsCorrect1 codeArityLNTFIsCorrect2 codeArityLNTRIsCorrect1 codeArityLNTRIsCorrect2 _ _ b) /r; intros x2 H5 x3 x4 H6; rewrite <- H6. assert (H4: x2 = notH x). { eapply codeFormulaInj. assumption. } cut (code.codePrf (cl:=LcodeLNT) x3 x2 x4 = n). ---- generalize x4; clear H6 x4; rewrite H4. intros x4 H6; apply T'prf2Tprf. 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). * decompose record H3 /r; intros x2 x3 H4 H6. apply contradiction with x. -- exists x2, x3; assumption. -- assumption. * apply contradiction with (substF (LNN2LNT_formula A) 0 (natToTermLNT (code.codeFormula (cl:=LcodeLNT) x))). -- unfold A; replace (LNN2LNT_formula (forallH 1 (impH codeSysPrf (existH 2 (andH (LT (var 2) (var 1)) (substF codeSysPrfNot 1 (var 2))))))) with (forallH 1 (impH (LNN2LNT_formula codeSysPrf) (existH 2 (andH (LNN2LNT_formula (LT (var 2) (var 1))) (LNN2LNT_formula (substF codeSysPrfNot 1 (var 2))))))). ++ rewrite (subFormulaForall LNT). induction (eq_nat_dec 1 0) as [a | b]. ** discriminate a. ** induction (In_dec eq_nat_dec 1 (freeVarT (natToTermLNT (code.codeFormula (cl:=LcodeLNT) x)))). --- elim (closedNatToTerm _ _ a). --- clear b0 b; set (E := LNN2LNT_formula (nat_rec (fun _ => fol.Formula LNN) (LNT2LNN_formula (equal LNT.Zero LNT.Zero)) (fun (n : nat) rec => andH (notH (substF (substF codeSysPrf 0 (natToTermLNN (codeFormula x))) 1 (natToTermLNN 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. cut (In x2 (freeVarF (andH (notH (substF (substF codeSysPrf 0 (natToTermLNN (codeFormula x))) 1 (natToTermLNN n))) ((fix F (n : nat) : (fun _ : nat => fol.Formula LNN) n := match n with | O => LNT2LNN_formula (equal LNT.Zero LNT.Zero) | S n0 => (fun (n1 : nat) (rec : fol.Formula LNN) => andH (notH (substF (substF codeSysPrf 0 (natToTermLNN (codeFormula x))) 1 (natToTermLNN n1))) rec) n0 (F n0) end) n)))). ++ clear H3; intros H3; SimplFreeVar. ** apply (Compat815.le_not_lt x2 1). --- apply (freeVarCodeSysPrf LNT LcodeLNT codeArityLNTF codeArityLNTR codeArityLNTFIsPR codeArityLNTRIsPR (LNT2LNN_formula repT) v0 freeVarRepT'). apply H4. --- lia. ** rewrite <- LNT2LNN_natToTerm in H3. rewrite LNT2LNN_freeVarT in H3. apply (closedNatToTerm _ _ H3). ** rewrite <- LNT2LNN_natToTerm in H3. rewrite LNT2LNN_freeVarT in H3. apply (closedNatToTerm _ _ H3). ** assert (H4: In x2 (freeVarF (LNN2LNT_formula (nat_rec (fun _ : nat => fol.Formula LNN) (LNT2LNN_formula (equal LNT.Zero LNT.Zero)) (fun (n : nat) (rec : fol.Formula LNN) => andH (notH (substF (substF codeSysPrf 0 (natToTermLNN (codeFormula x))) 1 (natToTermLNN n))) rec) n)))) by apply LNN2LNT_freeVarF2, H3. apply (IHn _ H4). ++ apply LNN2LNT_freeVarF1, H3. } apply impE with E. +++ set (G := substF (substF (LNN2LNT_formula codeSysPrfNot) 0 (natToTerm (codeFormula x))) 1 (natToTerm (codePrf x0 (notH x) x1))). apply impE with G. *** apply sysExtend with PA. assumption. repeat apply impI. apply forallI. intros [x2 [H5 H6]]. induction H6 as [x2 H6| x2 H6]. induction H6 as [x2 H6| x2 H6]. apply (closedPA 1). exists x2; auto. induction H6. unfold G in H5; SimplFreeVar. induction H6. apply (H4 _ H5). rewrite (subFormulaImp LNT). rewrite (subFormulaExist LNT). induction (eq_nat_dec 2 0) as [a | b]. discriminate a. induction (In_dec eq_nat_dec 2 (freeVarT (natToTermLNT (code.codeFormula (cl:=LcodeLNT) x)))) as [a | b0]. elim (closedNatToTerm _ _ a). clear b0 b; rewrite (subFormulaAnd LNT). apply impE with (impH (substF (LNN2LNT_formula codeSysPrf) 0 (natToTermLNT (code.codeFormula (cl:=LcodeLNT) x))) (existH 2 (andH (LNN2LNT_formula (LT (var 2) (var 1))) (substF (LNN2LNT_formula (substF codeSysPrfNot 1 (var 2))) 0 (natToTermLNT (code.codeFormula (cl:=LcodeLNT) x)))))). repeat simple apply sysWeaken. apply iffE1. apply (reduceImp LNT). apply iffRefl. apply (reduceExist LNT). apply closedPA. apply (reduceAnd LNT). apply iffTrans with (LNN2LNT_formula (substF (LT (var 2) (var 1)) 0 (natToTermLNN (code.codeFormula (cl:=LcodeLNT) x)))). rewrite <- LNN2LNT_iff. apply NN2PA. apply (folLogic.iffRefl LNN). rewrite <- LNN2LNT_natToTerm. apply LNN2LNT_subFormula. apply iffRefl. apply orE with (LNN2LNT_formula (orH (LT (var 1) (natToTermLNN (codePrf x0 (notH x) x1))) (LNT2LNN_formula (equal (var 1) (natToTerm (codePrf x0 (notH x) x1)))))) (LNN2LNT_formula (LT (natToTermLNN (codePrf x0 (notH x) x1)) (var 1))). repeat simple apply sysWeaken. apply impE with (LNN2LNT_formula (orH (LT (var 1) (natToTermLNN (codePrf x0 (notH x) x1))) (orH (LNT2LNN_formula (equal (var 1) (natToTerm (codePrf x0 (notH x) x1)))) (LT (natToTermLNN (codePrf x0 (notH x) x1)) (var 1))))). repeat rewrite LNN2LNT_or. 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 NN2PA. simpl; rewrite LNT2LNN_natToTerm. apply nn9. apply impI. apply impE with G. apply impE with E. apply impE with (LNN2LNT_formula (LT (var 1) (natToTermLNN (S (codePrf x0 (notH x) x1))))). repeat simple apply sysWeaken. apply PAboundedLT. intros n H5; repeat rewrite (subFormulaImp LNT). repeat apply impI. fold codeFormula; apply contradiction with (substF (substF (LNN2LNT_formula codeSysPrf) 0 (natToTermLNT (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 (LNN2LNT_formula (nat_rec (fun _ : nat => fol.Formula LNN) (LNT2LNN_formula (equal LNT.Zero LNT.Zero)) (fun (n1 : nat) (rec : fol.Formula LNN) => andH (notH (substF (substF codeSysPrf 0 (natToTermLNN (codeFormula x))) 1 (natToTermLNN n1))) rec) n0)). apply sysWeaken. repeat apply impI. apply IHn0. assumption. unfold nat_rec, nat_rect; rewrite LNN2LNT_and. eapply andE2. apply Axm; right; constructor. unfold E, nat_rec, nat_rect; rewrite H3. rewrite LNN2LNT_and. apply impE with (LNN2LNT_formula (notH (substF (substF codeSysPrf 0 (natToTermLNN (codeFormula x))) 1 (natToTermLNN n0)))). apply sysWeaken. apply iffE1. apply iffTrans with (notH (LNN2LNT_formula (substF (substF codeSysPrf 0 (natToTermLNN (codeFormula x))) 1 (natToTermLNN n0)))). apply iffRefl. apply (reduceNot LNT). repeat rewrite <- LNN2LNT_natToTerm. apply iffTrans with (substF (LNN2LNT_formula (substF codeSysPrf 0 (natToTermLNN (codeFormula x)))) 1 (LNN2LNT_term (natToTermLNN n0))). apply LNN2LNT_subFormula. apply (reduceSub LNT). apply closedPA. apply LNN2LNT_subFormula. eapply andE1. apply Axm; right; constructor. apply impE with (substF E 1 (natToTerm n)). apply iffE1. apply (subFormulaNil LNT). apply H4. apply Axm; left; right; constructor. apply impE with (LNN2LNT_formula (orH (LT (var 1) (natToTermLNN (codePrf x0 (notH x) x1))) (LNT2LNN_formula (equal (var 1) (natToTerm (codePrf x0 (notH x) x1)))))). repeat simple apply sysWeaken. replace (impH (LNN2LNT_formula (orH (LT (var 1) (natToTermLNN (codePrf x0 (notH x) x1))) (LNT2LNN_formula (equal (var 1) (natToTerm (codePrf x0 (notH x) x1)))))) (LNN2LNT_formula (LT (var 1) (natToTermLNN (S (codePrf x0 (notH x) x1)))))) with (LNN2LNT_formula (impH (orH (LT (var 1) (natToTermLNN (codePrf x0 (notH x) x1))) (LNT2LNN_formula (equal (var 1) (natToTerm (codePrf x0 (notH x) x1))))) (LT (var 1) (natToTermLNN (S (codePrf x0 (notH x) x1)))))). apply NN2PA. simpl; rewrite LNT2LNN_natToTerm. apply nnPlusNotNeeded. reflexivity. 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 LNT). apply andI. apply impE with (LNN2LNT_formula (LT (natToTermLNN (codePrf x0 (notH x) x1)) (var 1))). repeat simple apply sysWeaken. apply impTrans with (LNN2LNT_formula (substF (LT (var 2) (var 1)) 2 (natToTermLNN (codePrf x0 (notH x) x1)))). replace (impH (LNN2LNT_formula (LT (natToTermLNN (codePrf x0 (notH x) x1)) (var 1))) (LNN2LNT_formula (substF (LT (var 2) (var 1)) 2 (natToTermLNN (codePrf x0 (notH x) x1))))) with (LNN2LNT_formula (impH (LT (natToTermLNN (codePrf x0 (notH x) x1)) (var 1)) (substF (LT (var 2) (var 1)) 2 (natToTermLNN (codePrf x0 (notH x) x1))))). apply NN2PA. unfold LT; apply (folLogic.impI LNN). rewrite (subFormulaRelation LNN). simpl; apply (folLogic.Axm LNN); right; constructor. reflexivity. apply iffE1. rewrite <- LNN2LNT_natToTerm. apply LNN2LNT_subFormula. apply Axm; right; constructor. apply sysWeaken. apply sysWeaken. apply impE with (substF (substF (LNN2LNT_formula codeSysPrfNot) 0 (natToTerm (codeFormula x))) 1 (natToTerm (codePrf x0 (notH x) x1))). apply sysWeaken. apply iffE2. fold codeFormula; apply iffTrans with (substF (substF (substF (LNN2LNT_formula codeSysPrfNot) 1 (var 2)) 0 (natToTermLNT (codeFormula x))) 2 (natToTerm (codePrf x0 (notH x) x1))). repeat (apply (reduceSub LNT); [ apply closedPA | idtac ]). replace (var 2) with (LNN2LNT_term (var 2)). apply LNN2LNT_subFormula. reflexivity. apply iffTrans with (substF (substF (substF (LNN2LNT_formula codeSysPrfNot) 0 (natToTermLNT (codeFormula x))) 1 (var 2)) 2 (natToTerm (codePrf x0 (notH x) x1))). repeat (apply (reduceSub LNT); [ apply closedPA | idtac ]). apply (subFormulaExch LNT). discriminate. intros H5; SimplFreeVar. discriminate H6. apply closedNatToTerm. apply (subFormulaTrans LNT). unfold not in |- *; intros; SimplFreeVar. apply (Compat815.le_not_lt 2 1). apply freeVarCodeSysPrfN. apply LNN2LNT_freeVarF1. assumption. apply Nat.lt_succ_diag_r. apply Axm; right; constructor. *** unfold G; apply impE with (LNN2LNT_formula (substF (substF codeSysPrfNot 0 (natToTermLNN (codeFormula x))) 1 (natToTermLNN (codePrf x0 (notH x) x1)))). apply iffE1. repeat rewrite <- LNN2LNT_natToTerm. apply iffTrans with (substF (LNN2LNT_formula (substF codeSysPrfNot 0 (natToTermLNN (codeFormula x)))) 1 (LNN2LNT_term (natToTermLNN (codePrf x0 (notH x) x1)))). apply LNN2LNT_subFormula. apply sysExtend with PA. assumption. apply (reduceSub LNT). apply closedPA. apply LNN2LNT_subFormula. apply T'prf2Tprf. apply codeSysPrfNCorrect1. assumption. +++ clear H4; unfold E; clear E. induction (S (codePrf x0 (notH x) x1)). *** simpl; apply eqRefl. *** unfold nat_rec, nat_rect; rewrite LNN2LNT_and. apply andI. ---- induction (eq_nat_dec (checkPrf LNT LcodeLNT codeArityLNTF codeArityLNTR (codeFormula x) n) 0) as [a | b]. ++++ unfold codeSysPrf, codeFormula in |- *. apply T'prf2Tprf. apply codeSysPrfCorrect3. intros A0 p H4; rewrite H4 in a. rewrite (checkPrfCorrect1 LNT LcodeLNT codeArityLNTF codeArityLNTR codeArityLNTFIsCorrect1 codeArityLNTRIsCorrect1) in a. discriminate a. ++++ decompose record (checkPrfCorrect2 LNT LcodeLNT codeArityLNTF codeArityLNTR codeArityLNTFIsCorrect1 codeArityLNTFIsCorrect2 codeArityLNTRIsCorrect1 codeArityLNTRIsCorrect2 _ _ b) /r. intros x2 H5 x3 x4 H6; rewrite <- H6. assert (H4: x2 = x). { eapply (codeFormulaInj LNT). assumption. } rewrite <- H4. apply T'prf2Tprf. 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. ++ reflexivity. -- apply impE with (notH x). ++ apply cp2, iffE2. apply sysExtend with PA. apply extendsPA. 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) 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)