KM.Algebra.KMH_implicative

From Stdlib Require Import Ensembles.

Require Import syntax.
Require Import KMH_export.

Implicativity of KM

Section implicative.

A syntactic property entailing that a logic is algebraisable is that implicativity. It consists of 5 properties.

Property 1.

Theorem KMH_IL1 ϕ : KMH_prv (Empty_set _) (ϕ → ϕ).
Proof.
apply imp_Id_gen.
Qed.

Property 3.

Theorem KMH_IL2 ϕ ψ χ : KMH_prv (fun δ => δ = (ϕ → ψ ) \/ δ = (ψ → χ )) (ϕ → χ).
Proof.
eapply meta_Imp_trans.
- apply Id ; left ; split.
- apply Id ; right ; split.
Qed.

Property 4.

Theorem KMH_IL4 ϕ ψ : KMH_prv (fun δ => δ = ϕ \/ δ = (ϕ → ψ )) ψ.
Proof.
eapply MP.
- apply Id ; right ; split.
- apply Id ; left ; split.
Qed.

Property 5.

Theorem KMH_IL5 ϕ ψ : KMH_prv (Singleton _ ϕ) (ψ → ϕ).
Proof.
eapply MP.
- apply Thm_irrel.
- apply Id ; split.
Qed.

Property 3 is shown for each of the logical operators the language.

Theorem KMH_IL3_Top :
    KMH_prv (Empty_set _) (⊤ → ⊤).
Proof.
apply imp_Id_gen.
Qed.

Theorem KMH_IL3_Bot :
    KMH_prv (Empty_set _) (⊥ → ⊥).
Proof.
apply imp_Id_gen.
Qed.

Definition EqImp4 ϕ1 ϕ2 ψ1 ψ2 := fun δ => δ = (ϕ1 → ϕ2 ) \/ δ = (ψ1 → ψ2 ) \/ δ = (ϕ2 → ϕ1 ) \/ δ = (ψ2 → ψ1 ).

Theorem KMH_IL3_And ϕ1 ϕ2 ψ1 ψ2 :
    KMH_prv (EqImp4 ϕ1 ϕ2 ψ1 ψ2) ((ϕ1 ∧ ψ1 ) → (ϕ2 ∧ ψ2 )).
Proof.
eapply MP.
- eapply MP.
  + apply Ax ; left ; eapply IA8 ; reflexivity.
  + eapply meta_Imp_trans.
    * apply Ax ; left ; eapply IA6 ; reflexivity.
    * apply Id ; firstorder.
- eapply meta_Imp_trans.
  + apply Ax ; left ; eapply IA7 ; reflexivity.
  + apply Id ; firstorder.
Qed.

Theorem KMH_IL3_Or ϕ1 ϕ2 ψ1 ψ2 :
    KMH_prv (EqImp4 ϕ1 ϕ2 ψ1 ψ2) ((ϕ1 ∨ ψ1 ) → (ϕ2 ∨ ψ2 )).
Proof.
eapply MP.
- eapply MP.
  + apply Ax ; left ; eapply IA5 ; reflexivity.
  + eapply meta_Imp_trans.
    * apply Id. left ; reflexivity.
    * apply Ax ; left ; eapply IA3 ; reflexivity.
- apply meta_Imp_trans with ψ2.
  + apply Id ; firstorder.
  + apply Ax ; left ; eapply IA4 ; reflexivity.
Qed.

Theorem KMH_IL3_Imp ϕ1 ϕ2 ψ1 ψ2 :
    KMH_prv (EqImp4 ϕ1 ϕ2 ψ1 ψ2) ((ϕ1 → ψ1 ) → (ϕ2 → ψ2 )).
Proof.
eapply MP.
- apply And_Imp.
- apply meta_Imp_trans with ψ1.
  + apply meta_Imp_trans with ((ϕ1 → ψ1) ∧ ϕ1).
    * eapply MP.
      -- eapply MP.
        ++ apply Ax ; left ; eapply IA8 ; reflexivity.
        ++ apply Ax ; left ; eapply IA6 ; reflexivity.
      -- apply meta_Imp_trans with ϕ2.
        ++ apply Ax ; left ; eapply IA7 ; reflexivity.
        ++ apply Id ; firstorder.
    * eapply MP ; [ apply Imp_And | apply imp_Id_gen].
  + apply Id ; firstorder.
Qed.

Definition EqImp2 ϕ ψ := fun δ => δ = (ϕ → ψ ) \/ δ = (ψ → ϕ ).

Theorem KMH_IL3_Box ϕ ψ :
    KMH_prv (EqImp2 ϕ ψ) ((□ ϕ ) → (□ ψ )).
Proof.
eapply MP.
- apply Ax ; right ; eapply K ; reflexivity.
- apply gKMH_id_KMH. apply gNec.
  apply gId ; unfold In ; left ; auto.
Qed.

End implicative.