add(InterpretabilityLogic): Add completeness of IL

Foundation.lean

@@ -188,7 +188,8 @@ import Foundation.ProvabilityLogic.Classification.Trace
 
 -- Interpretability Logic
 import Foundation.InterpretabilityLogic.Veltman.Logic.CL
-import Foundation.InterpretabilityLogic.Veltman.Logic.IL
+import Foundation.InterpretabilityLogic.Veltman.Logic.IL.Soundness
+import Foundation.InterpretabilityLogic.Veltman.Logic.IL.Completeness
 
 -- Meta
 import Foundation.Meta.Qq

Foundation/InterpretabilityLogic/Formula/Basic.lean

@@ -53,7 +53,6 @@ instance : LukasiewiczAbbrev (Formula α) where
 instance : DiaAbbrev (Formula α) := ⟨rfl⟩
 
 
-
 @[simp, grind] lemma and_inj : φ₁ ⋏ φ₂ = ψ₁ ⋏ ψ₂ ↔ φ₁ = ψ₁ ∧ φ₂ = ψ₂ := by simp [Wedge.wedge]
 
 @[simp, grind] lemma or_inj : φ₁ ⋎ φ₂ = ψ₁ ⋎ ψ₂ ↔ φ₁ = ψ₁ ∧ φ₂ = ψ₂ := by simp [Vee.vee]
@@ -65,6 +64,22 @@ instance : DiaAbbrev (Formula α) := ⟨rfl⟩
 @[simp, grind] lemma neg_inj : ∼φ = ∼ψ ↔ φ = ψ := by simp [NegAbbrev.neg];
 
 
+@[simp, grind] lemma eq_falsum : (falsum : Formula α) = ⊥ := rfl
+
+@[simp, grind] lemma eq_or : or φ ψ = φ ⋎ ψ := rfl
+
+@[simp, grind] lemma eq_and : and φ ψ = φ ⋏ ψ := rfl
+
+@[simp, grind] lemma eq_imp : imp φ ψ = φ ➝ ψ := rfl
+
+@[simp, grind] lemma eq_neg : neg φ = ∼φ := rfl
+
+@[simp, grind] lemma eq_box : box φ = □φ := rfl
+
+@[simp, grind] lemma eq_dia : dia φ = ◇φ := rfl
+
+
+
 section ToString
 
 variable [ToString α]

Foundation/InterpretabilityLogic/Formula/Complement.lean

