Library Goedel.goedel2

From Coq Require Import Ensembles.
From Coq Require Import List.
From Coq Require Import Arith.
From hydras.Ackermann Require Import folProp.
From hydras.Ackermann Require Import folProof.
From hydras.Ackermann Require Import folReplace.
From hydras.Ackermann Require Import folLogic3.
From hydras.Ackermann Require Import subProp.
From hydras.Ackermann Require Import ListExt.

From Goedel Require Import fixPoint.
From hydras.Ackermann Require Import NN2PA.
From Goedel Require Import codeSysPrf.
From hydras.Ackermann Require Import PAtheory.
From hydras.Ackermann Require Import code.
From hydras.Ackermann Require Import checkPrf.
From hydras.Ackermann Require Import codeNatToTerm.
From Goedel Require Import rosserPA.

Section Goedel's_2nd_Incompleteness.

  Variable T : System.

  Hypothesis extendsPA : Included _ PA T.

  Variable repT : Formula.
  Variable v0 : nat.
  Hypothesis
    freeVarRepT : ∀ v : nat, In v (freeVarF repT) → v = v0.
  Hypothesis
    expressT1 :
    ∀ f : Formula,
      mem _ T f →
      SysPrf T (substF repT v0 (natToTerm (codeFormula f))).
  Hypothesis
    expressT2 :
    ∀ f : Formula,
      ¬ mem _ T f →
      SysPrf T
        (notH (substF repT v0 (natToTerm (codeFormula f)))).

  Definition codeSysPf :=
    (codeSysPf LNT LcodeLNT codeArityLNTF codeArityLNTR
       codeArityLNTFIsPR codeArityLNTRIsPR (LNT2LNN_formula repT) v0).

  Section Goedel1PA.


    Definition T' := T' T.

    Definition extendsNN := extendsNN T.

    Definition Tprf2T'prf := Tprf2T'prf T.

    Definition expressT'1 := expressT'1 T repT v0 expressT1.

    Definition expressT'2 := expressT'2 T repT v0 expressT2.

    Definition freeVarRepT' := freeVarRepT' repT v0 freeVarRepT.

    Definition codeSysPfCorrect :=
      codeSysPfCorrect LNT LcodeLNT codeArityLNTF
        codeArityLNTR codeArityLNTFIsPR codeArityLNTFIsCorrect1
        codeArityLNTRIsPR
        codeArityLNTRIsCorrect1 T' extendsNN T (LNT2LNN_formula repT) v0
        freeVarRepT' expressT'1.

    Definition G := let (a,_) :=
                      FixPointLNT (notH (LNN2LNT_formula codeSysPf)) 0
                    in a.

    Definition box (f:Formula) :=
      (substF (LNN2LNT_formula codeSysPf) 0
         (natToTerm (codeFormula f))).

    Lemma GS : SysPrf T (iffH G (notH (box G))).

    Lemma HBL1 : ∀ f, SysPrf T f → SysPrf T (box f).

    Lemma FirstIncompletenessA : SysPrf T G → Inconsistent LNT T.

  End Goedel1PA.

  Definition F : Formula :=
    (notH (L:= LNT) (forallH 0 (equal (var 0) (var 0)))).

  Definition Con := notH (box F).

  Hypothesis HBL2 : ∀ f, SysPrf T (impH (box f) (box (box f))).
  Hypothesis HBL3 : ∀ f g, SysPrf T (impH (box (impH f g)) (impH (box f) (box g))).

  Theorem SecondIncompletness :
    SysPrf T Con → Inconsistent LNT T.

End Goedel's_2nd_Incompleteness.