Library Goedel.rosser

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 Export Languages.
From Goedel Require Import fixPoint.
From Goedel Require Import codeSysPrf.
From hydras.Ackermann Require Import NNtheory.
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.
Import LNN NN NNnotations.
From hydras Require Import Compat815.

Section Rosser's_Incompleteness.

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

Variable T : System.

Hypothesis extendsNN : Included _ NN 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 codeSysPrf :=
  codeSysPrf LNN LcodeLNN codeArityLNTF codeArityLNNR
    codeArityLNTFIsPR codeArityLNNRIsPR repT v0.

Definition codeSysPrfCorrect1 :=
  codeSysPrfCorrect1 LNN LcodeLNN codeArityLNTF
    codeArityLNNR codeArityLNTFIsPR codeArityLNTFIsCorrect1 codeArityLNNRIsPR
    codeArityLNNRIsCorrect1 T extendsNN T repT v0 freeVarRepT expressT1.

Definition codeSysPrfCorrect2 :=
  codeSysPrfCorrect2 LNN LcodeLNN codeArityLNTF
    codeArityLNNR codeArityLNTFIsPR codeArityLNTFIsCorrect1 codeArityLNNRIsPR
    codeArityLNNRIsCorrect1 T extendsNN T repT v0 freeVarRepT expressT2.

Definition codeSysPrfCorrect3 :=
  codeSysPrfCorrect3 LNN LcodeLNN codeArityLNTF
    codeArityLNNR codeArityLNTFIsPR codeArityLNTFIsCorrect1
    codeArityLNTFIsCorrect2 codeArityLNNRIsPR codeArityLNNRIsCorrect1
    codeArityLNNRIsCorrect2 T extendsNN.


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

Definition codeSysPrfNot :=
  codeSysPrfNot LNN LcodeLNN codeArityLNTF
    codeArityLNNR codeArityLNTFIsPR codeArityLNNRIsPR repT v0.

Definition freeVarCodeSysPrfN :=
  freeVarCodeSysPrfN LNN LcodeLNN codeArityLNTF
    codeArityLNNR codeArityLNTFIsPR codeArityLNNRIsPR repT v0 freeVarRepT.

Definition codeSysPrfNCorrect1 :=
  codeSysPrfNCorrect1 LNN LcodeLNN codeArityLNTF
    codeArityLNNR codeArityLNTFIsPR codeArityLNTFIsCorrect1 codeArityLNNRIsPR
    codeArityLNNRIsCorrect1 T extendsNN T repT v0 freeVarRepT expressT1.

Definition codeSysPrfNCorrect2 :=
  codeSysPrfNCorrect2 LNN LcodeLNN codeArityLNTF
    codeArityLNNR codeArityLNTFIsPR codeArityLNTFIsCorrect1 codeArityLNNRIsPR
    codeArityLNNRIsCorrect1 T extendsNN T repT v0 freeVarRepT expressT2.

Definition codeSysPrfNCorrect3 :=
  codeSysPrfNCorrect3 LNN LcodeLNN codeArityLNTF
    codeArityLNNR codeArityLNTFIsPR codeArityLNTFIsCorrect1
    codeArityLNTFIsCorrect2 codeArityLNNRIsPR codeArityLNNRIsCorrect1
    codeArityLNNRIsCorrect2 T extendsNN
    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 LNN A a),
    (∃ B : Formulas,
        (∃ q : Prf LNN B b,
            codePrf _ _ q < S (codePrf _ _ p) ∧
              (∀ x : Formula, In x B → mem _ T x))) ∨
      (∀ (B : Formulas) (q : Prf LNN B b),
          codePrf _ _ q < S (codePrf _ _ p) →
          ∃ g : Formula, In g B ∧ ¬ mem _ T g).

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

End Rosser's_Incompleteness.

Definition RepresentsInSelf (T:System) :=
  ∃ rep:Formula, ∃ v:nat,
    (∀ x : nat, In x (freeVarF rep) → x = v) ∧
      (∀ f : Formula,
          mem Formula T f →
          SysPrf T (substF rep v (natToTerm (codeFormula f)))) ∧
      (∀ f : Formula,
          ¬ mem Formula T f →
          SysPrf T
            (notH (substF rep v (natToTerm (codeFormula f))))).

Definition DecidableSet (A:_)(s:Ensemble A) :=
  (∀ x : A,
      mem A s x ∨
        ¬ mem A s x).

Theorem Incompleteness :
  ∀ T : System,
    Included Formula NN T →
    RepresentsInSelf T →
    DecidableSet Formula T →
    ∃ f : Formula,
      (Sentence f) ∧
        (SysPrf T f ∨ SysPrf T (notH f) → Inconsistent LNN T).