@@ -0,0 +1,89 @@
+import Foundation.InterpretabilityLogic.Formula.Basic
+import Foundation.Propositional.CMCF
+
+namespace LO.InterpretabilityLogic
+
+namespace Formula
+
+variable {α}
+
+
+@[elab_as_elim]
+def cases_neg [DecidableEq α] {C : Formula α → Sort w}
+    (hfalsum : C ⊥)
+    (hatom   : ∀ a : α, C (atom a))
+    (hneg    : ∀ φ : Formula α, C (∼φ))
+    (himp    : ∀ (φ ψ : Formula α), ψ ≠ ⊥ → C (φ ➝ ψ))
+    (hbox    : ∀ (φ : Formula α), C (□φ))
+    (hrhd    : ∀ (φ ψ : Formula α), C (φ ▷ ψ))
+    : (φ : Formula α) → C φ
+  | ⊥       => hfalsum
+  | atom a  => hatom a
+  | □φ      => hbox φ
+  | ∼φ      => hneg φ
+  | φ ➝ ψ  => if e : ψ = ⊥ then e ▸ hneg φ else himp φ ψ e
+  | φ ▷ ψ  => hrhd φ ψ
+
+@[elab_as_elim]
+def rec_neg [DecidableEq α] {C : Formula α → Sort w}
+    (hfalsum : C ⊥)
+    (hatom   : ∀ a : α, C (atom a))
+    (hneg    : ∀ φ : Formula α, C (φ) → C (∼φ))
+    (himp    : ∀ (φ ψ : Formula α), ψ ≠ ⊥ → C φ → C ψ → C (φ ➝ ψ))
+    (hbox    : ∀ (φ : Formula α), C (φ) → C (□φ))
+    (hrhd    : ∀ (φ ψ : Formula α), C (φ) → C (ψ) → C (φ ▷ ψ))
+    : (φ : Formula α) → C φ
+  | ⊥       => hfalsum
+  | atom a  => hatom a
+  | □φ      => hbox φ (rec_neg hfalsum hatom hneg himp hbox hrhd φ)
+  | ∼φ      => hneg φ (rec_neg hfalsum hatom hneg himp hbox hrhd φ)
+  | φ ➝ ψ  =>
+    if e : ψ = ⊥
+    then e ▸ hneg φ (rec_neg hfalsum hatom hneg himp hbox hrhd φ)
+    else himp φ ψ e (rec_neg hfalsum hatom hneg himp hbox hrhd φ) (rec_neg hfalsum hatom hneg himp hbox hrhd ψ)
+  | φ ▷ ψ  => hrhd φ ψ (rec_neg hfalsum hatom hneg himp hbox hrhd φ) (rec_neg hfalsum hatom hneg himp hbox hrhd ψ)
+
+
+def complement : Formula α → Formula α
+  | ∼φ => φ
+  | φ  => ∼φ
+instance : Compl (Formula α) where
+  compl := complement
+
+namespace complement
+
+variable {φ ψ : Formula α}
+
+@[grind] lemma neg_def : -(∼φ) = φ := by induction φ <;> rfl;
+
+@[grind] lemma bot_def : -(⊥ : Formula α) = ∼(⊥) := rfl
+
+@[grind] lemma box_def : -(□φ) = ∼(□φ) := rfl
+
+@[grind] lemma rhd_def : -(φ ▷ ψ) = ∼(φ ▷ ψ) := rfl
+
+@[grind]
+lemma imp_def₁ (hq : ψ ≠ ⊥) : -(φ ➝ ψ) = ∼(φ ➝ ψ) := by
+  suffices complement (φ ➝ ψ) = ∼(φ ➝ ψ) by tauto;
+  unfold complement;
+  split <;> simp_all;
+
+@[grind] lemma imp_def₂ (hq : ψ = ⊥) : -(φ ➝ ψ) = φ := hq ▸ rfl
+
+end complement
+
+end Formula
+
+
+open LO.Entailment in
+instance [DecidableEq α] [Entailment S (Formula α)] {𝓢 : S} [Entailment.Cl 𝓢] : Entailment.ComplEquiv 𝓢 where
+  compl_equiv! {φ} := by
+    induction φ using Formula.cases_neg with
+    | hneg => apply E_symm $ dn
+    | himp φ ψ hψ =>
+      rw [Formula.complement.imp_def₁ hψ];
+      apply E_Id;
+    | hbox | hatom | hfalsum | hrhd => apply E_Id;
+
+
+end LO.InterpretabilityLogic

Foundation/InterpretabilityLogic/Formula/Subformula.lean

