Library hydras.Ackermann.folLogic

From Coq Require Import Ensembles List.

From hydras.Ackermann Require Import ListExt folProof folProp Deduction.
Import FolNotations.

Section Logic_Rules.

Variable L : Language.
Let Formula := Formula L.
Let Formulas := Formulas L.
Let System := System L.
Let Term := Term L.
Let Terms := Terms L.
Let Prf := Prf L.
Let SysPrf := SysPrf L.
Arguments Ensembles.Add {U} _ _.

Lemma Axm T f: mem _ T f → SysPrf T f.

Lemma sysExtend (T U : System) (f : Formula):
 Included _ T U → SysPrf T f → SysPrf U f.

Lemma sysWeaken (T : System) (f g : Formula):
  SysPrf T f → SysPrf (Ensembles.Add T g) f.

Lemma impI (T : System) (f g : Formula):
 SysPrf (Ensembles.Add T g) f → SysPrf T (g → f)%fol.

Lemma impE (T : System) (f g : Formula):
 SysPrf T (g → f)%fol → SysPrf T g → SysPrf T f.

Lemma contradiction (T : System) (f g : Formula):
 SysPrf T f → SysPrf T (¬ f)%fol → SysPrf T g.

Lemma nnE (T : System) (f : Formula): SysPrf T (¬ ¬ f)%fol → SysPrf T f.

Lemma nnI (T : System) (f : Formula): SysPrf T f → SysPrf T (¬ ¬ f)%fol.

Lemma cp1 (T : System) (f g : Formula) :
 SysPrf T (¬ f → ¬ g)%fol → SysPrf T (g → f)%fol.

Lemma cp2 (T : System) (f g : Formula):
 SysPrf T (g → f)%fol → SysPrf T (¬f → ¬g)%fol.

Lemma orI1 (T : System) (f g : Formula): SysPrf T f → SysPrf T (f ∨ g)%fol.

Lemma orI2 (T : System) (f g : Formula): SysPrf T g → SysPrf T (f ∨ g)%fol.

Lemma noMiddle (T : System) (f : Formula): SysPrf T (¬ f ∨ f)%fol.

Lemma orE (T : System) (f g h : Formula):
 SysPrf T (f ∨ g)%fol →
 SysPrf T (f → h)%fol → SysPrf T (g → h)%fol → SysPrf T h.

Lemma orSys (T : System) (f g h : Formula):
 SysPrf (Ensembles.Add T f) h → SysPrf (Ensembles.Add T g) h →
 SysPrf (Ensembles.Add T (f ∨ g)%fol) h.

Lemma andI (T : System) (f g : Formula):
 SysPrf T f → SysPrf T g → SysPrf T (f ∧ g)%fol.

Lemma andE1 (T : System) (f g : Formula):
  SysPrf T (f ∧ g)%fol → SysPrf T f.

Lemma andE2 (T : System) (f g : Formula):
  SysPrf T (f ∧ g)%fol → SysPrf T g.

Lemma iffI (T : System) (f g : Formula) :
 SysPrf T (f → g)%fol → SysPrf T (g → f)%fol → SysPrf T (f ↔ g)%fol.

Lemma iffE1 (T : System) (f g : Formula):
  SysPrf T (f ↔ g)%fol → SysPrf T (f → g)%fol.

Lemma iffE2 (T : System) (f g : Formula):
  SysPrf T (f ↔ g)%fol → SysPrf T (g → f)%fol.

Lemma forallI (T : System) (f : Formula) (v : nat):
 ¬ In_freeVarSys L v T → SysPrf T f → SysPrf T (allH v, f)%fol.

Lemma forallE (T : System) (f : Formula) (v : nat) (t : Term):
 SysPrf T (allH v, f)%fol → SysPrf T (substF f v t).

Lemma forallSimp (T : System) (f : Formula) (v : nat):
  SysPrf T (allH v, f)%fol → SysPrf T f.

Lemma existI (T : System) (f : Formula) (v : nat) (t : Term):
  SysPrf T (substF f v t) → SysPrf T (exH v, f)%fol.

Lemma existE (T : System) (f g : Formula) (v : nat):
 ¬ In_freeVarSys L v T →
 ¬ In v (freeVarF g) →
 SysPrf T (exH v, f)%fol → SysPrf T (f → g)%fol → SysPrf T g.

Lemma existSimp (T : System) (f : Formula) (v : nat) :
 SysPrf T f → SysPrf T (exH v, f)%fol.

Lemma existSys (T : System) (f g : Formula) (v : nat):
 ¬ In_freeVarSys L v T →
 ¬ In v (freeVarF g) →
 SysPrf (Ensembles.Add T f) g →
 SysPrf (Ensembles.Add T (exH v, f)%fol) g.

Section Not_Rules.

Lemma absurd1 (T : System) (f : Formula) :
 SysPrf T (f → ¬f)%fol → SysPrf T (¬f)%fol.

Lemma nImp (T : System) (f g : Formula) :
 SysPrf T (f ∧ ¬g)%fol → SysPrf T (¬ (f → g))%fol.

Lemma nOr (T : System) (f g : Formula):
 SysPrf T (¬ f ∧ ¬ g)%fol → SysPrf T (¬ (f ∨ g))%fol.

Lemma nAnd (T : System) (f g : Formula):
 SysPrf T (¬ f ∨ ¬ g)%fol → SysPrf T (¬ (f ∧ g))%fol.

Lemma nForall (T : System) (f : Formula) (v : nat) :
 SysPrf T (exH v, ¬ f)%fol → SysPrf T (¬ (allH v, f))%fol.

Lemma nExist (T : System) (f : Formula) (v : nat):
 SysPrf T (allH v, ¬f)%fol → SysPrf T (¬ (exH v, f))%fol.

End Not_Rules.

Section Other_Rules.

Lemma impRefl (T : System) (f : Formula): SysPrf T (f → f)%fol.

Lemma impTrans (T : System) (f g h : Formula):
 SysPrf T (f → g)%fol → SysPrf T (g → h)%fol → SysPrf T (f → h)%fol.

Lemma orSym (T : System) (f g : Formula):
 SysPrf T (f ∨ g)%fol → SysPrf T (g ∨ f)%fol.

Lemma andSym (T : System) (f g : Formula):
  SysPrf T (f ∧ g)%fol → SysPrf T (g ∧ f)%fol.

Lemma iffRefl (T : System) (f : Formula) : SysPrf T (f ↔ f)%fol.

Lemma iffSym (T : System) (f g : Formula) :
  SysPrf T (f ↔ g)%fol → SysPrf T (g ↔ f)%fol.

Lemma iffTrans (T : System) (f g h : Formula):
 SysPrf T (f ↔ g)%fol → SysPrf T (g ↔ h)%fol → SysPrf T (f ↔ h)%fol.

End Other_Rules.

Lemma openClosed (T : System) (f : Formula):
 SysPrf T (close L f) → SysPrf T f.

End Logic_Rules.