diff --git a/Foundation.lean b/Foundation.lean index 1871025a0..9beb92359 100644 --- a/Foundation.lean +++ b/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 diff --git a/Foundation/InterpretabilityLogic/Formula/Basic.lean b/Foundation/InterpretabilityLogic/Formula/Basic.lean index c90190f90..c2b26b75d 100644 --- a/Foundation/InterpretabilityLogic/Formula/Basic.lean +++ b/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 α] diff --git a/Foundation/InterpretabilityLogic/Formula/Complement.lean b/Foundation/InterpretabilityLogic/Formula/Complement.lean new file mode 100644 index 000000000..a1dc7a5d8 --- /dev/null +++ b/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 diff --git a/Foundation/InterpretabilityLogic/Formula/Subformula.lean b/Foundation/InterpretabilityLogic/Formula/Subformula.lean new file mode 100644 index 000000000..f64f8f272 --- /dev/null +++ b/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 diff --git a/Foundation/InterpretabilityLogic/LogicSymbol.lean b/Foundation/InterpretabilityLogic/LogicSymbol.lean index 6fbe791d0..c340bf845 100644 --- a/Foundation/InterpretabilityLogic/LogicSymbol.lean +++ b/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 diff --git a/Foundation/InterpretabilityLogic/Veltman/Basic.lean b/Foundation/InterpretabilityLogic/Veltman/Basic.lean index 76382d2eb..03e0a81fb 100644 --- a/Foundation/InterpretabilityLogic/Veltman/Basic.lean +++ b/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 diff --git a/Foundation/InterpretabilityLogic/Veltman/Hilbert.lean b/Foundation/InterpretabilityLogic/Veltman/Hilbert.lean index c56c30d91..c7e20e21f 100644 --- a/Foundation/InterpretabilityLogic/Veltman/Hilbert.lean +++ b/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 diff --git a/Foundation/InterpretabilityLogic/Veltman/Logic/CL.lean b/Foundation/InterpretabilityLogic/Veltman/Logic/CL.lean index b7db1d9e5..aa0d67276 100644 --- a/Foundation/InterpretabilityLogic/Veltman/Logic/CL.lean +++ b/Foundation/InterpretabilityLogic/Veltman/Logic/CL.lean @@ -3,18 +3,30 @@ import Foundation.InterpretabilityLogic.Veltman.Hilbert namespace LO.InterpretabilityLogic open Veltman - +open Formula.Veltman namespace Veltman -protected abbrev FrameClass.CL : FrameClass := Set.univ +protected abbrev FrameClass.CL : FrameClass := { F | F.IsCL } abbrev trivialFrame : Veltman.Frame where toKripkeFrame := Modal.Kripke.blackpoint S _ _ _ := True + +instance : Veltman.trivialFrame.IsCL where S_refl _ := ⟨by tauto⟩ S_trans _ := ⟨by tauto⟩ +lemma validates_CL_axioms_union {F : Veltman.Frame} [F.IsCL] : F ⊧* CL.axioms := by + constructor; + rintro φ (rfl | rfl | rfl | rfl | rfl | rfl); + . apply ValidOnFrame.axiomK; + . apply ValidOnFrame.axiomL; + . apply ValidOnFrame.axiomJ1; + . apply ValidOnFrame.axiomJ2; + . apply ValidOnFrame.axiomJ3; + . apply ValidOnFrame.axiomJ4; + end Veltman @@ -22,14 +34,15 @@ namespace CL instance Veltman.sound : Sound InterpretabilityLogic.CL FrameClass.CL := instSound_of_validates_axioms $ by constructor; - intro φ hφ; - have := (show CL.axioms ∪ ∅ = CL.axioms by simp) ▸ validates_CL_axioms_union (Ax := ∅) (C := FrameClass.CL) ⟨by tauto⟩; - apply this.models; + intro φ hφ F hF; + simp only [Set.mem_setOf_eq] at hF; + apply validates_CL_axioms_union.models; assumption; instance : Entailment.Consistent InterpretabilityLogic.CL := consistent_of_sound_frameclass FrameClass.CL $ by use Veltman.trivialFrame; - simp; + apply Set.mem_setOf_eq.mpr; + infer_instance; end CL diff --git a/Foundation/InterpretabilityLogic/Veltman/Logic/IL/Completeness.lean b/Foundation/InterpretabilityLogic/Veltman/Logic/IL/Completeness.lean new file mode 100644 index 000000000..67301c7e6 --- /dev/null +++ b/Foundation/InterpretabilityLogic/Veltman/Logic/IL/Completeness.lean @@ -0,0 +1,381 @@ +import Foundation.InterpretabilityLogic.Veltman.Logic.IL.Soundness +import Foundation.InterpretabilityLogic.Formula.Subformula +import Foundation.InterpretabilityLogic.Formula.Complement +import Foundation.Propositional.CMCF + +namespace LO.InterpretabilityLogic + +variable {α : Type*} [DecidableEq α] +variable {S} [Entailment S (Formula α)] +variable {𝓢 : S} + +open Modal (Kripke.Frame Kripke.Model) + +namespace FormulaFinset + +class Adequate (Φ : FormulaFinset α) extends Φ.SubformulaClosed where + compl_closed : ∀ φ ∈ Φ, -φ ∈ Φ + mem_top_rhd_top : ⊤ ▷ ⊤ ∈ Φ + mem_part₁ : ∀ {φ ψ}, (φ ▷ ψ) ∈ Φ → (□-φ) ∈ Φ ∧ (□-ψ) ∈ Φ + mem_part₂ : ∀ {φ₁ ψ₁ φ₂ ψ₂}, + (φ₁ ▷ ψ₁) ∈ Φ → (φ₂ ▷ ψ₂) ∈ Φ → + ∀ ξ₁ ∈ [φ₁, ψ₁, φ₂, ψ₂], + ∀ ξ₂ ∈ [φ₁, ψ₁, φ₂, ψ₂], + (ξ₁ ▷ ξ₂) ∈ Φ + +attribute [simp] Adequate.mem_top_rhd_top + +namespace Adequate + +variable {Φ : FormulaFinset α} [Φ.Adequate] + +@[grind ⇒] lemma mem_imp (h : φ ➝ ψ ∈ Φ) : φ ∈ Φ ∧ ψ ∈ Φ := SubformulaClosed.mem_imp h +@[grind ⇒] lemma mem_box (h : □φ ∈ Φ) : φ ∈ Φ := SubformulaClosed.mem_box h +@[grind ⇒] lemma mem_rhd (h : φ ▷ ψ ∈ Φ) : φ ∈ Φ ∧ ψ ∈ Φ := SubformulaClosed.mem_rhd h + +end Adequate + +end FormulaFinset + + + +section + +def AdequateSet (α) [DecidableEq α] := { Φ : FormulaFinset α // Φ.Adequate } + +namespace AdequateSet + +variable {Φ : AdequateSet α} + +@[grind ⇒] lemma mem_imp (h : φ ➝ ψ ∈ Φ.1) : φ ∈ Φ.1 ∧ ψ ∈ Φ.1 := Φ.2.mem_imp h +@[grind ⇒] lemma mem_box (h : □φ ∈ Φ.1) : φ ∈ Φ.1 := Φ.2.mem_box h +@[grind ⇒] lemma mem_rhd (h : φ ▷ ψ ∈ Φ.1) : φ ∈ Φ.1 ∧ ψ ∈ Φ.1 := Φ.2.mem_rhd h + +end AdequateSet + + +open Finset.LO +open LO.ComplementMaximalConsistentFinset + +-- def MaximalConsistentSet (𝓢 : S) (Φ : AdequateSet α) := { Ψ : FormulaFinset α // Ψ ⊆ Φ.1 ∧ Ψ.Maximal 𝓢 ∧ Ψ.Consistent 𝓢 } + +variable {Φ : AdequateSet α} {Γ Δ Θ : { Γ : ComplementMaximalConsistentFinset 𝓢 Φ.1 // Γ.1 ⊆ Φ.1 }} + +structure ILSuccessor (Γ Δ : { Γ : ComplementMaximalConsistentFinset 𝓢 Φ.1 // Γ.1 ⊆ Φ.1 }) : Prop where + prop1 : (∀ φ ∈ Γ.1.1.prebox, φ ∈ Δ.1 ∧ □φ ∈ Δ.1) + prop2 : (∃ φ ∈ Δ.1.1.prebox, □φ ∉ Γ.1) +infix:80 " ≺ " => ILSuccessor + +structure ILCriticalSuccessor (χ : { χ : Formula α // χ ∈ Φ.1}) (Γ Δ : { Γ : ComplementMaximalConsistentFinset 𝓢 Φ.1 // Γ.1 ⊆ Φ.1 }) extends Γ ≺ Δ where + prop3 : ∀ φ, φ ▷ χ.1 ∈ Γ.1 → -φ ∈ Δ.1 ∧ □-φ ∈ Δ.1 +notation Γ:max " ≺[" χ "] " Δ:max => ILCriticalSuccessor χ Γ Δ + +lemma claim1 (hΓΔ : Γ ≺[χ] Δ) (hΔΘ : Δ ≺ Θ) : Γ ≺[χ] Θ where + prop1 := by + intro φ hφ; + apply hΔΘ.prop1 φ; + simpa using hΓΔ.prop1 _ hφ |>.2; + prop2 := by + rcases hΔΘ.prop2 with ⟨φ, hφ, h⟩; + use φ; + constructor; + . assumption; + . contrapose! h; + apply hΓΔ.prop1 φ ?_ |>.2; + simpa; + prop3 := by + intro φ hφ; + rcases hΓΔ.prop3 φ hφ with ⟨h₁, h₂⟩; + apply hΔΘ.prop1; + simpa; + +open LO.InterpretabilityLogic.Entailment +open LO.Entailment +open LO.Modal.Entailment + +omit [DecidableEq α] in +lemma claim2_1 [Entailment.IL 𝓢] : 𝓢 ⊢ (φ ⋎ ◇φ) ▷ φ := by + apply (J3 (𝓢 := 𝓢)) ⨀ ?_ ⨀ ?_; + . -- TODO: 𝓢 ⊢ φ ▷ φ + apply J1 (𝓢 := 𝓢) ⨀ (nec! C!_id); + . apply J5; + +lemma claim2_2 [Entailment.IL 𝓢] : 𝓢 ⊢ φ ▷ (φ ⋏ □(∼φ)) := by + apply rhd_trans ?_ claim2_1; + apply rhd_of_lc; + apply nec!; + suffices 𝓢 ⊢ ∼◇(φ ⋏ □(∼φ)) ➝ □(∼φ) by cl_prover [this] + apply C!_replace (CN!_of_CN!_left INLNM) axiomL!; + apply box_regularity!; + cl_prover; + +lemma claim3 [Entailment.IL 𝓢] (h₁ : ∼(φ ▷ χ.1) ∈ Γ.1) : ∃ Δ, (Γ ≺[χ] Δ) ∧ φ ∈ Δ.1 := by + have : (φ ▷ χ.1) ∈ Φ.1 := Φ.2.compl_closed (∼(φ ▷ χ.1)) $ Γ.2 h₁; + have : □-φ ∈ Φ.1 := Φ.2.mem_part₁ this |>.1; + have : □-φ ∉ Γ.1 := by + by_contra hC; + replace hC : Γ *⊢[𝓢] □-φ := ComplementMaximalConsistentFinset.membership_iff (by simpa) |>.mp hC; + apply ComplementMaximalConsistentFinset.iff_mem_compl (by simpa) |>.mpr $ Formula.complement.rhd_def ▸ h₁; + apply ComplementMaximalConsistentFinset.membership_iff (by simpa) |>.mpr; + apply (show Γ *⊢[𝓢] □(φ ➝ χ.1) ➝ (φ ▷ χ.1) by exact Entailment.Context.of! $ J1) ⨀ ?_; + apply (Entailment.Context.of! $ ?_) ⨀ hC; + apply box_regularity!; + apply C!_trans $ C_of_E_mpr! $ compl_equiv; + exact CNC!; + let Ξ₁ := Γ.1.1.prebox; + let Ξ₂ := (Γ.1.1.preimage (λ ξ => ξ ▷ χ.1) (by simp)); + let Δ₁ : FormulaFinset _ := {φ, □-φ} + let Δ₂ : FormulaFinset _ := Ξ₁ + let Δ₃ : FormulaFinset _ := Ξ₁.box + let Δ₄ : FormulaFinset _ := Ξ₂.image (λ ξ => -ξ) + let Δ₅ : FormulaFinset _ := Ξ₂.image (λ ξ => □(-ξ)) + let Δ : FormulaFinset _ := Δ₁ ∪ Δ₂ ∪ Δ₃ ∪ Δ₄ ∪ Δ₅ + have Δ_consis : Consistent 𝓢 Δ := by + by_contra!; + obtain ⟨Θ, hΘ₁, H⟩ := def_inconsistent.mp this; + replace H : Δ *⊢[𝓢] ⊥ := Context.weakening! hΘ₁ H; + rw [show Δ = ((Δ₂ ∪ Δ₃) ∪ Δ₁ ∪ (Δ₄ ∪ Δ₅)) by grind] at H; + replace H : 𝓢 ⊢ (Δ₂ ∪ Δ₃).conj ⋏ Δ₁.conj ➝ Finset.conj (Δ₄ ∪ Δ₅) ➝ ⊥ := + C!_trans CKFconjFconjUnion! $ CK!_iff_CC!.mp $ C!_trans CKFconjFconjUnion! $ FConj_DT.mpr H; + replace H : 𝓢 ⊢ (Δ₂ ∪ Δ₃).conj ➝ (Δ₁.conj ➝ (∼(Δ₄ ∪ Δ₅).conj)) := by cl_prover [H]; + replace H : 𝓢 ⊢ □Δ₂.conj ➝ □(Δ₁.conj ➝ ∼(Δ₄ ∪ Δ₅).conj) := C!_trans ?_ $ box_regularity! H; + replace H : 𝓢 ⊢ □Δ₂.conj ➝ Δ₁.conj ▷ ∼(Δ₄ ∪ Δ₅).conj := C!_trans H J1; + replace H : 𝓢 ⊢ □Δ₂.conj ➝ ((φ ⋏ □(∼φ)) ▷ (Ξ₂.disj ⋎ ◇Ξ₂.disj)) := by sorry; + replace H : 𝓢 ⊢ □Δ₂.conj ➝ (φ ▷ Ξ₂.disj) := by + have H₁ : 𝓢 ⊢ ((φ ⋏ □(∼φ)) ▷ (Ξ₂.disj ⋎ ◇Ξ₂.disj)) ➝ ((Ξ₂.disj ⋎ ◇Ξ₂.disj) ▷ Ξ₂.disj) ➝ ((φ ⋏ □(∼φ)) ▷ Ξ₂.disj) := J2 + have H₂ : 𝓢 ⊢ (φ ▷ (φ ⋏ □(∼φ))) ➝ ((φ ⋏ □(∼φ)) ▷ Ξ₂.disj) ➝ (φ ▷ Ξ₂.disj) := J2 + have H₃ : 𝓢 ⊢ (Ξ₂.disj ⋎ ◇Ξ₂.disj) ▷ Ξ₂.disj := claim2_1 + have H₄ : 𝓢 ⊢ φ ▷ (φ ⋏ □(∼φ)) := claim2_2; + cl_prover [H, H₁, H₂, H₃, H₄] + replace H : 𝓢 ⊢ (□Δ₂.conj ⋏ (Ξ₂.image (λ ξ => ξ ▷ χ.1)).conj) ➝ (φ ▷ χ.1) := by + have H₁ : 𝓢 ⊢ (Ξ₂.image (λ ξ => ξ ▷ χ.1)).conj ➝ (Ξ₂.disj ▷ χ) := by sorry + have H₂ : 𝓢 ⊢ (φ ▷ Ξ₂.disj) ➝ (Ξ₂.disj ▷ χ) ➝ (φ ▷ χ) := J2; + cl_prover [H, H₁, H₂]; + replace H := H ⨀ ?_; + . sorry; + . sorry; + . sorry; + obtain ⟨Ω, hΩ⟩ : ∃ Ω : ComplementMaximalConsistentFinset 𝓢 Φ.1, Δ ⊆ Ω.1 := ComplementMaximalConsistentFinset.lindenbaum Δ_consis; + sorry; + /- + use ⟨Δ, by sorry⟩; + constructor; + . exact { + prop1 := by + intro ψ hψ; + simp at hψ; + constructor; + . apply hΔ; + simp only [Finset.mem_union, Δ₀]; + left; left; left; right; + simpa; + . apply hΔ; + simp only [Finset.mem_union, Δ₀]; + left; left; right; + simpa; + prop2 := by + use (-φ); + constructor; + . suffices □-φ ∈ Δ.1 by simpa; + apply hΔ; + simp [Δ₀]; + . assumption; + prop3 := by + intro ψ hψ; + constructor; + . apply hΔ; + simp only [Finset.mem_union, Δ₀]; + left; right; + suffices ∃ ξ, (ξ ▷ χ.1 ∈ Γ.1) ∧ -ξ = -ψ by simpa; + use ψ; + . apply hΔ; + simp only [Finset.mem_union, Δ₀]; + right; + suffices ∃ ξ, (ξ ▷ χ.1 ∈ Γ.1) ∧ -ξ = -ψ by simpa; + use ψ; + } + . apply hΔ; + simp [Δ₀]; + -/ + +lemma claim4 (h₁ : (φ ▷ ψ) ∈ Γ.1) (h₂ : φ ∈ Δ.1) (h₃ : Γ ≺[χ] Δ) + : ∃ Δ', (Γ ≺[χ] Δ') ∧ ψ ∈ Δ'.1 ∧ □(-ψ) ∈ Δ'.1 := by + have : □-ψ ∉ Γ.1 := by + by_contra hC; + sorry; + let Δ₀ : FormulaFinset _ := + {ψ, □-ψ} ∪ + Γ.1.1.prebox ∪ + Γ.1.1.prebox.box ∪ + ((Γ.1.1.preimage (λ ξ => ξ ▷ χ) (by simp)) |>.image (λ ξ => -ξ)) ∪ + ((Γ.1.1.preimage (λ ξ => ξ ▷ χ) (by simp)) |>.image (λ ξ => □-ξ)) + + have Δ₀_consis : Consistent 𝓢 Δ := by sorry; + obtain ⟨Δ, hΔ⟩ : ∃ Δ : ComplementMaximalConsistentFinset 𝓢 Φ.1, Δ₀ ⊆ Δ.1 := by + sorry; + use ⟨Δ, by sorry⟩; + refine ⟨?_, ?_, ?_⟩; + . exact { + prop1 := by + intro ψ hψ; + simp at hψ; + constructor; + . apply hΔ; + simp only [Finset.mem_union, Δ₀]; + left; left; left; right; + simpa; + . apply hΔ; + simp only [Finset.mem_union, Δ₀]; + left; left; right; + simpa; + prop2 := by + use (-ψ); + constructor; + . suffices □-ψ ∈ Δ.1 by simpa; + apply hΔ; + simp [Δ₀]; + . assumption; + prop3 := by + intro ψ hψ; + constructor; + . apply hΔ; + simp only [Finset.mem_union, Δ₀]; + left; right; + suffices ∃ ξ, (ξ ▷ χ.1 ∈ Γ.1) ∧ -ξ = -ψ by simpa; + use ψ; + . apply hΔ; + simp only [Finset.mem_union, Δ₀]; + right; + suffices ∃ ξ, (ξ ▷ χ.1 ∈ Γ.1) ∧ -ξ = -ψ by simpa; + use ψ; + } + . apply hΔ; simp [Δ₀]; + . apply hΔ; simp [Δ₀]; + +end + +open Veltman + +namespace Veltman + +variable {α : Type*} [DecidableEq α] +variable [Entailment S (Formula ℕ)] +variable {Φ : AdequateSet _} {𝓢 : S} {Γ : { Γ : ComplementMaximalConsistentFinset 𝓢 Φ.1 // Γ.1 ⊆ Φ.1 }} + +protected inductive ILMiniCanonicalModel.IsWorld (Γ : { Γ : ComplementMaximalConsistentFinset 𝓢 Φ.1 // Γ.1 ⊆ Φ.1 }) + : { Γ : ComplementMaximalConsistentFinset 𝓢 Φ.1 // Γ.1 ⊆ Φ.1 } × List { φ // φ ∈ Φ.1 } → Prop + | i₁ : ILMiniCanonicalModel.IsWorld Γ ⟨Γ, []⟩ + | i₂ {Δ Δ'} {τ} : ILMiniCanonicalModel.IsWorld Γ ⟨Δ, τ⟩ → Δ < Δ' → ILMiniCanonicalModel.IsWorld Γ ⟨Δ', τ⟩ + | i₃ {Δ Δ'} {τ χ} : ILMiniCanonicalModel.IsWorld Γ ⟨Δ, τ⟩ → Δ ≺[χ] Δ' → ILMiniCanonicalModel.IsWorld Γ ⟨Δ', (τ ++ [χ])⟩ + +def ILMiniCanonicalModel (Γ : { Γ : ComplementMaximalConsistentFinset 𝓢 Φ.1 // Γ.1 ⊆ Φ.1 }) : Veltman.Model where + toKripkeFrame := { + World := { P // ILMiniCanonicalModel.IsWorld Γ P } + world_nonempty := ⟨⟨(Γ, []), ILMiniCanonicalModel.IsWorld.i₁⟩⟩ + Rel X Y := ∃ χ, X.1.1 ≺[χ] Y.1.1 ∧ (∃ τ, Y.1.2 = X.1.2 ++ [χ] ++ τ) + } + S X U V := + X ≺ U.1 ∧ + X ≺ V.1 ∧ + (∃ χ, (∃ τ, U.1.1.2 = X.1.2 ++ [χ] ++ τ) ∧ (∃ τ, V.1.1.2 = X.1.2 ++ [χ] ++ τ)) + Val X p := (.atom p) ∈ X.1.1.1 + +instance : (ILMiniCanonicalModel Γ).IsFiniteGL where + trans X Y Z := by + rintro ⟨χ₁, RXY, ⟨τ₁, hτ₁⟩⟩ ⟨χ₂, RYZ, ⟨τ₂, hτ₂⟩⟩; + use χ₁; + constructor; + . exact claim1 RXY RYZ.1; + . use τ₁ ++ [χ₂] ++ τ₂; + simp [hτ₂, hτ₁]; + irrefl := by + rintro _ ⟨_, _, ⟨_, hτ⟩⟩; + simp at hτ; + world_finite := by + simp [ILMiniCanonicalModel]; + sorry + +instance : (ILMiniCanonicalModel Γ).IsIL where + S_refl X := by + constructor; + rintro ⟨U, RXU⟩; + refine ⟨RXU, RXU, ?_⟩; + . rcases RXU with ⟨χ, RχXU, ⟨τ, hτ⟩⟩; + tauto; + S_trans X := by + constructor; + rintro ⟨U, RXU⟩ ⟨V, RXV⟩ ⟨W, RXW⟩ ⟨_, _, ⟨χ₁, ⟨⟨τ₁₁, hτ₁₁⟩, ⟨τ₁₂, hτ₁₂⟩⟩⟩⟩ ⟨_, _, ⟨χ₂, ⟨τ₂₁, hτ₂₁⟩, ⟨τ₂₂, hτ₂₂⟩⟩⟩; + refine ⟨RXU, RXW, ?_⟩; + simp_all; + S_IL := by + rintro X ⟨U, RXU⟩ ⟨V, RXV⟩ ⟨_, _, ⟨_, _⟩⟩; + refine ⟨RXU, RXV, ?_⟩; + rcases RXU with ⟨ξ, _, ⟨_, _⟩⟩; + use ξ; + simp_all; + +instance : (ILMiniCanonicalModel Γ).IsFiniteIL where + +open Formula.Veltman + +lemma ILMiniCanonicalModel.truthlemma [Entailment.IL 𝓢] {X : ILMiniCanonicalModel Γ} (hφ : φ ∈ Φ.1) : X ⊧ φ ↔ φ ∈ X.1.1.1 := by + induction φ generalizing X with + | hfalsum => sorry; + | hatom a => tauto; + | himp φ ψ ihφ ihψ => + suffices φ ∈ X.1.1.1 → ψ ∈ X.1.1.1 ↔ φ ➝ ψ ∈ X.1.1.1 by simpa [Satisfies, (ihφ (X := X) (by grind)), ihψ (X := X) (by grind)]; + sorry; + | hbox φ ih => + have := ih (X := X) (by grind); + sorry; + | hrhd φ ψ ihφ ihψ => + let ψ : { χ // χ ∈ Φ.1} := ⟨ψ, by grind⟩; + suffices (∀ U : {V // X ≺ V}, U.1 ⊧ φ → ∃ V : {V // X ≺ V}, (ILMiniCanonicalModel Γ).S X U V ∧ V.1 ⊧ ψ.1) ↔ φ ▷ ψ ∈ X.1.1.1 by tauto + constructor; + . contrapose!; + intro h; + replace h : ∼(φ ▷ ψ) ∈ X.1.1.1 := by sorry; + obtain ⟨Δ, hΔ₁, hΔ₂⟩ := claim3 h; + use ⟨⟨⟨Δ, X.1.2 ++ [ψ]⟩, IsWorld.i₃ X.2 hΔ₁⟩, ⟨ψ, by simpa⟩⟩; + constructor; + . apply ihφ (by grind) |>.mpr; + simpa; + . rintro V ⟨_, ⟨χ, hχXV, _⟩, h⟩; + apply ihψ (by grind) |>.not.mpr; + have := hχXV.prop3 χ (by sorry) |>.1; + sorry; + . rintro h ⟨U, ⟨χ, hχXU, τ, eU₂⟩⟩ hU; + replace hU := ihφ (by grind) |>.mp hU; + obtain ⟨Δ, hΔ₁, hΔ₂, hΔ₃⟩ := claim4 h hU hχXU; + use ⟨⟨⟨Δ, X.1.2 ++ [χ]⟩, IsWorld.i₃ X.2 hΔ₁⟩, ⟨χ, by simpa⟩⟩; + constructor; + . refine ⟨?_, ?_, ?_⟩; + . use χ; tauto; + . use χ; simpa; + . use χ; + constructor; + . use τ; + . use []; simp; + . apply ihψ (by grind) |>.mpr; + simpa; + +end Veltman + +open Formula.Veltman in +instance IL.Veltman.finite_complete : Complete InterpretabilityLogic.IL Veltman.FrameClass.FiniteIL := by + constructor; + intro φ; + contrapose! + intro hφ; + apply not_validOnFrameClass_of_exists_model_world; + let Φ : AdequateSet ℕ := ⟨{-φ}, by sorry⟩ + obtain ⟨Γ, hΓ⟩ : ∃ Γ : ComplementMaximalConsistentFinset (InterpretabilityLogic.IL) Φ.1, {-φ} ⊆ Γ.1 := ComplementMaximalConsistentFinset.lindenbaum (by sorry) + use ILMiniCanonicalModel ⟨Γ, by sorry⟩, ⟨⟨⟨Γ, _⟩, []⟩, ILMiniCanonicalModel.IsWorld.i₁⟩; + constructor; + . apply Set.mem_setOf_eq.mpr; + infer_instance; + . apply ILMiniCanonicalModel.truthlemma (by sorry) |>.not.mpr; + simp; + sorry; + +end LO.InterpretabilityLogic diff --git a/Foundation/InterpretabilityLogic/Veltman/Logic/IL.lean b/Foundation/InterpretabilityLogic/Veltman/Logic/IL/Soundness.lean similarity index 62% rename from Foundation/InterpretabilityLogic/Veltman/Logic/IL.lean rename to Foundation/InterpretabilityLogic/Veltman/Logic/IL/Soundness.lean index 7edbf3a42..6c534cbb8 100644 --- a/Foundation/InterpretabilityLogic/Veltman/Logic/IL.lean +++ b/Foundation/InterpretabilityLogic/Veltman/Logic/IL/Soundness.lean @@ -9,6 +9,12 @@ namespace Veltman protected abbrev FrameClass.IL : FrameClass := { F | F.IsIL } + +protected class Frame.IsFiniteIL (F : Veltman.Frame) extends F.IsIL, F.IsFinite where + +protected abbrev FrameClass.FiniteIL : FrameClass := { F | F.IsFiniteIL } + + instance : Veltman.trivialFrame.IsIL where S_IL _ _ _ := by simp; @@ -18,13 +24,13 @@ end Veltman namespace IL instance Veltman.sound : Sound InterpretabilityLogic.IL FrameClass.IL := instSound_of_validates_axioms $ by - rw [(show IL.axioms = CL.axioms ∪ {(InterpretabilityLogic.Axioms.J5 (.atom 0))} by simp)]; - apply validates_CL_axioms_union; constructor; - suffices FrameClass.IL ⊧ Axioms.J5 (Formula.atom 0) by simpa; - intro F hF; - simp only [Set.mem_setOf_eq] at hF; - apply Formula.Veltman.ValidOnFrame.axiomJ5; + rintro φ (rfl | hφ) F hF; + . simp only [Set.mem_setOf_eq] at hF; + apply Formula.Veltman.ValidOnFrame.axiomJ5; + . simp only [Set.mem_setOf_eq] at hF; + apply validates_CL_axioms_union.models; + assumption; instance : Entailment.Consistent InterpretabilityLogic.IL := consistent_of_sound_frameclass FrameClass.IL $ by use Veltman.trivialFrame; diff --git a/Foundation/Modal/MCS.lean b/Foundation/Modal/MCS.lean new file mode 100644 index 000000000..c16adc33c --- /dev/null +++ b/Foundation/Modal/MCS.lean @@ -0,0 +1,145 @@ +/- + Maximal consistent set for basic modal logic +-/ +import Foundation.Propositional.MCS +import Foundation.Modal.Entailment.K +import Foundation.Vorspiel.Set.Supplemental + +namespace LO.MaximalConsistentSet + +open Set.LO +open LO.Entailment LO.Entailment.Context +open LO.Modal LO.Modal.Entailment + +variable {F} [DecidableEq F] [BasicModalLogicalConnective F] + {S} [Entailment S F] + {𝓢 : S} [Entailment.K 𝓢] + +variable {Γ Γ₁ Γ₂ : MaximalConsistentSet 𝓢} {φ ψ : F} {n : ℕ} + +lemma iff_mem_multibox : (□^[n]φ ∈ Γ) ↔ (∀ {Γ' : MaximalConsistentSet 𝓢}, (Γ.1.premultibox n ⊆ Γ'.1) → (φ ∈ Γ')) := by + constructor; + . intro hp Γ' hΓ'; apply hΓ'; simpa; + . contrapose!; + intro hp; + obtain ⟨Γ', hΓ'⟩ := lindenbaum (𝓢 := 𝓢) (Γ := insert (∼φ) (Γ.1.premultibox n)) (by + apply iff_consistent_insert_neg_unprovable.mpr; + by_contra hC; + obtain ⟨Γ, hΓ₁, hΓ₂⟩ := Context.provable_iff.mp hC; + have : 𝓢 ⊢ □^[n]⋀Γ ➝ □^[n]φ := imply_multibox_distribute'! hΓ₂; + have : 𝓢 ⊬ □^[n]⋀Γ ➝ □^[n]φ := by + have := Context.provable_iff.not.mp $ iff_mem_provable.not.mp hp; + push_neg at this; + have : 𝓢 ⊬ ⋀(Γ.multibox n) ➝ □^[n]φ := FiniteContext.provable_iff.not.mp $ this (Γ.multibox n) (by + intro ψ hq; + obtain ⟨χ, hr₁, rfl⟩ := List.exists_multibox_of_mem_multibox hq; + simpa using hΓ₁ χ hr₁; + ); + revert this; + contrapose; + simp only [not_not]; + exact C!_trans collect_multibox_conj!; + contradiction; + ); + use Γ'; + constructor; + . exact Set.Subset.trans (by tauto_set) hΓ'; + . apply iff_mem_neg.mp; + apply hΓ'; + simp only [Set.mem_insert_iff, true_or] + +lemma iff_mem_box : (□φ ∈ Γ) ↔ (∀ {Γ' : MaximalConsistentSet 𝓢}, (Γ.1.prebox ⊆ Γ'.1) → (φ ∈ Γ')) := iff_mem_multibox (n := 1) + + +lemma multibox_dn_iff : (□^[n](∼∼φ) ∈ Γ) ↔ (□^[n]φ ∈ Γ) := by + simp only [iff_mem_multibox]; + grind; + +lemma box_dn_iff : (□(∼∼φ) ∈ Γ) ↔ (□φ ∈ Γ) := multibox_dn_iff (n := 1) + + +lemma mem_multibox_dual : □^[n]φ ∈ Γ ↔ ∼(◇^[n](∼φ)) ∈ Γ := by + simp only [iff_mem_provable]; + constructor; + . intro h; + obtain ⟨Γ, hΓ₁, hΓ₂⟩ := Context.provable_iff.mp h; + apply Context.provable_iff.mpr; + use Γ; + constructor; + . assumption; + . exact FiniteContext.provable_iff.mpr $ C!_trans (FiniteContext.provable_iff.mp hΓ₂) (K!_left multibox_duality!); + . intro h; + obtain ⟨Γ, hΓ₁, hΓ₂⟩ := Context.provable_iff.mp h; + apply Context.provable_iff.mpr; + use Γ; + constructor; + . assumption; + . exact FiniteContext.provable_iff.mpr $ C!_trans (FiniteContext.provable_iff.mp hΓ₂) (K!_right multibox_duality!); + +lemma mem_box_dual : □φ ∈ Γ ↔ (∼(◇(∼φ)) ∈ Γ) := mem_multibox_dual (n := 1) + +lemma mem_multidia_dual : ◇^[n]φ ∈ Γ ↔ ∼(□^[n](∼φ)) ∈ Γ := by + simp only [iff_mem_provable]; + constructor; + . intro h; + obtain ⟨Γ, hΓ₁, hΓ₂⟩ := Context.provable_iff.mp h; + apply Context.provable_iff.mpr; + existsi Γ; + constructor; + . assumption; + . exact FiniteContext.provable_iff.mpr $ C!_trans (FiniteContext.provable_iff.mp hΓ₂) (K!_left multidia_duality!); + . intro h; + obtain ⟨Γ, hΓ₁, hΓ₂⟩ := Context.provable_iff.mp h; + apply Context.provable_iff.mpr; + existsi Γ; + constructor; + . assumption; + . exact FiniteContext.provable_iff.mpr $ C!_trans (FiniteContext.provable_iff.mp hΓ₂) (K!_right multidia_duality!); +lemma mem_dia_dual : ◇φ ∈ Γ ↔ (∼(□(∼φ)) ∈ Γ) := mem_multidia_dual (n := 1) + +lemma iff_mem_multidia : (◇^[n]φ ∈ Γ) ↔ (∃ Γ' : MaximalConsistentSet 𝓢, (Γ.1.premultibox n ⊆ Γ'.1) ∧ (φ ∈ Γ'.1)) := by + constructor; + . intro h; + have := mem_multidia_dual.mp h; + have := iff_mem_neg.mp this; + have := iff_mem_multibox.not.mp this; + push_neg at this; + obtain ⟨Γ', h₁, h₂⟩ := this; + use Γ'; + constructor; + . exact h₁; + . exact iff_mem_negneg.mp $ iff_mem_neg.mpr h₂; + . rintro ⟨Γ', h₁, h₂⟩; + apply mem_multidia_dual.mpr; + apply iff_mem_neg.mpr; + apply iff_mem_multibox.not.mpr; + push_neg; + use Γ'; + constructor; + . exact h₁; + . exact iff_mem_neg.mp $ iff_mem_negneg.mpr h₂; + +lemma iff_mem_dia : (◇φ ∈ Γ) ↔ (∃ Γ' : MaximalConsistentSet 𝓢, (Γ.1.prebox ⊆ Γ'.1) ∧ (φ ∈ Γ'.1)) := iff_mem_multidia (n := 1) + + +lemma multibox_multidia : (∀ {φ}, (□^[n]φ ∈ Γ₁.1 → φ ∈ Γ₂.1)) ↔ (∀ {φ}, (φ ∈ Γ₂.1 → ◇^[n]φ ∈ Γ₁.1)) := by + constructor; + . intro h φ; + contrapose!; + intro h₂; + apply iff_mem_neg.mp; + apply h; + apply iff_mem_negneg.mp; + apply (neg_congruence $ mem_multidia_dual).mp; + exact iff_mem_neg.mpr h₂; + . intro h φ; + contrapose!; + intro h₂; + apply iff_mem_neg.mp; + apply (neg_congruence $ mem_multibox_dual).mpr; + apply iff_mem_negneg.mpr; + apply h; + exact iff_mem_neg.mpr h₂; + + +end LO.MaximalConsistentSet diff --git a/Foundation/Propositional/CMCF.lean b/Foundation/Propositional/CMCF.lean new file mode 100644 index 000000000..3ea707042 --- /dev/null +++ b/Foundation/Propositional/CMCF.lean @@ -0,0 +1,390 @@ +/- + Complement maximal consistent finset for propositional logic +-/ +import Foundation.Logic.HilbertStyle.Supplemental + +section + +open LO + +variable {F} [LogicalConnective F] + {S} [Entailment S F] +variable {𝓢 : S} {Γ Δ : Finset F} {φ ψ : F} {Φ : Finset F} + + +namespace LO + +class Compl (F : Type*) where + compl : F → F + +prefix:120 "-" => Compl.compl + +namespace Entailment + +class ComplEquiv [LogicalConnective F] [Compl F] (𝓢 : S) where + compl_equiv! {φ : F} : 𝓢 ⊢! ∼φ ⭤ -φ +export ComplEquiv (compl_equiv!) + +@[simp] lemma compl_equiv {φ : F} [Compl F] [ComplEquiv 𝓢] : 𝓢 ⊢ ∼φ ⭤ -φ := ⟨compl_equiv!⟩ + +section + +variable [Compl F] [Entailment.Minimal 𝓢] [Entailment.ComplEquiv 𝓢] + +def compl_of_neg! [Entailment.Minimal 𝓢] (h : 𝓢 ⊢! ∼φ) : 𝓢 ⊢! -φ := K_left compl_equiv! ⨀ h +@[grind] lemma compl_of_neg : 𝓢 ⊢ ∼φ → 𝓢 ⊢ -φ := λ ⟨a⟩ => ⟨compl_of_neg! a⟩ + +def neg_of_compl! [Entailment.Minimal 𝓢] (h : 𝓢 ⊢! -φ) : 𝓢 ⊢! ∼φ := K_right compl_equiv! ⨀ h +@[grind] lemma neg_of_compl : 𝓢 ⊢ -φ → 𝓢 ⊢ ∼φ := λ ⟨a⟩ => ⟨neg_of_compl! a⟩ + +def O_of_compl! (h₁ : 𝓢 ⊢! φ) (h₂ : 𝓢 ⊢! -φ) : 𝓢 ⊢! ⊥ := negMDP (neg_of_compl! h₂) h₁ +@[grind] lemma O_of_compl : 𝓢 ⊢ φ → 𝓢 ⊢ -φ → 𝓢 ⊢ ⊥ := λ ⟨a⟩ ⟨b⟩ => ⟨O_of_compl! a b⟩ + +def O_of_Ncompl! [DecidableEq F] (h₁ : 𝓢 ⊢! ∼φ) (h₂ : 𝓢 ⊢! ∼-φ) : 𝓢 ⊢! ⊥ := negMDP (K_right (ENN_of_E compl_equiv!) ⨀ h₂) h₁ +@[grind] lemma O_of_Ncompl [DecidableEq F] : 𝓢 ⊢ ∼φ → 𝓢 ⊢ ∼-φ → 𝓢 ⊢ ⊥ := λ ⟨a⟩ ⟨b⟩ => ⟨O_of_Ncompl! a b⟩ + +instance FiniteContext.ComplEquiv (Γ : FiniteContext F 𝓢) : ComplEquiv Γ := ⟨λ {_} => of compl_equiv!⟩ + +instance Context.ComplEquiv (Γ : Context F 𝓢) : ComplEquiv Γ := ⟨λ {_} => of compl_equiv!⟩ + +end + +end Entailment + +end LO + + + +open LO.Entailment LO.Entailment.Context + +namespace Finset.LO + +variable [DecidableEq F] + +def Consistent (𝓢 : S) (Γ : Finset F) : Prop := Γ *⊬[𝓢] ⊥ + +def Inconsistent (𝓢 : S) (Γ : Finset F) : Prop := ¬(Consistent 𝓢 Γ) + +def ComplementBounded [Compl F] (Γ Φ : Finset F) : Prop := Γ ⊆ (Φ ∪ Φ.image (-·)) + +/-- For every `φ` in `Δ`, `φ` or `-φ` is in `Γ` -/ +def ComplementMaximal [Compl F] (Γ Φ : Finset F) : Prop := ∀ φ ∈ Φ, φ ∈ Γ ∨ -φ ∈ Γ + + +lemma def_consistent [Entailment.Minimal 𝓢] : Consistent 𝓢 Γ ↔ ∀ Δ : Finset F, (Δ ⊆ Γ) → Δ *⊬[𝓢] ⊥ := by + constructor; + . intro h Δ hΔ; + have := Context.provable_iff_finset.not.mp h; + push_neg at this; + apply this; + simpa; + . intro h; + apply Context.provable_iff_finset.not.mpr; + push_neg; + simpa using h; + +lemma def_inconsistent [Entailment.Minimal 𝓢] : Inconsistent 𝓢 Γ ↔ ∃ Δ : Finset F, (Δ ⊆ Γ) ∧ (Δ *⊢[𝓢] ⊥) := by + rw [Inconsistent, def_consistent]; + push_neg; + simp; + + +section + +variable [Entailment.Cl 𝓢] + +@[simp] +lemma empty_conisistent [consis : Entailment.Consistent 𝓢] : Consistent 𝓢 ∅ := by + obtain ⟨φ, hφ⟩ := consis.exists_unprovable; + apply def_consistent.mpr; + intro Δ hΔ; + rw [(show Δ = ∅ by simpa [Set.subset_empty_iff, Finset.coe_eq_empty] using hΔ)]; + contrapose! hφ; + apply Context.emptyPrf! + apply of_O!; + simp_all; + +@[grind] +lemma not_mem_falsum (Γ_consis : Consistent 𝓢 Γ) : ⊥ ∉ Γ := by + contrapose! Γ_consis; + suffices Γ *⊢[𝓢] ⊥ by simpa [Consistent]; + apply Context.by_axm!; + simpa; + +@[grind] +lemma not_mem_neg_of_mem (Γ_consis : Consistent 𝓢 Γ) (h : φ ∈ Γ) : ∼φ ∉ Γ := by + by_contra hC; + apply def_consistent.mp Γ_consis {φ, ∼φ} ?_; + . apply Context.bot_of_mem_neg (φ := φ) <;> simp; + . grind; + +@[grind] +lemma not_mem_of_mem_neg (Γ_consis : Consistent 𝓢 Γ) (h : ∼φ ∈ Γ) : φ ∉ Γ := by + by_contra hC; + apply def_consistent.mp Γ_consis {φ, ∼φ} ?_; + . apply Context.bot_of_mem_neg (φ := φ) <;> simp; + . grind; + +lemma iff_insert_consistent : Consistent 𝓢 (insert φ Γ) ↔ ∀ Δ ⊆ Γ, Δ *⊬[𝓢] φ ➝ ⊥ := by + constructor; + . intro h Γ hΓ; + have := def_consistent.mp h (insert φ Γ) ?_; + . contrapose! this; + simp only [Finset.coe_insert]; + apply Context.deductInv! this; + . grind; + . intro h; + apply def_consistent.mpr; + intro Γ hΓ; + have := @h (Γ.erase φ) (by grind); + contrapose! this; + simp only [Finset.coe_erase]; + apply Context.deduct!; + apply Context.weakening! (Γ := Γ); + . simp; + . assumption; + +lemma iff_insert_inconsistent : Inconsistent 𝓢 (insert φ Γ) ↔ ∃ Δ ⊆ Γ, Δ *⊢[𝓢] φ ➝ ⊥ := by + unfold Inconsistent; + apply not_iff_not.mp; + push_neg; + exact iff_insert_consistent; + +lemma neg_provable_iff_insert_not_consistent : Inconsistent 𝓢 (insert φ Γ) ↔ Γ *⊢[𝓢] ∼φ := by + apply Iff.trans iff_insert_inconsistent; + constructor; + . rintro ⟨Δ, hΓΔ, hΔ⟩; + apply N!_iff_CO!.mpr; + apply weakening! hΓΔ hΔ; + . intro h; + use Γ; + constructor; + . tauto; + . apply N!_iff_CO!.mp h; + +section + +variable [Compl F] [ComplEquiv 𝓢] + +@[grind] +lemma not_mem_compl_of_mem (Γ_consis : Consistent 𝓢 Γ) (h : φ ∈ Γ) : (-φ) ∉ Γ := by + by_contra hC; + apply def_consistent.mp Γ_consis {φ, -φ} ?_; + . replace h₁ : {φ, -φ} *⊢[𝓢] φ := by_axm! (by simp); + replace h₂ : {φ, -φ} *⊢[𝓢] -φ := by_axm! (by simp); + convert O_of_compl h₁ h₂; + simp; + . grind; + +@[grind] +lemma not_mem_of_mem_compl (Γ_consis : Consistent 𝓢 Γ) (h : -φ ∈ Γ) : φ ∉ Γ := by + by_contra hC; + apply def_consistent.mp Γ_consis {φ, -φ} ?_; + . replace h₁ : {φ, -φ} *⊢[𝓢] φ := by_axm! (by simp); + replace h₂ : {φ, -φ} *⊢[𝓢] -φ := by_axm! (by simp); + convert O_of_compl h₁ h₂; + simp; + . grind; + +end + +end + + +namespace exists_consistent_complement_closed + +open Classical + +variable [Compl F] + +variable {Γ : Finset F} {l : List F} + +noncomputable def next (𝓢 : S) (φ : F) (Γ : Finset F) : Finset F := if Consistent 𝓢 (insert φ Γ) then insert φ Γ else insert (-φ) Γ + +noncomputable def enum (𝓢 : S) (Γ : Finset F) : List F → Finset F + | [] => Γ + | ψ :: ψs => next 𝓢 ψ (enum 𝓢 Γ ψs) + +local notation:max t"[" l "]" => enum 𝓢 t l + + +section + +@[simp] lemma eq_enum_nil : Γ[[]] = Γ := by simp [enum] + +@[simp] +lemma subset_enum_step : Γ[l] ⊆ (Γ[(ψ :: l)]) := by + simp [enum, next]; + split <;> simp; + +@[simp] +lemma subset_enum : Γ ⊆ Γ[l] := by + induction l with + | nil => simp; + | cons ψ ψs ih => exact Set.Subset.trans ih $ by apply subset_enum_step; + + +lemma of_mem_seed (h : φ ∈ l) : φ ∈ Γ[l] ∨ -φ ∈ Γ[l] := by + induction l with + | nil => simp_all; + | cons ψ ψs ih => + simp only [enum, next]; + rcases List.mem_cons.mp h with (rfl | h) <;> grind; + +lemma of_mem_enum (h : φ ∈ Γ[l]) : φ ∈ Γ ∨ φ ∈ l ∨ (∃ ψ ∈ l, -ψ = φ) := by + induction l generalizing φ with + | nil => simp_all; + | cons ψ ψs ih => + simp only [enum, next] at h; + split at h <;> rcases Finset.mem_insert.mp h with (rfl | h) <;> grind; + +end + + +section + +variable [ComplEquiv 𝓢] [Entailment.Cl 𝓢] + +lemma consistent_next (Γ_consis : Consistent 𝓢 Γ) (φ : F) : Consistent 𝓢 (next 𝓢 φ Γ) := by + simp only [next]; + split; + . simpa; + . rename_i h; + by_contra hC; + have h₁ : ↑Γ *⊢[𝓢] ∼φ := neg_provable_iff_insert_not_consistent.mp h; + have h₂ : ↑Γ *⊢[𝓢] ∼-φ := @neg_provable_iff_insert_not_consistent.mp hC; + have : ↑Γ *⊢[𝓢] ⊥ := O_of_Ncompl h₁ h₂; + contradiction; + +@[grind] +lemma consistent_enum (Γ_consis : Consistent 𝓢 Γ) : Consistent 𝓢 (Γ[l]) := by + induction l with + | nil => exact Γ_consis; + | cons ψ ψs ih => apply consistent_next; exact ih; + +end + +end exists_consistent_complement_closed + +open exists_consistent_complement_closed in +theorem exists_consistent_complement_closed [Compl F] [ComplEquiv 𝓢] [Entailment.Cl 𝓢] (Γ_consis : Consistent 𝓢 Γ) + : ∃ Γ', (Γ ⊆ Γ') ∧ (Consistent 𝓢 Γ') ∧ (ComplementMaximal Γ' Φ) := by + use enum 𝓢 Γ Φ.toList; + refine ⟨?_, ?_, ?_⟩; + . simp; + . grind; + . intro φ hφ; + apply of_mem_seed; + simpa; + +end Finset.LO + + + + +namespace LO + +open Finset.LO + +variable [Compl F] {Φ : Finset F} + +abbrev ComplementMaximalConsistentFinset (𝓢 : S) (Φ : Finset F) := { Γ : Finset F // (Consistent 𝓢 Γ) ∧ (ComplementMaximal Γ Φ) } + +variable {Γ Γ₁ Γ₂ Δ : ComplementMaximalConsistentFinset 𝓢 Φ} {φ ψ : F} + +namespace ComplementMaximalConsistentFinset + +instance : Membership (F) (ComplementMaximalConsistentFinset 𝓢 Φ) := ⟨λ X φ => φ ∈ X.1⟩ + +@[simp] lemma consistent (Γ : ComplementMaximalConsistentFinset 𝓢 Φ) : Consistent 𝓢 Γ := Γ.2.1 +@[simp] lemma unprovable_falsum : Γ.1 *⊬[𝓢] ⊥ := Γ.consistent +@[simp, grind] lemma mem_falsum [DecidableEq F] [Entailment.Cl 𝓢] : ⊥ ∉ Γ := not_mem_falsum (consistent Γ) + +@[simp] lemma maximal (Γ : ComplementMaximalConsistentFinset 𝓢 Φ) : ComplementMaximal Γ Φ := Γ.2.2 + +@[grind] +lemma mem_compl_of_not_mem (hs : ψ ∈ Φ) : ψ ∉ Γ → -ψ ∈ Γ := by + intro h; + rcases Γ.maximal ψ (by assumption) with (h | h); + . contradiction; + . assumption; + +@[grind] +lemma mem_of_not_mem_compl (hs : ψ ∈ Φ) : -ψ ∉ Γ → ψ ∈ Γ := by grind; + +@[grind] +lemma equality_def : Γ₁ = Γ₂ ↔ Γ₁.1 = Γ₂.1 := by + constructor; + . intro h; cases h; rfl; + . intro h; cases Γ₁; cases Γ₂; simp_all; + +variable [Entailment.ComplEquiv 𝓢] [Entailment.Cl 𝓢] + +theorem lindenbaum [DecidableEq F] {Γ : Finset F} (Γ_consis : Consistent 𝓢 Γ) + : ∃ Γ' : ComplementMaximalConsistentFinset 𝓢 Φ, Γ ⊆ Γ'.1 := by + obtain ⟨Γ', ⟨_, _⟩⟩ := exists_consistent_complement_closed Γ_consis; + use ⟨Γ', ?_⟩; + assumption; + +noncomputable instance [DecidableEq F] [Entailment.Consistent 𝓢] : Inhabited (ComplementMaximalConsistentFinset 𝓢 Φ) := ⟨lindenbaum (Γ := ∅) (by simp) |>.choose⟩ + +variable [DecidableEq F] + +@[grind] +lemma membership_iff (hξ : φ ∈ Φ) : (φ ∈ Γ) ↔ (Γ *⊢[𝓢] φ) := by + constructor; + . intro h; exact Context.by_axm! h; + . intro h₁; + suffices -φ ∉ Γ by + apply or_iff_not_imp_right.mp $ ?_; + . assumption; + . apply Γ.maximal; + simpa; + by_contra hC; + have h₂ : Γ *⊢[𝓢] -φ := Context.by_axm! hC; + simpa using O_of_compl h₁ h₂; + +@[grind] +lemma mem_verum (h : ⊤ ∈ Φ) : ⊤ ∈ Γ := by + apply membership_iff h |>.mpr; + exact verum!; + +@[grind] +lemma iff_not_mem_compl (hξ : φ ∈ Φ) : (φ ∈ Γ) ↔ (-φ ∉ Γ) := by + apply Iff.trans $ membership_iff hξ; + constructor; + . intro h₁ h₂; + replace h₂ : Γ *⊢[𝓢] -φ := Context.by_axm! h₂; + simpa using O_of_compl h₁ h₂; + . intro h; + apply Context.by_axm!; + simpa using mem_of_not_mem_compl hξ h; + +@[grind] +lemma iff_mem_compl (hξ : φ ∈ Φ) : (φ ∉ Γ) ↔ (-φ ∈ Γ) := by simpa using iff_not_mem_compl hξ |>.not; + +@[grind] +lemma iff_mem_imp (hφψΦ : (φ ➝ ψ) ∈ Φ) (hφΦ : φ ∈ Φ) (hψΦ : ψ ∈ Φ) : (φ ➝ ψ ∈ Γ) ↔ (φ ∈ Γ → ψ ∈ Γ) := by + constructor; + . intro hφψ hφ; + replace hφψΦ := membership_iff hφψΦ |>.mp hφψ; + replace hφΦ := membership_iff hφΦ |>.mp hφ; + apply membership_iff hψΦ |>.mpr; + exact hφψΦ ⨀ hφΦ; + . intro hφψ; + rcases not_or_of_imp hφψ with (hφ | hψ); + . apply membership_iff hφψΦ |>.mpr; + apply C_of_N; + apply neg_of_compl; + apply Context.by_axm; + exact mem_compl_of_not_mem hφΦ hφ; + . apply membership_iff hφψΦ |>.mpr; + apply C!_of_conseq!; + apply membership_iff hψΦ |>.mp; + assumption; + +end ComplementMaximalConsistentFinset + +end LO + +end diff --git a/Foundation/Propositional/MCS.lean b/Foundation/Propositional/MCS.lean new file mode 100644 index 000000000..e3aa89cd3 --- /dev/null +++ b/Foundation/Propositional/MCS.lean @@ -0,0 +1,323 @@ +/- + Maximal consistent set for propositional classical logic +-/ +import Foundation.Logic.HilbertStyle.Supplemental +import Foundation.Meta.ClProver + +section + +open LO LO.Entailment LO.Entailment.Context + +variable {F} [DecidableEq F] [LogicalConnective F] + {S} [Entailment S F] +variable {𝓢 : S} {Γ Δ : Set F} {φ ψ : F} + +namespace Set.LO + +def Consistent (𝓢 : S) (Γ : Set F) : Prop := Γ *⊬[𝓢] ⊥ + +def Inconsistent (𝓢 : S) (Γ : Set F) : Prop := ¬(Consistent 𝓢 Γ) + +def Maximal (𝓢 : S) (Γ : Set F) : Prop := ∀ Δ, Γ ⊂ Δ → Inconsistent 𝓢 Δ + + +lemma def_consistent [Entailment.Minimal 𝓢] : Consistent 𝓢 Γ ↔ ∀ Δ : Finset F, (↑Δ ⊆ Γ) → Δ *⊬[𝓢] ⊥ := by + constructor; + . intro h Δ hΔ; + have := Context.provable_iff_finset.not.mp h; + push_neg at this; + apply this; + simpa; + . intro h; + apply Context.provable_iff_finset.not.mpr; + push_neg; + simpa using h; + +lemma def_inconsistent [Entailment.Minimal 𝓢] : Inconsistent 𝓢 Γ ↔ ∃ Δ : Finset F, (↑Δ ⊆ Γ) ∧ (Δ *⊢[𝓢] ⊥) := by + rw [Inconsistent, def_consistent]; + push_neg; + simp; + +omit [DecidableEq F] in +@[grind] +lemma iff_maximal_no_proper_consistent_superset : Maximal 𝓢 Γ ↔ (∀ Δ, Consistent 𝓢 Δ → Γ ⊆ Δ → Δ = Γ) := by + dsimp [Maximal, Inconsistent]; + grind; + +section + +variable [Entailment.Cl 𝓢] + +@[simp] +lemma empty_consistent [consis : Entailment.Consistent 𝓢] : Consistent 𝓢 ∅ := by + obtain ⟨φ, hφ⟩ := consis.exists_unprovable; + apply def_consistent.mpr; + intro Δ hΔ; + rw [(show Δ = ∅ by simpa [Set.subset_empty_iff, Finset.coe_eq_empty] using hΔ)]; + contrapose! hφ; + apply Context.emptyPrf! + apply of_O!; + simp_all; + +@[grind] +lemma not_mem_falsum_of_consistent (Γ_consis : Consistent 𝓢 Γ) : ⊥ ∉ Γ := by + contrapose! Γ_consis; + suffices Γ *⊢[𝓢] ⊥ by simpa [Consistent]; + apply Context.by_axm!; + simpa; + +@[grind] +lemma not_mem_neg_of_mem_of_consistent (Γ_consis : Consistent 𝓢 Γ) (h : φ ∈ Γ) : ∼φ ∉ Γ := by + by_contra hC; + apply def_consistent.mp Γ_consis {φ, ∼φ} ?_; + . apply Context.bot_of_mem_neg (φ := φ) <;> simp; + . grind; + +@[grind] +lemma not_mem_of_mem_neg_of_consistent (Γ_consis : Consistent 𝓢 Γ) (h : ∼φ ∈ Γ) : φ ∉ Γ := by + by_contra hC; + apply def_consistent.mp Γ_consis {φ, ∼φ} ?_; + . apply Context.bot_of_mem_neg (φ := φ) <;> simp; + . grind; + +lemma iff_insert_consistent : Consistent 𝓢 (insert φ Γ) ↔ ∀ Δ : Finset F, ↑Δ ⊆ Γ → Δ *⊬[𝓢] φ ➝ ⊥ := by + constructor; + . intro h Γ hΓ; + have := def_consistent.mp h (insert φ Γ) ?_; + . contrapose! this; + simp only [Finset.coe_insert]; + apply Context.deductInv! this; + . grind; + . intro h; + apply def_consistent.mpr; + intro Γ hΓ; + have := @h (Γ.erase φ) (by grind); + contrapose! this; + apply Context.deduct!; + apply Context.weakening! (Γ := Γ); + . simp; + . assumption; + +lemma iff_inconsistent_insert : Inconsistent 𝓢 (insert φ Γ) ↔ ∃ Δ : Finset F, ↑Δ ⊆ Γ ∧ Δ *⊢[𝓢] φ ➝ ⊥ := by + rw [Inconsistent, iff_insert_consistent] + push_neg; + simp; + +lemma iff_inconsistent_insert_provable_neg : Inconsistent 𝓢 (insert φ Γ) ↔ Γ *⊢[𝓢] ∼φ := by + apply Iff.trans iff_inconsistent_insert; + constructor; + . rintro ⟨Δ, hΓΔ, hΔ⟩; + apply N!_iff_CO!.mpr; + apply weakening! hΓΔ hΔ; + . intro h; + obtain ⟨Δ, hΔ₁, hΔ₂⟩ := Context.provable_iff_finset.mp h; + use Δ; + constructor; + . tauto; + . apply N!_iff_CO!.mp; + assumption; + +lemma iff_inconsistent_insert_neg_provable : Inconsistent 𝓢 (insert (∼φ) Γ) ↔ Γ *⊢[𝓢] φ := by + apply Iff.trans iff_inconsistent_insert_provable_neg; + constructor <;> . intro h; cl_prover [h]; + +lemma iff_consistent_insert_neg_unprovable : Consistent 𝓢 (insert (∼φ) Γ) ↔ Γ *⊬[𝓢] φ := by + simpa [Inconsistent] using iff_inconsistent_insert_neg_provable.not; + +lemma iff_consistent_neg_singleton_unprovable : Consistent 𝓢 ({∼φ}) ↔ 𝓢 ⊬ φ := by + rw [(show {∼φ} = insert (∼φ) ∅ by simp), iff_consistent_insert_neg_unprovable]; + apply Context.provable_iff_provable.not.symm; + + +lemma or_consistent_insert_consistent_insert_neg (T_consis : Consistent 𝓢 T) (φ) : + Consistent 𝓢 (insert φ T) ∨ Consistent 𝓢 (insert (∼φ) T) := by + by_contra! hC; + obtain ⟨hC₁, hC₂⟩ := hC; + obtain ⟨Δ₁, hΔ₁Γ, hΔ₁⟩ := iff_inconsistent_insert.mp $ by simpa using hC₁; + obtain ⟨Δ₂, hΔ₂Γ, hΔ₂⟩ := iff_inconsistent_insert.mp $ by simpa using hC₂; + apply def_consistent.mp T_consis (Δ₁ ∪ Δ₂); + . grind; + . replace hΔ₁ : ↑(Δ₁ ∪ Δ₂) *⊢[𝓢] φ ➝ ⊥ := Context.weakening! (by simp) hΔ₁; + replace hΔ₂ : ↑(Δ₁ ∪ Δ₂) *⊢[𝓢] ∼φ ➝ ⊥ := Context.weakening! (by simp) hΔ₂; + exact of_C!_of_C!_of_A! hΔ₁ hΔ₂ (by simp); + +lemma exists_consistent_maximal_of_consistent (Γ_consis : Consistent 𝓢 Γ) + : ∃ Δ, Γ ⊆ Δ ∧ Consistent 𝓢 Δ ∧ ∀ U, Consistent 𝓢 U → Δ ⊆ U → U = Δ := by + obtain ⟨Δ, h₁, ⟨h₂, h₃⟩⟩ := zorn_subset_nonempty { Γ | Consistent 𝓢 Γ} (by + intro c hc chain hnc; + existsi (⋃₀ c); + simp only [Set.mem_setOf_eq]; + constructor; + . apply def_consistent.mpr; + intro Γ hΓ; + by_contra hC; + obtain ⟨U, hUc, hUs⟩ := Set.subset_mem_chain_of_finite c hnc chain (s := ↑Γ.toSet) (by simp) $ by + intro φ hφ; + apply hΓ hφ; + have : Consistent 𝓢 U := hc hUc; + have : Inconsistent 𝓢 U := by + apply def_inconsistent.mpr; + use Γ; + contradiction; + . intro s a; + exact Set.subset_sUnion_of_mem a; + ) Γ Γ_consis; + use Δ; + refine ⟨?_, ?_, ?_⟩; + . assumption; + . assumption; + . intro U hU hZU; + apply Set.eq_of_subset_of_subset; + . exact h₃ hU hZU; + . assumption; + +end + +end Set.LO + + +namespace LO + +open Set.LO + +abbrev MaximalConsistentSet (𝓢 : S) := { Γ // Consistent 𝓢 Γ ∧ Maximal 𝓢 Γ } + +namespace MaximalConsistentSet + +variable {Γ Δ Γ₁ Γ₂ : MaximalConsistentSet 𝓢} + +instance : Membership F (MaximalConsistentSet 𝓢) := ⟨λ Γ φ => φ ∈ Γ.1⟩ + +omit [DecidableEq F] in @[simp] lemma consistent (Γ : MaximalConsistentSet 𝓢) : Consistent 𝓢 Γ := Γ.2.1 + +omit [DecidableEq F] in lemma maximal (Γ : MaximalConsistentSet 𝓢) : Maximal 𝓢 Γ := Γ.2.2 + +omit [DecidableEq F] in +lemma no_proper_consistent_superset (Γ : MaximalConsistentSet 𝓢) : ∀ Δ, Consistent 𝓢 Δ → Γ.1 ⊆ Δ → Δ = Γ.1 := by + apply iff_maximal_no_proper_consistent_superset.mp; + exact Γ.maximal; + + +variable [Entailment.Cl 𝓢] + +lemma exists_of_consistent {Γ : Set F} (Γ_consis : Consistent 𝓢 Γ) : ∃ Δ : MaximalConsistentSet 𝓢, (Γ ⊆ Δ.1) := by + have ⟨Γ, _⟩ := exists_consistent_maximal_of_consistent Γ_consis; + use ⟨Γ, ?_⟩ <;> grind; + +alias lindenbaum := exists_of_consistent + + +instance [Entailment.Consistent 𝓢] : Nonempty (MaximalConsistentSet 𝓢) := ⟨lindenbaum empty_consistent |>.choose⟩ + +@[grind] +lemma or_mem_mem_neg (φ) : φ ∈ Γ ∨ ∼φ ∈ Γ := by + by_contra! hC; + rcases or_consistent_insert_consistent_insert_neg Γ.consistent φ with h | h; + . apply hC.1; simpa using Γ.no_proper_consistent_superset _ h (by simp); + . apply hC.2; simpa using Γ.no_proper_consistent_superset _ h (by simp); + +lemma iff_mem_provable : φ ∈ Γ ↔ Γ.1 *⊢[𝓢] φ := by + constructor; + . intro h; + apply Context.by_axm!; + simpa; + . intro hφ; + suffices ∼φ ∉ Γ.1 by apply or_iff_not_imp_right.mp $ (or_mem_mem_neg φ); assumption; + by_contra hnφ; + apply Γ.consistent; + replace hnφ : Γ.1 *⊢[𝓢] ∼φ := Context.by_axm! hnφ; + cl_prover [hφ, hnφ]; + +@[simp, grind] lemma not_mem_falsum : ⊥ ∉ Γ := not_mem_falsum_of_consistent Γ.consistent +@[simp, grind] lemma mem_verum : ⊤ ∈ Γ := by apply iff_mem_provable.mpr; cl_prover; + +@[grind] +lemma iff_mem_neg : (∼φ ∈ Γ) ↔ (φ ∉ Γ) := by + simp only [iff_mem_provable]; + constructor; + . intro hnφ hφ; + apply Γ.consistent; + cl_prover [hφ, hnφ]; + . intro hφ; + apply Context.by_axm!; + simpa using Γ.no_proper_consistent_superset _ (iff_consistent_insert_neg_unprovable.mpr hφ) (by tauto); + +lemma iff_forall_mem_provable : (∀ Γ : MaximalConsistentSet 𝓢, φ ∈ Γ) ↔ 𝓢 ⊢ φ := by + constructor; + . contrapose!; + intro h; + obtain ⟨Γ, hΓ⟩ := lindenbaum $ iff_consistent_neg_singleton_unprovable.mpr h; + use Γ; + apply iff_mem_neg.mp; + simpa using hΓ; + . intro h Γ; + apply iff_mem_provable.mpr; + exact Context.of! h; + +@[grind] lemma mem_of_provable (h : 𝓢 ⊢ φ) : φ ∈ Γ := iff_forall_mem_provable.mpr h Γ + +@[grind] lemma iff_mem_negneg : (∼∼φ ∈ Γ) ↔ (φ ∈ Γ) := by grind + +@[grind ⇒] +lemma iff_mem_imp : ((φ ➝ ψ) ∈ Γ) ↔ ((φ ∈ Γ) → (ψ ∈ Γ)) := by + constructor; + . intro hφψ hφ; + simp_all only [iff_mem_provable] + cl_prover [hφψ, hφ]; + . intro h; + rcases imp_iff_not_or.mp h with (h | h); + . replace h := iff_mem_provable.mp $ iff_mem_neg.mpr h; + apply iff_mem_provable.mpr; + cl_prover [h]; + . replace h := iff_mem_provable.mp h; + apply iff_mem_provable.mpr; + cl_prover [h]; + + +@[grind] +lemma mdp (hφψ : (φ ➝ ψ) ∈ Γ) (hφ : φ ∈ Γ) : ψ ∈ Γ := iff_mem_imp.mp hφψ hφ + +@[grind ⇒] +lemma iff_mem_and : ((φ ⋏ ψ) ∈ Γ) ↔ (φ ∈ Γ) ∧ (ψ ∈ Γ) := by + constructor; + . intro hφψ; + simp_all only [iff_mem_provable]; + constructor <;> cl_prover [hφψ]; + . simp_all only [iff_mem_provable]; + rintro ⟨hφ, hψ⟩; + cl_prover [hφ, hψ]; + +@[grind ⇒] +lemma iff_mem_or : ((φ ⋎ ψ) ∈ Γ) ↔ (φ ∈ Γ) ∨ (ψ ∈ Γ) := by + constructor; + . intro hφψ; + replace hφψ := iff_mem_provable.mp hφψ; + by_contra!; + rcases this with ⟨hφ, hψ⟩; + replace hφ := iff_mem_provable.mp $ iff_mem_neg.mpr hφ; + replace hψ := iff_mem_provable.mp $ iff_mem_neg.mpr hψ; + apply Γ.consistent; + cl_prover [hφψ, hφ, hψ]; + . simp_all only [iff_mem_provable]; + rintro (h | h) <;> cl_prover [h]; + +@[grind] +lemma iff_mem_conj {l : List F} : (⋀l ∈ Γ) ↔ (∀ φ ∈ l, φ ∈ Γ) := by simp [iff_mem_provable, Conj₂!_iff_forall_provable]; + +lemma imp_of_provable_C (hφψ : Γ *⊢[𝓢] (φ ➝ ψ)) : (φ ∈ Γ) → (ψ ∈ Γ) := by + apply iff_mem_imp.mp; + apply iff_mem_provable.mpr; + assumption; + +lemma iff_of_provable_E (h : Γ *⊢[𝓢] (φ ⭤ ψ)) : φ ∈ Γ ↔ ψ ∈ Γ := by + constructor <;> . apply imp_of_provable_C; cl_prover [h]; + +@[grind ⇒] lemma neg_monotone (h : φ ∈ Γ → ψ ∈ Γ) : (∼ψ ∈ Γ) → (∼φ ∈ Γ) := by simp only [iff_mem_neg]; grind; + +@[grind ⇒] lemma neg_congruence (h : φ ∈ Γ ↔ ψ ∈ Γ) : (∼φ ∈ Γ) ↔ (∼ψ ∈ Γ) := by grind; + +end MaximalConsistentSet + +end LO + +end