@@ -0,0 +1,99 @@
+import Foundation.InterpretabilityLogic.Formula.Basic
+
+namespace LO.InterpretabilityLogic
+
+variable {α} [DecidableEq α] {φ ψ χ : Formula α}
+
+namespace Formula
+
+@[grind]
+def subformulas : Formula α → Finset (Formula α)
+  | atom a => {atom a}
+  | ⊥      => {⊥}
+  | φ ➝ ψ => {φ ➝ ψ} ∪ subformulas φ ∪ subformulas ψ
+  | □φ     => {□φ} ∪ subformulas φ
+  | φ ▷ ψ  => {φ ▷ ψ} ∪ subformulas φ ∪ subformulas ψ
+
+namespace subformulas
+
+@[simp, grind]
+lemma mem_self : φ ∈ φ.subformulas := by induction φ <;> simp_all [subformulas, Finset.mem_union, Finset.mem_singleton]
+
+@[grind ⇒]
+lemma mem_imp (h : (ψ ➝ χ) ∈ φ.subformulas) : ψ ∈ φ.subformulas ∧ χ ∈ φ.subformulas := by
+  induction φ with
+  | himp ψ χ ihψ ihχ
+  | hrhd ψ χ ihψ ihχ => simp_all [subformulas]; grind;
+  | _ => simp_all [subformulas];
+
+@[grind ⇒] lemma mem_neg (h : (∼ψ) ∈ φ.subformulas) : ψ ∈ φ.subformulas := (mem_imp h).1
+
+@[grind ⇒]
+lemma mem_box (h : (□ψ) ∈ φ.subformulas) : ψ ∈ φ.subformulas := by
+  induction φ with
+  | himp ψ χ ihψ ihχ
+  | hrhd ψ χ ihψ ihχ => simp_all [subformulas]; grind;
+  | hbox ψ ihψ => simp_all [subformulas]; grind;
+  | _ => simp_all [subformulas];
+
+@[grind ⇒]
+lemma mem_rhd (h : (ψ ▷ χ) ∈ φ.subformulas) : ψ ∈ φ.subformulas ∧ χ ∈ φ.subformulas := by
+  induction φ with
+  | himp ψ χ ihψ ihχ
+  | hrhd ψ χ ihψ ihχ => simp_all [subformulas]; grind;
+  | _ => simp_all [subformulas];
+
+@[grind ⇒] lemma mem_or (h : (ψ ⋎ χ) ∈ φ.subformulas) : ψ ∈ φ.subformulas ∨ χ ∈ φ.subformulas := by
+  simp only [LukasiewiczAbbrev.or] at h;
+  grind;
+
+@[grind ⇒] lemma mem_and (h : (ψ ⋏ χ) ∈ φ.subformulas) : ψ ∈ φ.subformulas ∧ χ ∈ φ.subformulas := by
+  simp only [LukasiewiczAbbrev.and] at h;
+  grind;
+
+end subformulas
+
+end Formula
+
+
+class FormulaFinset.SubformulaClosed (Φ : FormulaFinset α) where
+  subfml_closed : ∀ φ ∈ Φ, φ.subformulas ⊆ Φ
+
+namespace FormulaFinset.SubformulaClosed
+
+variable {Φ : FormulaFinset α} [Φ.SubformulaClosed]
+
+@[grind ⇒]
+lemma mem_imp (h : φ ➝ ψ ∈ Φ) : φ ∈ Φ ∧ ψ ∈ Φ := by
+  constructor <;>
+  . apply SubformulaClosed.subfml_closed _ h;
+    simp [Formula.subformulas];
+
+@[grind ⇒]
+lemma mem_neg (h : ∼φ ∈ Φ) : φ ∈ Φ := (mem_imp h).1
+
+@[grind ⇒]
+lemma mem_and (h : φ ⋏ ψ ∈ Φ) : φ ∈ Φ ∧ ψ ∈ Φ := by
+  simp only [LukasiewiczAbbrev.and] at h;
+  grind;
+
+@[grind ⇒]
+lemma mem_or (h : φ ⋎ ψ ∈ Φ) : φ ∈ Φ ∨ ψ ∈ Φ := by
+  simp only [LukasiewiczAbbrev.or] at h;
+  grind;
+
+@[grind ⇒]
+lemma mem_box (h : □φ ∈ Φ) : φ ∈ Φ := by
+  apply SubformulaClosed.subfml_closed _ h;
+  simp [Formula.subformulas];
+
+@[grind ⇒]
+lemma mem_rhd (h : φ ▷ ψ ∈ Φ) : φ ∈ Φ ∧ ψ ∈ Φ := by
+  constructor <;>
+  . apply SubformulaClosed.subfml_closed _ h;
+    simp [Formula.subformulas];
+
+end FormulaFinset.SubformulaClosed
+
+
+end LO.InterpretabilityLogic

Foundation/InterpretabilityLogic/LogicSymbol.lean

@@ -12,3 +12,13 @@ attribute [match_pattern] Rhd.rhd
 class InterpretabilityLogicalConnective (F : Type*) extends BasicModalLogicalConnective F, Rhd F
 
 end LO
+
+
+
+open LO
+
+namespace Finset.LO
+
+variable {F : Type*} [DecidableEq F] [InterpretabilityLogicalConnective F]
+
+end Finset.LO

Foundation/InterpretabilityLogic/Veltman/Basic.lean

@@ -10,15 +10,20 @@ open Entailment
 namespace Veltman
 
 structure Frame extends toKripkeFrame : Modal.Kripke.Frame where
