Library Goedel.rosserPA

From Coq Require Import Ensembles.
From Coq Require Import List.
From Coq Require Import Arith Lia.
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 hydras.Ackermann Require Import NNtheory.
From hydras.Ackermann Require Import NN2PA.
From Goedel Require Import fixPoint.
From Goedel Require Import codeSysPrf.
From hydras.Ackermann Require Import PAtheory.
From hydras.Ackermann Require Import code.
From Goedel Require Import PRrepresentable.
From hydras.Ackermann Require Import expressible.
From hydras.Ackermann Require Import checkPrf.
From hydras.Ackermann Require Import codeNatToTerm.
From hydras Require Import Compat815.
Import NNnotations.

Section Rosser's_Incompleteness.

  Definition codeFormula := codeFormula (cl:=LcodeLNT).

  Variable T : System.
  Definition T' : fol.System LNN :=
    Union _ NN
      (fun x : fol.Formula LNN ⇒ mem _ T (LNN2LNT_formula x)).

Lemma extendsNN : Included _ NN T'.

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)))).

Lemma freeVarRepT' :
 ∀ v : nat, In v (freeVarF (LNT2LNN_formula repT)) → v = v0.

Lemma Tprf2T'prf :
  ∀ f : Formula, SysPrf T f → folProof.SysPrf LNN T' (LNT2LNN_formula f).

Lemma expressT'1 :
 ∀ f : Formula,
 mem _ T f →
 folProof.SysPrf LNN T'
   (substF (LNT2LNN_formula repT) v0
      (natToTermLNN (codeFormula f))).

Lemma expressT'2 :
  ∀ f : Formula,
    ¬ mem _ T f →
    folProof.SysPrf LNN T'
      (notH
         (substF (LNT2LNN_formula repT) v0
            (natToTermLNN (codeFormula f)))).

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

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

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

Definition codeSysPrfCorrect3 :=
  codeSysPrfCorrect3 LNT LcodeLNT codeArityLNTF
    codeArityLNTR codeArityLNTFIsPR codeArityLNTFIsCorrect1
    codeArityLNTFIsCorrect2 codeArityLNTRIsPR codeArityLNTRIsCorrect1
    codeArityLNTRIsCorrect2 T'
    extendsNN.

Definition codePrf := codePrf (cl:=LcodeLNT).

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

Definition freeVarCodeSysPrfN :=
  freeVarCodeSysPrfN LNT LcodeLNT codeArityLNTF
    codeArityLNTR codeArityLNTFIsPR codeArityLNTRIsPR
    (LNT2LNN_formula repT) v0 freeVarRepT'.

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

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

Definition codeSysPrfNCorrect3 :=
  codeSysPrfNCorrect3 LNT LcodeLNT codeArityLNTF
    codeArityLNTR codeArityLNTFIsPR codeArityLNTFIsCorrect1
    codeArityLNTFIsCorrect2 codeArityLNTRIsPR codeArityLNTRIsCorrect1
    codeArityLNTRIsCorrect2 T'
    extendsNN (LNT2LNN_formula repT) v0 freeVarRepT'.

Lemma decideAxioms :
  (∀ x : Formula, mem _ T x ∨ ¬ mem _ T x) →
  ∀ x : Formulas,
    (∀ g : Formula, In g x → mem _ T g) ∨
      (∃ g : Formula, In g x ∧ ¬ mem _ T g).

Lemma searchProof :
  (∀ x : Formula, mem _ T x ∨ ¬ mem _ T x) →
  ∀ (a b : Formula) (A : Formulas) (p : Prf LNT A a),
    (∃ B : Formulas,
        (∃ q : Prf LNT B b,
            codePrf _ _ q < S (codePrf _ _ p) ∧
              (∀ x : Formula, In x B → mem _ T x))) ∨
      (∀ (B : Formulas) (q : Prf LNT B b),
          codePrf _ _ q < S (codePrf _ _ p) →
          ∃ g : Formula, In g B ∧ ¬ mem _ T g).

Lemma T'prf2Tprf :
  ∀ f : fol.Formula LNN,
    folProof.SysPrf LNN T' f → SysPrf T (LNN2LNT_formula f).


Theorem Rosser'sIncompleteness :
  (∀ x : Formula, mem _ T x ∨ ¬ mem _ T x) →
  ∃ f : Formula,
    (∀ v : nat, ¬ In v (freeVarF f)) ∧
      (SysPrf T f ∨ SysPrf T (notH f) → Inconsistent LNT T).

End Rosser's_Incompleteness.

From hydras.Ackermann Require Import codePA.
From hydras.Ackermann Require Import PAconsistent.

Theorem PAIncomplete :
 ∃ f : Formula,
   (Sentence f) ∧ ~(SysPrf PA f ∨ SysPrf PA (notH f)).