KM.GHC.KMH

From Stdlib Require Import Ensembles.

Require Import syntax.

(* We define here the intuitionistic axioms. *)

Inductive IAxioms (F : form) : Prop :=
 | IA1 A B : F = (A → (B → A)) -> IAxioms F
 | IA2 A B C : F = ((A → (B → C)) → ((A → B) → (A → C))) -> IAxioms F
 | IA3 A B : F = (A → (A ∨ B)) -> IAxioms F
 | IA4 A B : F = (B → (A ∨ B)) -> IAxioms F
 | IA5 A B C : F = ((A → C) → ((B → C) → ((A ∨ B) → C))) -> IAxioms F
 | IA6 A B : F = ((A ∧ B) → A) -> IAxioms F
 | IA7 A B : F = ((A ∧ B) → B) -> IAxioms F
 | IA8 A B C : F = ((A → B) → ((A → C) → (A → (B ∧ C)))) -> IAxioms F
 | IA9 A : F = (⊥ → A) -> IAxioms F.

(* We then define the modal axioms. *)

Inductive MAxioms (F : form) : Prop :=
 | K A B : F = ((□ (A → B)) → ((□ A) → □ B)) -> MAxioms F
 | L A : F = (((□ A) → A) → A) -> MAxioms F
 | NA A B : F = ((□ A) → (B ∨ (B → A))) -> MAxioms F.

(* And join both set of axioms. *)

Definition Axioms (A : form) : Prop := IAxioms A \/ MAxioms A.

(* We can then define the generalised Hilbert system for local and 
   global KM, i.e. lKM and gKM. *)

Inductive KMH_prv : (form -> Prop) -> form -> Prop :=
  | Id Γ A : In _ Γ A -> KMH_prv Γ A
  | Ax Γ A : Axioms A -> KMH_prv Γ A
  | MP Γ A B : KMH_prv Γ (A → B) -> KMH_prv Γ A -> KMH_prv Γ B
  | Nec Γ A : KMH_prv (Empty_set _) A -> KMH_prv Γ (□ A).

  Inductive gKMH_prv : (form -> Prop) -> form -> Prop :=
  | gId Γ A : In _ Γ A -> gKMH_prv Γ A
  | gAx Γ A : Axioms A -> gKMH_prv Γ A
  | gMP Γ A B : gKMH_prv Γ (A → B) -> gKMH_prv Γ A -> gKMH_prv Γ B
  | gNec Γ A : gKMH_prv Γ A -> gKMH_prv Γ (□ A).