-  [F_GL : toKripkeFrame.IsInfiniteGL]
   S : (w : World) → (HRel { v // Rel w v })
-  S_refl  : ∀ w, IsRefl _ (S w)
-  S_trans : ∀ w, IsTrans _ (S w)
 
-instance {F :  Frame} : F.IsInfiniteGL := F.F_GL
+namespace Frame
 
-class Frame.IsIL (F : Frame) where
+class IsCL (F : Frame) extends F.IsInfiniteGL where
+  S_refl  : ∀ w, IsRefl _ (F.S w)
+  S_trans : ∀ w, IsTrans _ (F.S w)
+export IsCL (S_refl S_trans)
+
+class IsIL (F : Frame) extends F.IsCL where
   S_IL : ∀ w : F.World, ∀ x y : { v // w ≺ v }, (x.1 ≺ y.1) → (F.S w x y)
+export IsIL (S_IL)
+
+end Frame
 
 abbrev FrameClass := Set (Frame)
 
@@ -43,7 +48,7 @@ def Satisfies (M : Veltman.Model) (x : M.World) : Formula ℕ → Prop
   | ⊥  => False
   | φ ➝ ψ => (Satisfies M x φ) ➝ (Satisfies M x ψ)
   | □φ   => ∀ y, x ≺ y → (Satisfies M y φ)
-  | φ ▷ ψ => ∀ y, (Rxy : (x ≺ y)) → Satisfies M y φ → (∃ z : { v // x ≺ v }, M.S x ⟨y, Rxy⟩ z ∧ Satisfies M z ψ)
+  | φ ▷ ψ => ∀ y : { v // x ≺ v}, Satisfies M y φ → (∃ z : { v // x ≺ v }, M.S x y z ∧ Satisfies M z ψ)
 
 
 namespace Satisfies
@@ -121,15 +126,15 @@ lemma iff_subst_self {x : F.World} (s : Substitution ℕ) :
       exact hφ;
   | hrhd φ ψ ihφ ihψ =>
     constructor;
-    . intro h y Rxy hy;
-      obtain ⟨⟨z, Rxz⟩, Sxyz, hz₂⟩ := h _ Rxy $ ihφ.mpr hy;
+    . intro h y hy;
+      obtain ⟨⟨z, Rxz⟩, Sxyz, hz₂⟩ := h y $ ihφ.mpr hy;
       use ⟨z, Rxz⟩;
       constructor;
       . assumption;
       . apply ihψ.mp;
         assumption;
-    . intro h y Rxy hy;
-      obtain ⟨⟨z, Rxz⟩, Sxyz, hz₂⟩ := h _ Rxy $ ihφ.mp hy;
+    . intro h y hy;
+      obtain ⟨⟨z, Rxz⟩, Sxyz, hz₂⟩ := h y $ ihφ.mp hy;
       use ⟨z, Rxz⟩;
       constructor;
       . assumption;
@@ -233,40 +238,42 @@ protected lemma axiomK : M ⊧ (Modal.Axioms.K φ ψ)  := by
   replace hp := hp x Rxy;
   exact hpq hp;
 
-protected lemma axiomJ1 : M ⊧ Axioms.J1 φ ψ := by
-  intro x h y Rxy hy;
-  use ⟨y, Rxy⟩;
+protected lemma axiomJ1 [M.IsCL] : M ⊧ Axioms.J1 φ ψ := by
+  intro x h y hy;
+  use y;
   constructor;
-  . apply M.toVeltmanFrame.S_refl x |>.refl;
-  . exact h y Rxy hy;
-
-protected lemma axiomJ2 : M ⊧ Axioms.J2 φ ψ χ := by
-  intro x h₁ h₂ y Rxy hy;
-  obtain ⟨⟨u, Rxu⟩, Sxyu, hu⟩ := h₁ _ Rxy hy;
-  obtain ⟨⟨v, Ruv⟩, Sxuv, hv⟩ := h₂ u Rxu hu;
+  . apply M.S_refl x |>.refl;
+  . apply h;
+    . exact y.2;
+    . exact hy;
+
+protected lemma axiomJ2 [M.IsCL] : M ⊧ Axioms.J2 φ ψ χ := by
+  intro x h₁ h₂ y hy;
+  obtain ⟨⟨u, Rxu⟩, Sxyu, hu⟩ := h₁ y hy;
+  obtain ⟨⟨v, Ruv⟩, Sxuv, hv⟩ := h₂ ⟨u, Rxu⟩ hu;
   use ⟨v, Ruv⟩;
   constructor;
-  . apply M.toVeltmanFrame.S_trans x |>.trans;
+  . apply M.S_trans x |>.trans;
     . exact Sxyu;
     . exact Sxuv;
   . assumption;
 
 protected lemma axiomJ3 : M ⊧ Axioms.J3 φ ψ χ := by
-  intro x h₁ h₂ y Rxy h₃;
+  intro x h₁ h₂ y h₃;
   rcases Veltman.Satisfies.or_def.mp h₃ with (h₃ | h₃);
-  . obtain ⟨⟨u, Rxu⟩, Sxyu, hu⟩ := h₁ _ Rxy h₃; use ⟨u, Rxu⟩;
-  . obtain ⟨⟨u, Rxu⟩, Sxyu, hu⟩ := h₂ _ Rxy h₃; use ⟨u, Rxu⟩;
+  . obtain ⟨⟨u, Rxu⟩, Sxyu, hu⟩ := h₁ y h₃; use ⟨u, Rxu⟩;
+  . obtain ⟨⟨u, Rxu⟩, Sxyu, hu⟩ := h₂ y h₃; use ⟨u, Rxu⟩;
 
 protected lemma axiomJ4 : M ⊧ Axioms.J4 φ ψ := by
   intro x h₁ h₂;
   obtain ⟨y, Rxy, hy⟩ := Satisfies.dia_def.mp h₂;
-  obtain ⟨⟨z, Rxz⟩, Sxyz, hz⟩ := h₁ _ Rxy hy;
+  obtain ⟨⟨z, Rxz⟩, Sxyz, hz⟩ := h₁ ⟨y, Rxy⟩ hy;
   apply Satisfies.dia_def.mpr;
   use z;
   tauto;
 
-protected lemma axiomJ5 [M.toVeltmanFrame.IsIL] : M ⊧ Axioms.J5 φ := by
-  intro x y Rxy h;
+protected lemma axiomJ5 [M.IsIL] : M ⊧ Axioms.J5 φ := by
+  rintro x ⟨y, Rxy⟩ h;
   obtain ⟨z, Ryz, hz⟩ := Satisfies.dia_def.mp h;
   use ⟨z, M.toKripkeFrame.trans Rxy Ryz⟩;
   constructor;
@@ -352,11 +359,11 @@ lemma kripkeLift {φ : Modal.Formula _} : F ⊧ ↑φ ↔ F.toKripkeFrame ⊧ φ
 
 @[simp] protected lemma axiomK : F ⊧ (Modal.Axioms.K φ ψ) := fun _ ↦ ValidOnModel.axiomK
 
-@[simp] protected lemma axiomL : F ⊧ (Modal.Axioms.L φ) := ValidOnFrame.subst (s := λ _ => φ) $ kripkeLift.mpr $ Modal.Kripke.validate_AxiomL_of_trans_cwf
+@[simp] protected lemma axiomL [F.IsInfiniteGL] : F ⊧ (Modal.Axioms.L φ) := ValidOnFrame.subst (s := λ _ => φ) $ kripkeLift.mpr $ Modal.Kripke.validate_AxiomL_of_trans_cwf
 
-@[simp] protected lemma axiomJ1 : F ⊧ Axioms.J1 φ ψ := fun _ ↦ ValidOnModel.axiomJ1
+@[simp] protected lemma axiomJ1 [F.IsCL] : F ⊧ Axioms.J1 φ ψ := fun _ ↦ ValidOnModel.axiomJ1
 
-@[simp] protected lemma axiomJ2 : F ⊧ Axioms.J2 φ ψ χ := fun _ ↦ ValidOnModel.axiomJ2
+@[simp] protected lemma axiomJ2 [F.IsCL] : F ⊧ Axioms.J2 φ ψ χ := fun _ ↦ ValidOnModel.axiomJ2
 
 @[simp] protected lemma axiomJ3 : F ⊧ Axioms.J3 φ ψ χ := fun _ ↦ ValidOnModel.axiomJ3
 

Foundation/InterpretabilityLogic/Veltman/Hilbert.lean

@@ -77,18 +77,6 @@ lemma weakerThan_of_subset_frameClass
   apply Sound.sound (𝓜 := C₁) hφ;
   apply hC hF;
 
-lemma validates_CL_axioms_union (hV : C ⊧* Ax) : C ⊧* CL.axioms ∪ Ax := by
-  constructor;
-  rintro φ ((rfl | rfl | rfl | rfl | rfl | rfl) | hφ);
-  . intro _ _; apply ValidOnFrame.axiomK;
-  . intro _ _; apply ValidOnFrame.axiomL;
-  . intro _ _; apply ValidOnFrame.axiomJ1;
-  . intro _ _; apply ValidOnFrame.axiomJ2;
-  . intro _ _; apply ValidOnFrame.axiomJ3;
-  . intro _ _; apply ValidOnFrame.axiomJ4;
-  . apply hV.models;
-    assumption;
-
 end Veltman
 
 end LO.InterpretabilityLogic