Library Goedel.goedel1

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 subProp.
From hydras.Ackermann Require Import ListExt.
From Goedel Require Import fixPoint codeSysPrf.
From hydras.Ackermann Require Import wConsistent.
From hydras.Ackermann Require Import NN.
From hydras.Ackermann Require Import code.
From hydras.Ackermann Require Import checkPrf.
From hydras Require Import Compat815.

From LibHyps Require Export LibHyps.
From hydras Require Export MoreLibHyps NewNotations.

Import NNnotations codeNatToTerm.

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

Notation reflection f := (natToTerm (codeFNN f)).

Section Goedel's_1st_Incompleteness.

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 (reflection f)).

Hypothesis
  expressT2 :
    ∀ f : Formula, ¬ mem _ T f →
    SysPrf T (¬ (substF repT v0 (reflection f)))%fol.

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

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

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

Definition codeSysPfCorrect :=
  codeSysPfCorrect 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.

Lemma freeVarG : closed G.

Lemma FirstIncompletenessA : SysPrf T G → Inconsistent LNN T.


Lemma FirstIncompletenessB :
  wConsistent T → ¬ SysPrf T (notH G).

Theorem Goedel'sIncompleteness1st :
 wConsistent T →
 ∃ f : Formula, independent T f ∧ closed f.

End Goedel's_1st_Incompleteness.