Library hydras.Ackermann.folProof

From Coq Require Import Ensembles Lists.List Arith.
Import ListNotations.

From hydras.Ackermann Require Export fol.
From hydras.Ackermann Require Import folProp.
Import FolNotations.

Section ProofH.

Variable L : Language.

Let Formula := Formula L.
Let Formulas := Formulas L.
Let System := System L.
Let Term := Term L.
Let Terms := Terms L.

Fixpoint nVars (n: nat) : Terms n × Terms n:=
  match n with
    0 ⇒ (Tnil, Tnil)
  | S n0 ⇒
      (let (a,b) := nVars n0 in
       (Tcons (var (n0 + n0)) a,
         Tcons (var (S (n0 + n0))) b))
  end.

Section Example.
End Example.

Definition AxmEq4 (R : Relations L) : Formula.

Definition AxmEq5 (f : Functions L) : Formula.

Inductive Prf : Formulas → Formula → Set :=
| AXM : ∀ A : Formula, Prf [A] A
| MP :
  ∀ (Hyp1 Hyp2 : Formulas) (A B : Formula),
    Prf Hyp1 (A → B)%fol → Prf Hyp2 A → Prf (Hyp1 ++ Hyp2) B
| GEN :
  ∀ (Hyp : Formulas) (A : Formula) (v : nat),
    ¬ In v (freeVarListFormula L Hyp) → Prf Hyp A →
    Prf Hyp (allH v, A)%fol
| IMP1 : ∀ A B : Formula, Prf [] (A → B → A)%fol
| IMP2 :
  ∀ A B C : Formula,
    Prf [] ((A → B → C) → (A → B) → A → C)%fol
| CP :
  ∀ A B : Formula,
    Prf [] ((¬ A → ¬ B) → B → A)%fol
| FA1 :
  ∀ (A : Formula) (v : nat) (t : Term),
    Prf [] ((allH v, A) → substF A v t)%fol
| FA2 :
  ∀ (A : Formula) (v : nat),
    ¬ In v (freeVarF A) → Prf [] (A → allH v, A)%fol
| FA3 :
  ∀ (A B : Formula) (v : nat),
    Prf []
      ((allH v, A → B) → (allH v, A) → allH v, B)%fol
| EQ1 : Prf [] (v#0 = v#0)%fol
| EQ2 : Prf [] (v#0 = v#1 → v#1 = v#0)%fol
| EQ3 : Prf [] (v#0 = v#1 → v#1 = v#2 → v#0 = v#2)%fol
| EQ4 : ∀ R : Relations L, Prf [] (AxmEq4 R)
| EQ5 : ∀ f : Functions L, Prf [] (AxmEq5 f).

Definition SysPrf (T : System) (f : Formula) :=
  ∃ Hyp : Formulas,
    (∃ prf : Prf Hyp f,
       (∀ g : Formula, In g Hyp → mem _ T g)).

Definition Inconsistent (T : System) := ∀ f : Formula, SysPrf T f.

Definition Consistent (T : System) := ∃ f : Formula, ¬ SysPrf T f.

Definition independent T f := ¬ SysPrf T f ∧ ¬ SysPrf T (¬ f)%fol.

End ProofH.

Arguments independent {L} _ _.

Notation undecidable := (independent) (only parsing).