From 08b5c3d3bf9643c7ddd212af013bfd7bf19bbc44 Mon Sep 17 00:00:00 2001 From: SnO2WMaN Date: Thu, 30 Oct 2025 03:45:36 +0900 Subject: [PATCH 1/8] wip --- Foundation.lean | 3 +- .../InterpretabilityLogic/LogicSymbol.lean | 10 + .../InterpretabilityLogic/Veltman/Basic.lean | 67 ++-- .../Veltman/Hilbert.lean | 12 - .../Veltman/Logic/CL.lean | 25 +- .../Veltman/Logic/IL/Completeness.lean | 329 ++++++++++++++++++ .../Logic/{IL.lean => IL/Soundness.lean} | 18 +- 7 files changed, 409 insertions(+), 55 deletions(-) create mode 100644 Foundation/InterpretabilityLogic/Veltman/Logic/IL/Completeness.lean rename Foundation/InterpretabilityLogic/Veltman/Logic/{IL.lean => IL/Soundness.lean} (62%) 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/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..14fee7246 --- /dev/null +++ b/Foundation/InterpretabilityLogic/Veltman/Logic/IL/Completeness.lean @@ -0,0 +1,329 @@ +import Foundation.InterpretabilityLogic.Veltman.Logic.IL.Soundness + +namespace LO.InterpretabilityLogic + +variable {α : Type*} [DecidableEq α] +variable {S} [Entailment S (Formula α)] +variable {𝓢 : S} + +open Modal (Kripke.Frame Kripke.Model) + +namespace Formula + +def subformula : Formula α → Finset (Formula α) + | atom a => {atom a} + | ⊥ => {⊥} + | φ ➝ ψ => {φ ➝ ψ} ∪ subformula φ ∪ subformula ψ + | □φ => {□φ} ∪ subformula φ + | φ ▷ ψ => {φ ▷ ψ} ∪ subformula φ ∪ subformula ψ + +@[simp, grind] +lemma mem_self_subformula {φ : Formula α} : φ ∈ φ.subformula := by + induction φ <;> simp_all [subformula, Finset.mem_union, Finset.mem_singleton] + + +def complement : Formula α → Formula α + | ∼φ => φ + | φ => ∼φ +prefix:80 "-" => complement + +end Formula + + +namespace FormulaFinset + +variable {Φ Φ₁ Φ₂ : FormulaFinset α} + +class SubformulaClosed (Φ : FormulaFinset α) where + subfml_closed : ∀ φ ∈ Φ, φ.subformula ⊆ Φ + + +class Adequate (Φ : FormulaFinset α) extends Φ.SubformulaClosed where + compl_closed : ∀ φ ∈ Φ, -φ ∈ Φ + mem_top_rhd_top : ⊤ ▷ ⊤ ∈ Φ + mem_part₁ : ∀ {φ ψ}, (φ ▷ ψ) ∈ Φ → (□-φ) ∈ Φ ∧ (□-ψ) ∈ Φ + mem_part₂ : ∀ {φ₁ ψ₁ φ₂ ψ₂}, + (φ₁ ▷ ψ₁) ∈ Φ → (φ₂ ▷ ψ₂) ∈ Φ → + ∀ ξ₁ ∈ [φ₁, ψ₁, φ₂, ψ₂], + ∀ ξ₂ ∈ [φ₁, ψ₁, φ₂, ψ₂], + (ξ₁ ▷ ξ₂) ∈ Φ + +attribute [simp] Adequate.mem_top_rhd_top + + + +def Consistent (𝓢 : S) (Φ : FormulaFinset α) : Prop := Φ *⊬[𝓢] ⊥ +def Inconsistent (𝓢 : S) (Φ : FormulaFinset α) : Prop := ¬Consistent 𝓢 Φ + +def Maximal (𝓢 : S) (Φ : FormulaFinset α) := ∀ Ψ, Φ ⊂ Ψ → Inconsistent 𝓢 Ψ + +end FormulaFinset + +section + +def AdequateSet (α) [DecidableEq α] := { Φ : FormulaFinset α // Φ.Adequate } + +def MaximalConsistentSet (𝓢 : S) (Φ : AdequateSet α) := { Ψ : FormulaFinset α // Ψ ⊆ Φ.1 ∧ Ψ.Maximal 𝓢 ∧ Ψ.Consistent 𝓢 } + +variable {Φ} {Γ Δ Θ : MaximalConsistentSet 𝓢 Φ} + +structure ILSuccessor (Γ Δ : MaximalConsistentSet 𝓢 Φ) : Prop where + prop1 : (∀ φ ∈ Γ.1.prebox, φ ∈ Δ.1 ∧ □φ ∈ Δ.1) + prop2 : (∃ φ ∈ Δ.1.prebox, □φ ∉ Γ.1) +infix:80 " < " => ILSuccessor + +structure ILCriticalSuccessor (χ : { χ : Formula α // χ ∈ Φ.1}) (Γ Δ : MaximalConsistentSet 𝓢 Φ) 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; + +lemma claim3 (h₁ : ∼(φ ▷ χ.1) ∈ Γ.1) : ∃ Δ : MaximalConsistentSet 𝓢 Φ, (Γ <[χ] Δ) ∧ φ ∈ Δ.1 := by + have : (φ ▷ χ.1) ∈ Φ.1 := Φ.2.compl_closed (∼(φ ▷ χ.1)) $ Γ.2.1 h₁; + have : □-φ ∈ Φ.1 := Φ.2.mem_part₁ this |>.1; + have : □-φ ∉ Γ.1 := by + by_contra hC; + sorry; + let Δ₀ : FormulaFinset _ := + {φ, □-φ} ∪ + Γ.1.prebox ∪ + Γ.1.prebox.box ∪ + ((Γ.1.preimage (λ ξ => ξ ▷ χ.1) (by simp)) |>.image (λ ξ => -ξ)) ∪ + ((Γ.1.preimage (λ ξ => ξ ▷ χ.1) (by simp)) |>.image (λ ξ => □-ξ)) + have Δ₀_consis : Δ₀.Consistent 𝓢 := by sorry; + obtain ⟨Δ, hΔ⟩ : ∃ Δ : MaximalConsistentSet 𝓢 Φ, Δ₀ ⊆ Δ.1 := by + sorry; + use Δ; + 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₃ : Γ <[χ] Δ) + : ∃ Δ' : MaximalConsistentSet 𝓢 Φ, (Γ <[χ] Δ') ∧ ψ ∈ Δ'.1 ∧ □(-ψ) ∈ Δ'.1 := by + have : □-ψ ∉ Γ.1 := by + by_contra hC; + sorry; + let Δ₀ : FormulaFinset _ := + {ψ, □-ψ} ∪ + Γ.1.prebox ∪ + Γ.1.prebox.box ∪ + ((Γ.1.preimage (λ ξ => ξ ▷ χ) (by simp)) |>.image (λ ξ => -ξ)) ∪ + ((Γ.1.preimage (λ ξ => ξ ▷ χ) (by simp)) |>.image (λ ξ => □-ξ)) + + have Δ₀_consis : Δ₀.Consistent 𝓢 := by sorry; + obtain ⟨Δ, hΔ⟩ : ∃ Δ : MaximalConsistentSet 𝓢 Φ, Δ₀ ⊆ Δ.1 := by + sorry; + use Δ; + 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 {𝓢 : S} {Γ : MaximalConsistentSet 𝓢 Φ} + +protected inductive ILMiniCanonicalModel.IsWorld (Γ : MaximalConsistentSet 𝓢 Φ) : MaximalConsistentSet 𝓢 Φ → List { φ // φ ∈ Φ.1 } → Prop + | i₁ : ILMiniCanonicalModel.IsWorld Γ Γ [] + | i₂ {Δ Δ'} {τ} : ILMiniCanonicalModel.IsWorld Γ Δ τ → Δ < Δ' → ILMiniCanonicalModel.IsWorld Γ Δ' τ + | i₃ {Δ Δ'} {τ χ} : ILMiniCanonicalModel.IsWorld Γ Δ τ → Δ <[χ] Δ' → ILMiniCanonicalModel.IsWorld Γ Δ' (τ ++ [χ]) + +def ILMiniCanonicalModel (Γ : MaximalConsistentSet 𝓢 Φ) : Veltman.Model where + toKripkeFrame := { + World := { P : (MaximalConsistentSet 𝓢 Φ) × (List _) // ILMiniCanonicalModel.IsWorld Γ P.1 P.2 } + 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 + world_finite := by sorry + 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τ; + +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 {X : ILMiniCanonicalModel Γ} (hφ : φ ∈ Φ.1) : X ⊧ φ ↔ φ ∈ X.1.1.1 := by + induction φ generalizing X with + | hfalsum => sorry; + | hatom a => tauto; + | himp φ ψ ihφ ihψ => + have := ihφ (X := X) (by sorry); + have := ihψ (X := X) (by sorry); + sorry; + | hbox φ ih => + have := ih (X := X) (by sorry); + sorry; + | hrhd φ ψ ihφ ihψ => + let ψ : { χ // χ ∈ Φ.1} := ⟨ψ, by sorry⟩; + 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 sorry) |>.mpr; + simpa; + . rintro V ⟨_, ⟨χ, hχXV, _⟩, h⟩; + apply ihψ (by sorry) |>.not.mpr; + have := hχXV.prop3 χ (by sorry) |>.1; + sorry; + . rintro h ⟨U, ⟨χ, hχXU, τ, eU₂⟩⟩ hU; + replace hU := ihφ (by sorry) |>.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 sorry) |>.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Γ⟩ : ∃ Γ : MaximalConsistentSet (InterpretabilityLogic.IL) Φ, {-φ} ⊆ Γ.1 := by sorry; + use ILMiniCanonicalModel Γ, ⟨⟨Γ, []⟩, ILMiniCanonicalModel.IsWorld.i₁⟩; + constructor; + . apply Set.mem_setOf_eq.mpr; + infer_instance; + . apply ILMiniCanonicalModel.truthlemma (by sorry) |>.not.mpr; + 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; From 23c053269f74d76f1af9b04313b9624ecd0c3fa5 Mon Sep 17 00:00:00 2001 From: SnO2WMaN Date: Thu, 30 Oct 2025 18:16:58 +0900 Subject: [PATCH 2/8] CCMF --- .../Veltman/Logic/IL/Completeness.lean | 532 +++++++++++++++++- 1 file changed, 516 insertions(+), 16 deletions(-) diff --git a/Foundation/InterpretabilityLogic/Veltman/Logic/IL/Completeness.lean b/Foundation/InterpretabilityLogic/Veltman/Logic/IL/Completeness.lean index 14fee7246..f3bb07064 100644 --- a/Foundation/InterpretabilityLogic/Veltman/Logic/IL/Completeness.lean +++ b/Foundation/InterpretabilityLogic/Veltman/Logic/IL/Completeness.lean @@ -1,5 +1,411 @@ import Foundation.InterpretabilityLogic.Veltman.Logic.IL.Soundness + +namespace LO + +class Compl (F : Type*) [Tilde F] where + compl : F → F + +prefix:120 "-" => Compl.compl + + + +namespace Entailment + +class ComplEquiv [LogicalConnective F] [Compl F] [Entailment S F] (𝓢 : S) where + compl_equiv! {φ : F} : 𝓢 ⊢! ∼φ ⭤ -φ +export ComplEquiv (compl_equiv!) + + +section + +variable {F S : Type*} [LogicalConnective F] [Compl F] [Entailment S F] + {𝓢 : S} {φ : F} [ComplEquiv 𝓢] + +@[simp] lemma compl_equiv : 𝓢 ⊢ ∼φ ⭤ -φ := ⟨compl_equiv!⟩ + + +section + +variable [Entailment.Minimal 𝓢] + +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 + +end Entailment + + + +namespace CCMF + +open LO.Entailment LO.Entailment.Context LO.Modal.Entailment + + +variable {F} [LogicalConnective F] [DecidableEq F] + {S} [Entailment S F] +variable {𝓢 : S} {Γ Δ : Finset F} {φ ψ : F} + +def Consistent (𝓢 : S) (Γ : 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; + + +def Inconsistent (𝓢 : S) (Γ : Finset F) : Prop := ¬(Consistent 𝓢 Γ) + +lemma def_inconsistent [Entailment.Minimal 𝓢] : Inconsistent 𝓢 Γ ↔ ∃ Δ : Finset F, (Δ ⊆ Γ) ∧ (Δ *⊢[𝓢] ⊥) := by + rw [Inconsistent, def_consistent]; + push_neg; + simp; + + +def Maximal (𝓢 : S) (Γ : Finset F) : Prop := ∀ Δ, Γ ⊂ Δ → Inconsistent 𝓢 Δ + +def ComplementSubset [Compl F] (Γ Δ : Finset F) : Prop := Γ ⊆ (Δ ∪ Δ.image (-·)) + +/-- For every `φ` in `Δ`, `φ` or `-φ` is in `Γ` -/ +def ComplementMaximal [Compl F] (Γ Δ : Finset F) : Prop := ∀ φ ∈ Δ, φ ∈ Γ ∨ -φ ∈ Γ + + +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; + +end + + +section + +variable [Compl F] [Entailment.Cl 𝓢] [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 + + +namespace exists_consistent_complementary_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_complementary_closed + + +open exists_consistent_complementary_closed in +theorem exists_consistent_complement_maximal {Ξ : Finset F} [Compl F] [ComplEquiv 𝓢] [Entailment.Cl 𝓢] + (Γ_consis : Consistent 𝓢 Γ) + (subset_ΓΔ : ComplementSubset Γ Ξ) + : ∃ Γ', (Γ ⊆ Γ') ∧ (Consistent 𝓢 Γ') ∧ (ComplementSubset Γ' Ξ) ∧ (ComplementMaximal Γ' Ξ) := by + use enum 𝓢 Γ Ξ.toList; + refine ⟨?_, ?_, ?_, ?_⟩; + . simp; + . grind; + . intro φ hφ; + simp only [Finset.mem_union, Finset.mem_image]; + rcases of_mem_enum hφ with (hφ | hφ | ⟨ψ, hψ, rfl⟩); + . dsimp [ComplementSubset] at subset_ΓΔ + grind; + . left; + simpa using hφ; + . right; + use ψ; + constructor; + . simpa using hψ; + . rfl + . intro φ hφ; + apply of_mem_seed; + simpa; + +section + +variable [Compl F] {Φ : Finset F} + +abbrev ComplementMaximalConsistentFinset (𝓢 : S) (Φ : Finset F) := { Γ : Finset F // (Consistent 𝓢 Γ) ∧ (ComplementSubset Γ Φ) ∧ (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 [Entailment.Cl 𝓢] : ⊥ ∉ Γ := not_mem_falsum (consistent Γ) + +@[simp] lemma maximal (Γ : ComplementMaximalConsistentFinset 𝓢 Φ) : ComplementMaximal Γ Φ := Γ.2.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 {Γ : Finset F} (Γ_consis : Consistent 𝓢 Γ) (X_sub : ComplementSubset Γ Φ) + : ∃ Γ' : ComplementMaximalConsistentFinset 𝓢 Φ, Γ ⊆ Γ'.1 := by + obtain ⟨Y, ⟨_, _, _⟩⟩ := exists_consistent_complement_maximal Γ_consis X_sub; + use ⟨Y, (by assumption), (by assumption)⟩; + +noncomputable instance [Entailment.Consistent 𝓢] : Inhabited (ComplementMaximalConsistentFinset 𝓢 Φ) := ⟨lindenbaum (Γ := ∅) (by simp) (by tauto) |>.choose⟩ + +@[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 + +end CCMF + +end LO + + + + + + namespace LO.InterpretabilityLogic variable {α : Type*} [DecidableEq α] @@ -10,22 +416,59 @@ open Modal (Kripke.Frame Kripke.Model) namespace Formula -def subformula : Formula α → Finset (Formula α) +variable {φ ψ χ : Formula α} + +@[grind] +def subformulas : Formula α → Finset (Formula α) | atom a => {atom a} | ⊥ => {⊥} - | φ ➝ ψ => {φ ➝ ψ} ∪ subformula φ ∪ subformula ψ - | □φ => {□φ} ∪ subformula φ - | φ ▷ ψ => {φ ▷ ψ} ∪ subformula φ ∪ subformula ψ + | φ ➝ ψ => {φ ➝ ψ} ∪ subformulas φ ∪ subformulas ψ + | □φ => {□φ} ∪ subformulas φ + | φ ▷ ψ => {φ ▷ ψ} ∪ subformulas φ ∪ subformulas ψ + +namespace subformulas @[simp, grind] -lemma mem_self_subformula {φ : Formula α} : φ ∈ φ.subformula := by - induction φ <;> simp_all [subformula, Finset.mem_union, Finset.mem_singleton] +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_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_neg (h : (∼ψ) ∈ φ.subformulas) : ψ ∈ φ.subformulas := (mem_imp h).1 +@[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 def complement : Formula α → Formula α | ∼φ => φ | φ => ∼φ -prefix:80 "-" => complement +instance : Compl (Formula α) where + compl := complement end Formula @@ -35,7 +478,43 @@ namespace FormulaFinset variable {Φ Φ₁ Φ₂ : FormulaFinset α} class SubformulaClosed (Φ : FormulaFinset α) where - subfml_closed : ∀ φ ∈ Φ, φ.subformula ⊆ Φ + subfml_closed : ∀ φ ∈ Φ, φ.subformulas ⊆ Φ + +namespace SubformulaClosed + +variable [Φ.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 SubformulaClosed class Adequate (Φ : FormulaFinset α) extends Φ.SubformulaClosed where @@ -50,6 +529,16 @@ class Adequate (Φ : FormulaFinset α) extends Φ.SubformulaClosed where attribute [simp] Adequate.mem_top_rhd_top +namespace Adequate + +variable [Φ.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 + def Consistent (𝓢 : S) (Φ : FormulaFinset α) : Prop := Φ *⊬[𝓢] ⊥ @@ -63,6 +552,17 @@ 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 + + def MaximalConsistentSet (𝓢 : S) (Φ : AdequateSet α) := { Ψ : FormulaFinset α // Ψ ⊆ Φ.1 ∧ Ψ.Maximal 𝓢 ∧ Ψ.Consistent 𝓢 } variable {Φ} {Γ Δ Θ : MaximalConsistentSet 𝓢 Φ} @@ -271,14 +771,14 @@ lemma ILMiniCanonicalModel.truthlemma {X : ILMiniCanonicalModel Γ} (hφ : φ | hfalsum => sorry; | hatom a => tauto; | himp φ ψ ihφ ihψ => - have := ihφ (X := X) (by sorry); - have := ihψ (X := X) (by sorry); + 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 sorry); + + have := ih (X := X) (by grind); sorry; | hrhd φ ψ ihφ ihψ => - let ψ : { χ // χ ∈ Φ.1} := ⟨ψ, by sorry⟩; + 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!; @@ -287,14 +787,14 @@ lemma ILMiniCanonicalModel.truthlemma {X : ILMiniCanonicalModel Γ} (hφ : φ obtain ⟨Δ, hΔ₁, hΔ₂⟩ := claim3 h; use ⟨⟨⟨Δ, X.1.2 ++ [ψ]⟩, IsWorld.i₃ X.2 hΔ₁⟩, ⟨ψ, by simpa⟩⟩; constructor; - . apply ihφ (by sorry) |>.mpr; + . apply ihφ (by grind) |>.mpr; simpa; . rintro V ⟨_, ⟨χ, hχXV, _⟩, h⟩; - apply ihψ (by sorry) |>.not.mpr; + 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 sorry) |>.mp 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; @@ -305,7 +805,7 @@ lemma ILMiniCanonicalModel.truthlemma {X : ILMiniCanonicalModel Γ} (hφ : φ constructor; . use τ; . use []; simp; - . apply ihψ (by sorry) |>.mpr; + . apply ihψ (by grind) |>.mpr; simpa; end Veltman From f09d09ca0802ebfaaa5dbfceb4560942f5febae4 Mon Sep 17 00:00:00 2001 From: SnO2WMaN Date: Fri, 31 Oct 2025 01:33:05 +0900 Subject: [PATCH 3/8] wip --- .../Veltman/Logic/IL/Completeness.lean | 216 +++++++++++++----- 1 file changed, 164 insertions(+), 52 deletions(-) diff --git a/Foundation/InterpretabilityLogic/Veltman/Logic/IL/Completeness.lean b/Foundation/InterpretabilityLogic/Veltman/Logic/IL/Completeness.lean index f3bb07064..a52916784 100644 --- a/Foundation/InterpretabilityLogic/Veltman/Logic/IL/Completeness.lean +++ b/Foundation/InterpretabilityLogic/Veltman/Logic/IL/Completeness.lean @@ -87,10 +87,10 @@ lemma def_inconsistent [Entailment.Minimal 𝓢] : Inconsistent 𝓢 Γ ↔ ∃ def Maximal (𝓢 : S) (Γ : Finset F) : Prop := ∀ Δ, Γ ⊂ Δ → Inconsistent 𝓢 Δ -def ComplementSubset [Compl F] (Γ Δ : Finset F) : Prop := Γ ⊆ (Δ ∪ Δ.image (-·)) +def ComplementBounded [Compl F] (Γ Φ : Finset F) : Prop := Γ ⊆ (Φ ∪ Φ.image (-·)) /-- For every `φ` in `Δ`, `φ` or `-φ` is in `Γ` -/ -def ComplementMaximal [Compl F] (Γ Δ : Finset F) : Prop := ∀ φ ∈ Δ, φ ∈ Γ ∨ -φ ∈ Γ +def ComplementMaximal [Compl F] (Γ Φ : Finset F) : Prop := ∀ φ ∈ Φ, φ ∈ Γ ∨ -φ ∈ Γ section @@ -273,18 +273,17 @@ end exists_consistent_complementary_closed open exists_consistent_complementary_closed in -theorem exists_consistent_complement_maximal {Ξ : Finset F} [Compl F] [ComplEquiv 𝓢] [Entailment.Cl 𝓢] - (Γ_consis : Consistent 𝓢 Γ) - (subset_ΓΔ : ComplementSubset Γ Ξ) - : ∃ Γ', (Γ ⊆ Γ') ∧ (Consistent 𝓢 Γ') ∧ (ComplementSubset Γ' Ξ) ∧ (ComplementMaximal Γ' Ξ) := by - use enum 𝓢 Γ Ξ.toList; +theorem exists_consistent_complement_maximal [Compl F] [ComplEquiv 𝓢] [Entailment.Cl 𝓢] + (Γ_consis : Consistent 𝓢 Γ) (Γ_bounded : ComplementBounded Γ Φ) + : ∃ Γ', (Γ ⊆ Γ') ∧ (Consistent 𝓢 Γ') ∧ (ComplementBounded Γ' Φ) ∧ (ComplementMaximal Γ' Φ) := by + use enum 𝓢 Γ Φ.toList; refine ⟨?_, ?_, ?_, ?_⟩; . simp; . grind; . intro φ hφ; simp only [Finset.mem_union, Finset.mem_image]; rcases of_mem_enum hφ with (hφ | hφ | ⟨ψ, hψ, rfl⟩); - . dsimp [ComplementSubset] at subset_ΓΔ + . dsimp [ComplementBounded] at Γ_bounded grind; . left; simpa using hφ; @@ -301,7 +300,7 @@ section variable [Compl F] {Φ : Finset F} -abbrev ComplementMaximalConsistentFinset (𝓢 : S) (Φ : Finset F) := { Γ : Finset F // (Consistent 𝓢 Γ) ∧ (ComplementSubset Γ Φ) ∧ (ComplementMaximal Γ Φ) } +abbrev ComplementMaximalConsistentFinset (𝓢 : S) (Φ : Finset F) := { Γ : Finset F // (Consistent 𝓢 Γ) ∧ (ComplementBounded Γ Φ) ∧ (ComplementMaximal Γ Φ) } variable {Γ Γ₁ Γ₂ Δ : ComplementMaximalConsistentFinset 𝓢 Φ} {φ ψ : F} @@ -333,10 +332,11 @@ lemma equality_def : Γ₁ = Γ₂ ↔ Γ₁.1 = Γ₂.1 := by variable [Entailment.ComplEquiv 𝓢] [Entailment.Cl 𝓢] -theorem lindenbaum {Γ : Finset F} (Γ_consis : Consistent 𝓢 Γ) (X_sub : ComplementSubset Γ Φ) +theorem lindenbaum {Γ : Finset F} (Γ_consis : Consistent 𝓢 Γ) (Γ_bounded : ComplementBounded Γ Φ) : ∃ Γ' : ComplementMaximalConsistentFinset 𝓢 Φ, Γ ⊆ Γ'.1 := by - obtain ⟨Y, ⟨_, _, _⟩⟩ := exists_consistent_complement_maximal Γ_consis X_sub; - use ⟨Y, (by assumption), (by assumption)⟩; + obtain ⟨Γ', ⟨_, _⟩⟩ := exists_consistent_complement_maximal Γ_consis Γ_bounded; + use ⟨Γ', ?_⟩; + assumption; noncomputable instance [Entailment.Consistent 𝓢] : Inhabited (ComplementMaximalConsistentFinset 𝓢 Φ) := ⟨lindenbaum (Γ := ∅) (by simp) (by tauto) |>.choose⟩ @@ -463,6 +463,13 @@ lemma mem_rhd (h : (ψ ▷ χ) ∈ φ.subformulas) : ψ ∈ φ.subformulas ∧ end subformulas +@[simp, grind] lemma eq_falsum : (falsum : Formula α) = ⊥ := rfl +@[simp, grind] lemma eq_or (φ ψ : Formula α) : or φ ψ = φ ⋎ ψ := rfl +@[simp, grind] lemma eq_and (φ ψ : Formula α) : and φ ψ = φ ⋏ ψ := rfl +@[simp, grind] lemma eq_imp (φ ψ : Formula α) : imp φ ψ = φ ➝ ψ := rfl +@[simp, grind] lemma eq_neg (φ : Formula α) : neg φ = ∼φ := rfl +@[simp, grind] lemma eq_box (φ : Formula α) : box φ = □φ := rfl +@[simp, grind] lemma eq_dia (φ : Formula α) : dia φ = ◇φ := rfl def complement : Formula α → Formula α | ∼φ => φ @@ -470,6 +477,65 @@ def complement : Formula α → Formula α instance : Compl (Formula α) where compl := complement +namespace complement + +omit [DecidableEq α] +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 + + +@[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 ψ) + end Formula @@ -539,7 +605,15 @@ variable [Φ.Adequate] end Adequate - +open LO.Entailment in +instance [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; def Consistent (𝓢 : S) (Φ : FormulaFinset α) : Prop := Φ *⊬[𝓢] ⊥ def Inconsistent (𝓢 : S) (Φ : FormulaFinset α) : Prop := ¬Consistent 𝓢 Φ @@ -563,20 +637,22 @@ variable {Φ : AdequateSet α} end AdequateSet -def MaximalConsistentSet (𝓢 : S) (Φ : AdequateSet α) := { Ψ : FormulaFinset α // Ψ ⊆ Φ.1 ∧ Ψ.Maximal 𝓢 ∧ Ψ.Consistent 𝓢 } +open LO.CCMF + +-- def MaximalConsistentSet (𝓢 : S) (Φ : AdequateSet α) := { Ψ : FormulaFinset α // Ψ ⊆ Φ.1 ∧ Ψ.Maximal 𝓢 ∧ Ψ.Consistent 𝓢 } -variable {Φ} {Γ Δ Θ : MaximalConsistentSet 𝓢 Φ} +variable {Φ : AdequateSet α} {Γ Δ Θ : { Γ : ComplementMaximalConsistentFinset 𝓢 Φ.1 // Γ.1 ⊆ Φ.1 }} -structure ILSuccessor (Γ Δ : MaximalConsistentSet 𝓢 Φ) : Prop where - prop1 : (∀ φ ∈ Γ.1.prebox, φ ∈ Δ.1 ∧ □φ ∈ Δ.1) - prop2 : (∃ φ ∈ Δ.1.prebox, □φ ∉ Γ.1) -infix:80 " < " => ILSuccessor +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}) (Γ Δ : MaximalConsistentSet 𝓢 Φ) extends Γ < Δ where +structure ILCriticalSuccessor (χ : { χ : Formula α // χ ∈ Φ.1}) (Γ Δ : { Γ : ComplementMaximalConsistentFinset 𝓢 Φ.1 // Γ.1 ⊆ Φ.1 }) extends Γ ≺ Δ where prop3 : ∀ φ, φ ▷ χ.1 ∈ Γ.1 → -φ ∈ Δ.1 ∧ □-φ ∈ Δ.1 -notation Γ:max " <[" χ "] " Δ:max => ILCriticalSuccessor χ Γ Δ +notation Γ:max " ≺[" χ "] " Δ:max => ILCriticalSuccessor χ Γ Δ -lemma claim1 (hΓΔ : Γ <[χ] Δ) (hΔΘ : Δ < Θ) : Γ <[χ] Θ where +lemma claim1 (hΓΔ : Γ ≺[χ] Δ) (hΔΘ : Δ ≺ Θ) : Γ ≺[χ] Θ where prop1 := by intro φ hφ; apply hΔΘ.prop1 φ; @@ -595,22 +671,48 @@ lemma claim1 (hΓΔ : Γ <[χ] Δ) (hΔΘ : Δ < Θ) : Γ <[χ] Θ where apply hΔΘ.prop1; simpa; -lemma claim3 (h₁ : ∼(φ ▷ χ.1) ∈ Γ.1) : ∃ Δ : MaximalConsistentSet 𝓢 Φ, (Γ <[χ] Δ) ∧ φ ∈ Δ.1 := by - have : (φ ▷ χ.1) ∈ Φ.1 := Φ.2.compl_closed (∼(φ ▷ χ.1)) $ Γ.2.1 h₁; +open LO.InterpretabilityLogic.Entailment +open LO.Entailment in +open LO.Modal.Entailment in + +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; - sorry; + 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 Δ₀ : FormulaFinset _ := {φ, □-φ} ∪ - Γ.1.prebox ∪ - Γ.1.prebox.box ∪ - ((Γ.1.preimage (λ ξ => ξ ▷ χ.1) (by simp)) |>.image (λ ξ => -ξ)) ∪ - ((Γ.1.preimage (λ ξ => ξ ▷ χ.1) (by simp)) |>.image (λ ξ => □-ξ)) - have Δ₀_consis : Δ₀.Consistent 𝓢 := by sorry; - obtain ⟨Δ, hΔ⟩ : ∃ Δ : MaximalConsistentSet 𝓢 Φ, Δ₀ ⊆ Δ.1 := by + Γ.1.1.prebox ∪ + Γ.1.1.prebox.box ∪ + ((Γ.1.1.preimage (λ ξ => ξ ▷ χ.1) (by simp)) |>.image (λ ξ => -ξ)) ∪ + ((Γ.1.1.preimage (λ ξ => ξ ▷ χ.1) (by simp)) |>.image (λ ξ => □-ξ)) + have Δ₀_consis : Δ₀.Consistent 𝓢 := by + by_contra!; + obtain ⟨Θ, hΘ₁, hΘ₂⟩ := def_inconsistent.mp this; sorry; - use Δ; + have Δ₀_cs : ComplementBounded Δ₀ Φ.1 := by + intro ψ hψ; + simp [Δ₀] at hψ; + rcases hψ with rfl | rfl | hψ | ⟨ψ, hψ, rfl⟩ | ⟨ψ, hψ, rfl⟩ | ⟨ψ, hψ, rfl⟩ <;> + simp only [Finset.mem_union, Finset.mem_image]; + . left; have : ∼(ψ ▷ χ) ∈ Φ.1 := Γ.2 h₁; grind; + . left; grind; + . left; have : □ψ ∈ Φ.1 := Γ.2 hψ; grind; + . left; have : □ψ ∈ Φ.1 := Γ.2 hψ; grind; + . sorry; + . sorry; + obtain ⟨Δ, hΔ⟩ : ∃ Δ : ComplementMaximalConsistentFinset 𝓢 Φ.1, Δ₀ ⊆ Δ.1 := ComplementMaximalConsistentFinset.lindenbaum Δ₀_consis Δ₀_cs; + sorry; + /- + use ⟨Δ, by sorry⟩; constructor; . exact { prop1 := by @@ -648,23 +750,24 @@ lemma claim3 (h₁ : ∼(φ ▷ χ.1) ∈ Γ.1) : ∃ Δ : MaximalConsistentSet } . apply hΔ; simp [Δ₀]; + -/ -lemma claim4 (h₁ : (φ ▷ ψ) ∈ Γ.1) (h₂ : φ ∈ Δ.1) (h₃ : Γ <[χ] Δ) - : ∃ Δ' : MaximalConsistentSet 𝓢 Φ, (Γ <[χ] Δ') ∧ ψ ∈ Δ'.1 ∧ □(-ψ) ∈ Δ'.1 := by +lemma claim4 (h₁ : (φ ▷ ψ) ∈ Γ.1) (h₂ : φ ∈ Δ.1) (h₃ : Γ ≺[χ] Δ) + : ∃ Δ', (Γ ≺[χ] Δ') ∧ ψ ∈ Δ'.1 ∧ □(-ψ) ∈ Δ'.1 := by have : □-ψ ∉ Γ.1 := by by_contra hC; sorry; let Δ₀ : FormulaFinset _ := {ψ, □-ψ} ∪ - Γ.1.prebox ∪ - Γ.1.prebox.box ∪ - ((Γ.1.preimage (λ ξ => ξ ▷ χ) (by simp)) |>.image (λ ξ => -ξ)) ∪ - ((Γ.1.preimage (λ ξ => ξ ▷ χ) (by simp)) |>.image (λ ξ => □-ξ)) + Γ.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Δ⟩ : ∃ Δ : MaximalConsistentSet 𝓢 Φ, Δ₀ ⊆ Δ.1 := by + obtain ⟨Δ, hΔ⟩ : ∃ Δ : ComplementMaximalConsistentFinset 𝓢 Φ.1, Δ₀ ⊆ Δ.1 := by sorry; - use Δ; + use ⟨Δ, by sorry⟩; refine ⟨?_, ?_, ?_⟩; . exact { prop1 := by @@ -709,20 +812,23 @@ open Veltman namespace Veltman +open LO.CCMF + variable {α : Type*} [DecidableEq α] variable [Entailment S (Formula ℕ)] -variable {𝓢 : S} {Γ : MaximalConsistentSet 𝓢 Φ} +variable {Φ : AdequateSet _} {𝓢 : S} {Γ : { Γ : ComplementMaximalConsistentFinset 𝓢 Φ.1 // Γ.1 ⊆ Φ.1 }} -protected inductive ILMiniCanonicalModel.IsWorld (Γ : MaximalConsistentSet 𝓢 Φ) : MaximalConsistentSet 𝓢 Φ → List { φ // φ ∈ Φ.1 } → Prop - | i₁ : ILMiniCanonicalModel.IsWorld Γ Γ [] - | i₂ {Δ Δ'} {τ} : ILMiniCanonicalModel.IsWorld Γ Δ τ → Δ < Δ' → ILMiniCanonicalModel.IsWorld Γ Δ' τ - | i₃ {Δ Δ'} {τ χ} : ILMiniCanonicalModel.IsWorld Γ Δ τ → Δ <[χ] Δ' → ILMiniCanonicalModel.IsWorld Γ Δ' (τ ++ [χ]) +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 (Γ : MaximalConsistentSet 𝓢 Φ) : Veltman.Model where +def ILMiniCanonicalModel (Γ : { Γ : ComplementMaximalConsistentFinset 𝓢 Φ.1 // Γ.1 ⊆ Φ.1 }) : Veltman.Model where toKripkeFrame := { - World := { P : (MaximalConsistentSet 𝓢 Φ) × (List _) // ILMiniCanonicalModel.IsWorld Γ P.1 P.2 } + 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 ++ [χ] ++ τ) + Rel X Y := ∃ χ, X.1.1 ≺[χ] Y.1.1 ∧ (∃ τ, Y.1.2 = X.1.2 ++ [χ] ++ τ) } S X U V := X ≺ U.1 ∧ @@ -731,7 +837,6 @@ def ILMiniCanonicalModel (Γ : MaximalConsistentSet 𝓢 Φ) : Veltman.Model whe Val X p := (.atom p) ∈ X.1.1.1 instance : (ILMiniCanonicalModel Γ).IsFiniteGL where - world_finite := by sorry trans X Y Z := by rintro ⟨χ₁, RXY, ⟨τ₁, hτ₁⟩⟩ ⟨χ₂, RYZ, ⟨τ₂, hτ₂⟩⟩; use χ₁; @@ -742,6 +847,9 @@ instance : (ILMiniCanonicalModel Γ).IsFiniteGL where irrefl := by rintro _ ⟨_, _, ⟨_, hτ⟩⟩; simp at hτ; + world_finite := by + simp [ILMiniCanonicalModel]; + sorry instance : (ILMiniCanonicalModel Γ).IsIL where S_refl X := by @@ -766,7 +874,7 @@ instance : (ILMiniCanonicalModel Γ).IsFiniteIL where open Formula.Veltman -lemma ILMiniCanonicalModel.truthlemma {X : ILMiniCanonicalModel Γ} (hφ : φ ∈ Φ.1) : X ⊧ φ ↔ φ ∈ X.1.1.1 := by +lemma ILMiniCanonicalModel.truthlemma [Entailment.IL 𝓢] {X : ILMiniCanonicalModel Γ} (hφ : φ ∈ Φ.1) : X ⊧ φ ↔ φ ∈ X.1.1.1 := by induction φ generalizing X with | hfalsum => sorry; | hatom a => tauto; @@ -810,6 +918,7 @@ lemma ILMiniCanonicalModel.truthlemma {X : ILMiniCanonicalModel Γ} (hφ : φ end Veltman +open LO.CCMF open Formula.Veltman in instance IL.Veltman.finite_complete : Complete InterpretabilityLogic.IL Veltman.FrameClass.FiniteIL := by constructor; @@ -818,12 +927,15 @@ instance IL.Veltman.finite_complete : Complete InterpretabilityLogic.IL Veltman. intro hφ; apply not_validOnFrameClass_of_exists_model_world; let Φ : AdequateSet ℕ := ⟨{-φ}, by sorry⟩ - obtain ⟨Γ, hΓ⟩ : ∃ Γ : MaximalConsistentSet (InterpretabilityLogic.IL) Φ, {-φ} ⊆ Γ.1 := by sorry; - use ILMiniCanonicalModel Γ, ⟨⟨Γ, []⟩, ILMiniCanonicalModel.IsWorld.i₁⟩; + obtain ⟨Γ, hΓ⟩ : ∃ Γ : ComplementMaximalConsistentFinset (InterpretabilityLogic.IL) Φ.1, {-φ} ⊆ Γ.1 := ComplementMaximalConsistentFinset.lindenbaum + (by sorry) + (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 From 46be91773866d2a477449976e02c7db64b4be214 Mon Sep 17 00:00:00 2001 From: SnO2WMaN Date: Fri, 31 Oct 2025 01:33:07 +0900 Subject: [PATCH 4/8] wip --- .../Veltman/Logic/IL/Completeness.lean | 54 ++++++++----------- 1 file changed, 21 insertions(+), 33 deletions(-) diff --git a/Foundation/InterpretabilityLogic/Veltman/Logic/IL/Completeness.lean b/Foundation/InterpretabilityLogic/Veltman/Logic/IL/Completeness.lean index a52916784..9d035ef9e 100644 --- a/Foundation/InterpretabilityLogic/Veltman/Logic/IL/Completeness.lean +++ b/Foundation/InterpretabilityLogic/Veltman/Logic/IL/Completeness.lean @@ -87,10 +87,10 @@ lemma def_inconsistent [Entailment.Minimal 𝓢] : Inconsistent 𝓢 Γ ↔ ∃ def Maximal (𝓢 : S) (Γ : Finset F) : Prop := ∀ Δ, Γ ⊂ Δ → Inconsistent 𝓢 Δ -def ComplementBounded [Compl F] (Γ Φ : Finset F) : Prop := Γ ⊆ (Φ ∪ Φ.image (-·)) +def ComplementSubset [Compl F] (Γ Δ : Finset F) : Prop := Γ ⊆ (Δ ∪ Δ.image (-·)) /-- For every `φ` in `Δ`, `φ` or `-φ` is in `Γ` -/ -def ComplementMaximal [Compl F] (Γ Φ : Finset F) : Prop := ∀ φ ∈ Φ, φ ∈ Γ ∨ -φ ∈ Γ +def ComplementMaximal [Compl F] (Γ Δ : Finset F) : Prop := ∀ φ ∈ Δ, φ ∈ Γ ∨ -φ ∈ Γ section @@ -273,17 +273,18 @@ end exists_consistent_complementary_closed open exists_consistent_complementary_closed in -theorem exists_consistent_complement_maximal [Compl F] [ComplEquiv 𝓢] [Entailment.Cl 𝓢] - (Γ_consis : Consistent 𝓢 Γ) (Γ_bounded : ComplementBounded Γ Φ) - : ∃ Γ', (Γ ⊆ Γ') ∧ (Consistent 𝓢 Γ') ∧ (ComplementBounded Γ' Φ) ∧ (ComplementMaximal Γ' Φ) := by - use enum 𝓢 Γ Φ.toList; +theorem exists_consistent_complement_maximal {Ξ : Finset F} [Compl F] [ComplEquiv 𝓢] [Entailment.Cl 𝓢] + (Γ_consis : Consistent 𝓢 Γ) + (subset_ΓΔ : ComplementSubset Γ Ξ) + : ∃ Γ', (Γ ⊆ Γ') ∧ (Consistent 𝓢 Γ') ∧ (ComplementSubset Γ' Ξ) ∧ (ComplementMaximal Γ' Ξ) := by + use enum 𝓢 Γ Ξ.toList; refine ⟨?_, ?_, ?_, ?_⟩; . simp; . grind; . intro φ hφ; simp only [Finset.mem_union, Finset.mem_image]; rcases of_mem_enum hφ with (hφ | hφ | ⟨ψ, hψ, rfl⟩); - . dsimp [ComplementBounded] at Γ_bounded + . dsimp [ComplementSubset] at subset_ΓΔ grind; . left; simpa using hφ; @@ -300,7 +301,7 @@ section variable [Compl F] {Φ : Finset F} -abbrev ComplementMaximalConsistentFinset (𝓢 : S) (Φ : Finset F) := { Γ : Finset F // (Consistent 𝓢 Γ) ∧ (ComplementBounded Γ Φ) ∧ (ComplementMaximal Γ Φ) } +abbrev ComplementMaximalConsistentFinset (𝓢 : S) (Φ : Finset F) := { Γ : Finset F // (Consistent 𝓢 Γ) ∧ (ComplementSubset Γ Φ) ∧ (ComplementMaximal Γ Φ) } variable {Γ Γ₁ Γ₂ Δ : ComplementMaximalConsistentFinset 𝓢 Φ} {φ ψ : F} @@ -332,11 +333,10 @@ lemma equality_def : Γ₁ = Γ₂ ↔ Γ₁.1 = Γ₂.1 := by variable [Entailment.ComplEquiv 𝓢] [Entailment.Cl 𝓢] -theorem lindenbaum {Γ : Finset F} (Γ_consis : Consistent 𝓢 Γ) (Γ_bounded : ComplementBounded Γ Φ) +theorem lindenbaum {Γ : Finset F} (Γ_consis : Consistent 𝓢 Γ) (X_sub : ComplementSubset Γ Φ) : ∃ Γ' : ComplementMaximalConsistentFinset 𝓢 Φ, Γ ⊆ Γ'.1 := by - obtain ⟨Γ', ⟨_, _⟩⟩ := exists_consistent_complement_maximal Γ_consis Γ_bounded; - use ⟨Γ', ?_⟩; - assumption; + obtain ⟨Y, ⟨_, _, _⟩⟩ := exists_consistent_complement_maximal Γ_consis X_sub; + use ⟨Y, (by assumption), (by assumption)⟩; noncomputable instance [Entailment.Consistent 𝓢] : Inhabited (ComplementMaximalConsistentFinset 𝓢 Φ) := ⟨lindenbaum (Γ := ∅) (by simp) (by tauto) |>.choose⟩ @@ -696,19 +696,10 @@ lemma claim3 [Entailment.IL 𝓢] (h₁ : ∼(φ ▷ χ.1) ∈ Γ.1) : ∃ Δ, ( ((Γ.1.1.preimage (λ ξ => ξ ▷ χ.1) (by simp)) |>.image (λ ξ => □-ξ)) have Δ₀_consis : Δ₀.Consistent 𝓢 := by by_contra!; - obtain ⟨Θ, hΘ₁, hΘ₂⟩ := def_inconsistent.mp this; + + sorry; + have Δ₀_cs : ComplementSubset Δ₀ Φ.1 := by sorry; - have Δ₀_cs : ComplementBounded Δ₀ Φ.1 := by - intro ψ hψ; - simp [Δ₀] at hψ; - rcases hψ with rfl | rfl | hψ | ⟨ψ, hψ, rfl⟩ | ⟨ψ, hψ, rfl⟩ | ⟨ψ, hψ, rfl⟩ <;> - simp only [Finset.mem_union, Finset.mem_image]; - . left; have : ∼(ψ ▷ χ) ∈ Φ.1 := Γ.2 h₁; grind; - . left; grind; - . left; have : □ψ ∈ Φ.1 := Γ.2 hψ; grind; - . left; have : □ψ ∈ Φ.1 := Γ.2 hψ; grind; - . sorry; - . sorry; obtain ⟨Δ, hΔ⟩ : ∃ Δ : ComplementMaximalConsistentFinset 𝓢 Φ.1, Δ₀ ⊆ Δ.1 := ComplementMaximalConsistentFinset.lindenbaum Δ₀_consis Δ₀_cs; sorry; /- @@ -818,15 +809,14 @@ 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 Γ ⟨Δ', (τ ++ [χ])⟩ +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 := { P : _ × _ // ILMiniCanonicalModel.IsWorld Γ P.1 P.2 } world_nonempty := ⟨⟨(Γ, []), ILMiniCanonicalModel.IsWorld.i₁⟩⟩ Rel X Y := ∃ χ, X.1.1 ≺[χ] Y.1.1 ∧ (∃ τ, Y.1.2 = X.1.2 ++ [χ] ++ τ) } @@ -837,6 +827,7 @@ def ILMiniCanonicalModel (Γ : { Γ : ComplementMaximalConsistentFinset 𝓢 Φ. Val X p := (.atom p) ∈ X.1.1.1 instance : (ILMiniCanonicalModel Γ).IsFiniteGL where + world_finite := by sorry trans X Y Z := by rintro ⟨χ₁, RXY, ⟨τ₁, hτ₁⟩⟩ ⟨χ₂, RYZ, ⟨τ₂, hτ₂⟩⟩; use χ₁; @@ -847,9 +838,6 @@ instance : (ILMiniCanonicalModel Γ).IsFiniteGL where irrefl := by rintro _ ⟨_, _, ⟨_, hτ⟩⟩; simp at hτ; - world_finite := by - simp [ILMiniCanonicalModel]; - sorry instance : (ILMiniCanonicalModel Γ).IsIL where S_refl X := by From 6e1027af395c5ffeadf90e30d40e2f43e1f195bc Mon Sep 17 00:00:00 2001 From: SnO2WMaN Date: Fri, 31 Oct 2025 16:48:29 +0900 Subject: [PATCH 5/8] move --- .../Veltman/Logic/IL/Completeness.lean | 175 ++++---- Foundation/Logic/CCCF.lean | 388 ++++++++++++++++++ 2 files changed, 489 insertions(+), 74 deletions(-) create mode 100644 Foundation/Logic/CCCF.lean diff --git a/Foundation/InterpretabilityLogic/Veltman/Logic/IL/Completeness.lean b/Foundation/InterpretabilityLogic/Veltman/Logic/IL/Completeness.lean index 9d035ef9e..ba1620e33 100644 --- a/Foundation/InterpretabilityLogic/Veltman/Logic/IL/Completeness.lean +++ b/Foundation/InterpretabilityLogic/Veltman/Logic/IL/Completeness.lean @@ -53,7 +53,7 @@ end Entailment -namespace CCMF +namespace CCCF open LO.Entailment LO.Entailment.Context LO.Modal.Entailment @@ -87,10 +87,10 @@ lemma def_inconsistent [Entailment.Minimal 𝓢] : Inconsistent 𝓢 Γ ↔ ∃ def Maximal (𝓢 : S) (Γ : Finset F) : Prop := ∀ Δ, Γ ⊂ Δ → Inconsistent 𝓢 Δ -def ComplementSubset [Compl F] (Γ Δ : Finset F) : Prop := Γ ⊆ (Δ ∪ Δ.image (-·)) +def ComplementBounded [Compl F] (Γ Φ : Finset F) : Prop := Γ ⊆ (Φ ∪ Φ.image (-·)) /-- For every `φ` in `Δ`, `φ` or `-φ` is in `Γ` -/ -def ComplementMaximal [Compl F] (Γ Δ : Finset F) : Prop := ∀ φ ∈ Δ, φ ∈ Γ ∨ -φ ∈ Γ +def ComplementClosed [Compl F] (Γ Φ : Finset F) : Prop := ∀ φ ∈ Φ, φ ∈ Γ ∨ -φ ∈ Γ section @@ -196,7 +196,7 @@ lemma not_mem_of_mem_compl (Γ_consis : Consistent 𝓢 Γ) (h : -φ ∈ Γ) : end -namespace exists_consistent_complementary_closed +namespace exists_consistent_complement_closed open Classical @@ -269,51 +269,38 @@ lemma consistent_enum (Γ_consis : Consistent 𝓢 Γ) : Consistent 𝓢 (Γ[l]) end -end exists_consistent_complementary_closed +end exists_consistent_complement_closed -open exists_consistent_complementary_closed in -theorem exists_consistent_complement_maximal {Ξ : Finset F} [Compl F] [ComplEquiv 𝓢] [Entailment.Cl 𝓢] - (Γ_consis : Consistent 𝓢 Γ) - (subset_ΓΔ : ComplementSubset Γ Ξ) - : ∃ Γ', (Γ ⊆ Γ') ∧ (Consistent 𝓢 Γ') ∧ (ComplementSubset Γ' Ξ) ∧ (ComplementMaximal Γ' Ξ) := by - use enum 𝓢 Γ Ξ.toList; - refine ⟨?_, ?_, ?_, ?_⟩; +open exists_consistent_complement_closed in +theorem exists_consistent_complement_closed [Compl F] [ComplEquiv 𝓢] [Entailment.Cl 𝓢] (Γ_consis : Consistent 𝓢 Γ) + : ∃ Γ', (Γ ⊆ Γ') ∧ (Consistent 𝓢 Γ') ∧ (ComplementClosed Γ' Φ) := by + use enum 𝓢 Γ Φ.toList; + refine ⟨?_, ?_, ?_⟩; . simp; . grind; - . intro φ hφ; - simp only [Finset.mem_union, Finset.mem_image]; - rcases of_mem_enum hφ with (hφ | hφ | ⟨ψ, hψ, rfl⟩); - . dsimp [ComplementSubset] at subset_ΓΔ - grind; - . left; - simpa using hφ; - . right; - use ψ; - constructor; - . simpa using hψ; - . rfl . intro φ hφ; apply of_mem_seed; simpa; section +omit [DecidableEq F] variable [Compl F] {Φ : Finset F} -abbrev ComplementMaximalConsistentFinset (𝓢 : S) (Φ : Finset F) := { Γ : Finset F // (Consistent 𝓢 Γ) ∧ (ComplementSubset Γ Φ) ∧ (ComplementMaximal Γ Φ) } +abbrev ConsistentComplementClosedFinset (𝓢 : S) (Φ : Finset F) := { Γ : Finset F // (Consistent 𝓢 Γ) ∧ (ComplementClosed Γ Φ) } -variable {Γ Γ₁ Γ₂ Δ : ComplementMaximalConsistentFinset 𝓢 Φ} {φ ψ : F} +variable {Γ Γ₁ Γ₂ Δ : ConsistentComplementClosedFinset 𝓢 Φ} {φ ψ : F} -namespace ComplementMaximalConsistentFinset +namespace ConsistentComplementClosedFinset -instance : Membership (F) (ComplementMaximalConsistentFinset 𝓢 Φ) := ⟨λ X φ => φ ∈ X.1⟩ +instance : Membership (F) (ConsistentComplementClosedFinset 𝓢 Φ) := ⟨λ X φ => φ ∈ X.1⟩ -@[simp] lemma consistent (Γ : ComplementMaximalConsistentFinset 𝓢 Φ) : Consistent 𝓢 Γ := Γ.2.1 +@[simp] lemma consistent (Γ : ConsistentComplementClosedFinset 𝓢 Φ) : Consistent 𝓢 Γ := Γ.2.1 @[simp] lemma unprovable_falsum : Γ.1 *⊬[𝓢] ⊥ := Γ.consistent -@[simp, grind] lemma mem_falsum [Entailment.Cl 𝓢] : ⊥ ∉ Γ := not_mem_falsum (consistent Γ) +@[simp, grind] lemma mem_falsum [DecidableEq F] [Entailment.Cl 𝓢] : ⊥ ∉ Γ := not_mem_falsum (consistent Γ) -@[simp] lemma maximal (Γ : ComplementMaximalConsistentFinset 𝓢 Φ) : ComplementMaximal Γ Φ := Γ.2.2.2 +@[simp] lemma maximal (Γ : ConsistentComplementClosedFinset 𝓢 Φ) : ComplementClosed Γ Φ := Γ.2.2 @[grind] lemma mem_compl_of_not_mem (hs : ψ ∈ Φ) : ψ ∉ Γ → -ψ ∈ Γ := by @@ -333,12 +320,15 @@ lemma equality_def : Γ₁ = Γ₂ ↔ Γ₁.1 = Γ₂.1 := by variable [Entailment.ComplEquiv 𝓢] [Entailment.Cl 𝓢] -theorem lindenbaum {Γ : Finset F} (Γ_consis : Consistent 𝓢 Γ) (X_sub : ComplementSubset Γ Φ) - : ∃ Γ' : ComplementMaximalConsistentFinset 𝓢 Φ, Γ ⊆ Γ'.1 := by - obtain ⟨Y, ⟨_, _, _⟩⟩ := exists_consistent_complement_maximal Γ_consis X_sub; - use ⟨Y, (by assumption), (by assumption)⟩; +theorem lindenbaum [DecidableEq F] {Γ : Finset F} (Γ_consis : Consistent 𝓢 Γ) + : ∃ Γ' : ConsistentComplementClosedFinset 𝓢 Φ, Γ ⊆ Γ'.1 := by + obtain ⟨Γ', ⟨_, _⟩⟩ := exists_consistent_complement_closed Γ_consis; + use ⟨Γ', ?_⟩; + assumption; -noncomputable instance [Entailment.Consistent 𝓢] : Inhabited (ComplementMaximalConsistentFinset 𝓢 Φ) := ⟨lindenbaum (Γ := ∅) (by simp) (by tauto) |>.choose⟩ +noncomputable instance [DecidableEq F] [Entailment.Consistent 𝓢] : Inhabited (ConsistentComplementClosedFinset 𝓢 Φ) := ⟨lindenbaum (Γ := ∅) (by simp) |>.choose⟩ + +variable [DecidableEq F] @[grind] lemma membership_iff (hξ : φ ∈ Φ) : (φ ∈ Γ) ↔ (Γ *⊢[𝓢] φ) := by @@ -393,11 +383,11 @@ lemma iff_mem_imp (hφψΦ : (φ ➝ ψ) ∈ Φ) (hφΦ : φ ∈ Φ) (hψΦ : ψ apply membership_iff hψΦ |>.mp; assumption; -end ComplementMaximalConsistentFinset +end ConsistentComplementClosedFinset end -end CCMF +end CCCF end LO @@ -637,18 +627,18 @@ variable {Φ : AdequateSet α} end AdequateSet -open LO.CCMF +open LO.CCCF -- def MaximalConsistentSet (𝓢 : S) (Φ : AdequateSet α) := { Ψ : FormulaFinset α // Ψ ⊆ Φ.1 ∧ Ψ.Maximal 𝓢 ∧ Ψ.Consistent 𝓢 } -variable {Φ : AdequateSet α} {Γ Δ Θ : { Γ : ComplementMaximalConsistentFinset 𝓢 Φ.1 // Γ.1 ⊆ Φ.1 }} +variable {Φ : AdequateSet α} {Γ Δ Θ : { Γ : ConsistentComplementClosedFinset 𝓢 Φ.1 // Γ.1 ⊆ Φ.1 }} -structure ILSuccessor (Γ Δ : { Γ : ComplementMaximalConsistentFinset 𝓢 Φ.1 // Γ.1 ⊆ Φ.1 }) : Prop where +structure ILSuccessor (Γ Δ : { Γ : ConsistentComplementClosedFinset 𝓢 Φ.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 +structure ILCriticalSuccessor (χ : { χ : Formula α // χ ∈ Φ.1}) (Γ Δ : { Γ : ConsistentComplementClosedFinset 𝓢 Φ.1 // Γ.1 ⊆ Φ.1 }) extends Γ ≺ Δ where prop3 : ∀ φ, φ ▷ χ.1 ∈ Γ.1 → -φ ∈ Δ.1 ∧ □-φ ∈ Δ.1 notation Γ:max " ≺[" χ "] " Δ:max => ILCriticalSuccessor χ Γ Δ @@ -672,35 +662,72 @@ lemma claim1 (hΓΔ : Γ ≺[χ] Δ) (hΔΘ : Δ ≺ Θ) : Γ ≺[χ] Θ where simpa; open LO.InterpretabilityLogic.Entailment -open LO.Entailment in -open LO.Modal.Entailment in +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; + replace hC : Γ *⊢[𝓢] □-φ := ConsistentComplementClosedFinset.membership_iff (by simpa) |>.mp hC; + apply ConsistentComplementClosedFinset.iff_mem_compl (by simpa) |>.mpr $ Formula.complement.rhd_def ▸ h₁; + apply ConsistentComplementClosedFinset.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 Δ₀ : FormulaFinset _ := - {φ, □-φ} ∪ - Γ.1.1.prebox ∪ - Γ.1.1.prebox.box ∪ - ((Γ.1.1.preimage (λ ξ => ξ ▷ χ.1) (by simp)) |>.image (λ ξ => -ξ)) ∪ - ((Γ.1.1.preimage (λ ξ => ξ ▷ χ.1) (by simp)) |>.image (λ ξ => □-ξ)) - have Δ₀_consis : Δ₀.Consistent 𝓢 := by + 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!; - - sorry; - have Δ₀_cs : ComplementSubset Δ₀ Φ.1 := by - sorry; - obtain ⟨Δ, hΔ⟩ : ∃ Δ : ComplementMaximalConsistentFinset 𝓢 Φ.1, Δ₀ ⊆ Δ.1 := ComplementMaximalConsistentFinset.lindenbaum Δ₀_consis Δ₀_cs; + 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Ω⟩ : ∃ Ω : ConsistentComplementClosedFinset 𝓢 Φ.1, Δ ⊆ Ω.1 := ConsistentComplementClosedFinset.lindenbaum Δ_consis; sorry; /- use ⟨Δ, by sorry⟩; @@ -756,7 +783,7 @@ lemma claim4 (h₁ : (φ ▷ ψ) ∈ Γ.1) (h₂ : φ ∈ Δ.1) (h₃ : Γ ≺[ ((Γ.1.1.preimage (λ ξ => ξ ▷ χ) (by simp)) |>.image (λ ξ => □-ξ)) have Δ₀_consis : Δ₀.Consistent 𝓢 := by sorry; - obtain ⟨Δ, hΔ⟩ : ∃ Δ : ComplementMaximalConsistentFinset 𝓢 Φ.1, Δ₀ ⊆ Δ.1 := by + obtain ⟨Δ, hΔ⟩ : ∃ Δ : ConsistentComplementClosedFinset 𝓢 Φ.1, Δ₀ ⊆ Δ.1 := by sorry; use ⟨Δ, by sorry⟩; refine ⟨?_, ?_, ?_⟩; @@ -803,20 +830,21 @@ open Veltman namespace Veltman -open LO.CCMF +open LO.CCCF variable {α : Type*} [DecidableEq α] variable [Entailment S (Formula ℕ)] -variable {Φ : AdequateSet _} {𝓢 : S} {Γ : { Γ : ComplementMaximalConsistentFinset 𝓢 Φ.1 // Γ.1 ⊆ Φ.1 }} +variable {Φ : AdequateSet _} {𝓢 : S} {Γ : { Γ : ConsistentComplementClosedFinset 𝓢 Φ.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 Γ Δ' (τ ++ [χ]) +protected inductive ILMiniCanonicalModel.IsWorld (Γ : { Γ : ConsistentComplementClosedFinset 𝓢 Φ.1 // Γ.1 ⊆ Φ.1 }) + : { Γ : ConsistentComplementClosedFinset 𝓢 Φ.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 +def ILMiniCanonicalModel (Γ : { Γ : ConsistentComplementClosedFinset 𝓢 Φ.1 // Γ.1 ⊆ Φ.1 }) : Veltman.Model where toKripkeFrame := { - World := { P : _ × _ // ILMiniCanonicalModel.IsWorld Γ P.1 P.2 } + 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 ++ [χ] ++ τ) } @@ -827,7 +855,6 @@ def ILMiniCanonicalModel (Γ : { Γ : ComplementMaximalConsistentFinset 𝓢 Φ. Val X p := (.atom p) ∈ X.1.1.1 instance : (ILMiniCanonicalModel Γ).IsFiniteGL where - world_finite := by sorry trans X Y Z := by rintro ⟨χ₁, RXY, ⟨τ₁, hτ₁⟩⟩ ⟨χ₂, RYZ, ⟨τ₂, hτ₂⟩⟩; use χ₁; @@ -838,6 +865,9 @@ instance : (ILMiniCanonicalModel Γ).IsFiniteGL where irrefl := by rintro _ ⟨_, _, ⟨_, hτ⟩⟩; simp at hτ; + world_finite := by + simp [ILMiniCanonicalModel]; + sorry instance : (ILMiniCanonicalModel Γ).IsIL where S_refl X := by @@ -870,7 +900,6 @@ lemma ILMiniCanonicalModel.truthlemma [Entailment.IL 𝓢] {X : ILMiniCanonicalM 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ψ => @@ -906,7 +935,7 @@ lemma ILMiniCanonicalModel.truthlemma [Entailment.IL 𝓢] {X : ILMiniCanonicalM end Veltman -open LO.CCMF +open LO.CCCF open Formula.Veltman in instance IL.Veltman.finite_complete : Complete InterpretabilityLogic.IL Veltman.FrameClass.FiniteIL := by constructor; @@ -915,9 +944,7 @@ instance IL.Veltman.finite_complete : Complete InterpretabilityLogic.IL Veltman. intro hφ; apply not_validOnFrameClass_of_exists_model_world; let Φ : AdequateSet ℕ := ⟨{-φ}, by sorry⟩ - obtain ⟨Γ, hΓ⟩ : ∃ Γ : ComplementMaximalConsistentFinset (InterpretabilityLogic.IL) Φ.1, {-φ} ⊆ Γ.1 := ComplementMaximalConsistentFinset.lindenbaum - (by sorry) - (by sorry) + obtain ⟨Γ, hΓ⟩ : ∃ Γ : ConsistentComplementClosedFinset (InterpretabilityLogic.IL) Φ.1, {-φ} ⊆ Γ.1 := ConsistentComplementClosedFinset.lindenbaum (by sorry) use ILMiniCanonicalModel ⟨Γ, by sorry⟩, ⟨⟨⟨Γ, _⟩, []⟩, ILMiniCanonicalModel.IsWorld.i₁⟩; constructor; . apply Set.mem_setOf_eq.mpr; diff --git a/Foundation/Logic/CCCF.lean b/Foundation/Logic/CCCF.lean new file mode 100644 index 000000000..50ffeaa88 --- /dev/null +++ b/Foundation/Logic/CCCF.lean @@ -0,0 +1,388 @@ +import Foundation.Logic.HilbertStyle.Supplemental + + +namespace LO + +class Compl (F : Type*) [Tilde F] where + compl : F → F + +prefix:120 "-" => Compl.compl + + + +namespace Entailment + +class ComplEquiv [LogicalConnective F] [Compl F] [Entailment S F] (𝓢 : S) where + compl_equiv! {φ : F} : 𝓢 ⊢! ∼φ ⭤ -φ +export ComplEquiv (compl_equiv!) + + +section + +variable {F S : Type*} [LogicalConnective F] [Compl F] [Entailment S F] + {𝓢 : S} {φ : F} [ComplEquiv 𝓢] + +@[simp] lemma compl_equiv : 𝓢 ⊢ ∼φ ⭤ -φ := ⟨compl_equiv!⟩ + + +variable [Entailment.Minimal 𝓢] + +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 + + + +namespace CCCF + +open LO.Entailment LO.Entailment.Context + + +variable {F} [LogicalConnective F] [DecidableEq F] + {S} [Entailment S F] +variable {𝓢 : S} {Γ Δ : Finset F} {φ ψ : F} + +def Consistent (𝓢 : S) (Γ : 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; + + +def Inconsistent (𝓢 : S) (Γ : Finset F) : Prop := ¬(Consistent 𝓢 Γ) + +lemma def_inconsistent [Entailment.Minimal 𝓢] : Inconsistent 𝓢 Γ ↔ ∃ Δ : Finset F, (Δ ⊆ Γ) ∧ (Δ *⊢[𝓢] ⊥) := by + rw [Inconsistent, def_consistent]; + push_neg; + simp; + + +def Maximal (𝓢 : S) (Γ : Finset F) : Prop := ∀ Δ, Γ ⊂ Δ → Inconsistent 𝓢 Δ + +def ComplementBounded [Compl F] (Γ Φ : Finset F) : Prop := Γ ⊆ (Φ ∪ Φ.image (-·)) + +/-- For every `φ` in `Δ`, `φ` or `-φ` is in `Γ` -/ +def ComplementClosed [Compl F] (Γ Φ : Finset F) : Prop := ∀ φ ∈ Φ, φ ∈ Γ ∨ -φ ∈ Γ + + +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; + +end + + +section + +variable [Compl F] [Entailment.Cl 𝓢] [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 + + +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 𝓢 Γ') ∧ (ComplementClosed Γ' Φ) := by + use enum 𝓢 Γ Φ.toList; + refine ⟨?_, ?_, ?_⟩; + . simp; + . grind; + . intro φ hφ; + apply of_mem_seed; + simpa; + +section + +omit [DecidableEq F] +variable [Compl F] {Φ : Finset F} + +abbrev ConsistentComplementClosedFinset (𝓢 : S) (Φ : Finset F) := { Γ : Finset F // (Consistent 𝓢 Γ) ∧ (ComplementClosed Γ Φ) } + +variable {Γ Γ₁ Γ₂ Δ : ConsistentComplementClosedFinset 𝓢 Φ} {φ ψ : F} + +namespace ConsistentComplementClosedFinset + +instance : Membership (F) (ConsistentComplementClosedFinset 𝓢 Φ) := ⟨λ X φ => φ ∈ X.1⟩ + +@[simp] lemma consistent (Γ : ConsistentComplementClosedFinset 𝓢 Φ) : 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 (Γ : ConsistentComplementClosedFinset 𝓢 Φ) : ComplementClosed Γ Φ := Γ.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 𝓢 Γ) + : ∃ Γ' : ConsistentComplementClosedFinset 𝓢 Φ, Γ ⊆ Γ'.1 := by + obtain ⟨Γ', ⟨_, _⟩⟩ := exists_consistent_complement_closed Γ_consis; + use ⟨Γ', ?_⟩; + assumption; + +noncomputable instance [DecidableEq F] [Entailment.Consistent 𝓢] : Inhabited (ConsistentComplementClosedFinset 𝓢 Φ) := ⟨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 ConsistentComplementClosedFinset + +end + +end CCCF + +end LO From b2fbcedcbc77e2852180fb0dd653b23cbe36e299 Mon Sep 17 00:00:00 2001 From: SnO2WMaN Date: Fri, 31 Oct 2025 20:37:50 +0900 Subject: [PATCH 6/8] MCS propositional --- Foundation/Propositional/MCS.lean | 319 ++++++++++++++++++++++++++++++ 1 file changed, 319 insertions(+) create mode 100644 Foundation/Propositional/MCS.lean diff --git a/Foundation/Propositional/MCS.lean b/Foundation/Propositional/MCS.lean new file mode 100644 index 000000000..8caf61029 --- /dev/null +++ b/Foundation/Propositional/MCS.lean @@ -0,0 +1,319 @@ +/- + Maximal consistent set +-/ +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_not_mem : (∼φ ∈ Γ) ↔ (φ ∉ Γ) := 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_not_mem.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_mem : (∼∼φ ∈ Γ) ↔ (φ ∈ Γ) := 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_not_mem.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_not_mem.mpr hφ; + replace hψ := iff_mem_provable.mp $ iff_mem_neg_not_mem.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]; + +end MaximalConsistentSet + +end LO + +end From 5ec814c344306182643797e4051e6d9b49884ef6 Mon Sep 17 00:00:00 2001 From: SnO2WMaN Date: Fri, 31 Oct 2025 21:05:45 +0900 Subject: [PATCH 7/8] MCS modal --- Foundation/Modal/MCS.lean | 145 ++++++++++++++++++++++++++++++ Foundation/Propositional/MCS.lean | 24 ++--- 2 files changed, 159 insertions(+), 10 deletions(-) create mode 100644 Foundation/Modal/MCS.lean 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/MCS.lean b/Foundation/Propositional/MCS.lean index 8caf61029..e3aa89cd3 100644 --- a/Foundation/Propositional/MCS.lean +++ b/Foundation/Propositional/MCS.lean @@ -1,5 +1,5 @@ /- - Maximal consistent set + Maximal consistent set for propositional classical logic -/ import Foundation.Logic.HilbertStyle.Supplemental import Foundation.Meta.ClProver @@ -232,7 +232,7 @@ lemma iff_mem_provable : φ ∈ Γ ↔ Γ.1 *⊢[𝓢] φ := by @[simp, grind] lemma mem_verum : ⊤ ∈ Γ := by apply iff_mem_provable.mpr; cl_prover; @[grind] -lemma iff_mem_neg_not_mem : (∼φ ∈ Γ) ↔ (φ ∉ Γ) := by +lemma iff_mem_neg : (∼φ ∈ Γ) ↔ (φ ∉ Γ) := by simp only [iff_mem_provable]; constructor; . intro hnφ hφ; @@ -248,7 +248,7 @@ lemma iff_forall_mem_provable : (∀ Γ : MaximalConsistentSet 𝓢, φ ∈ Γ) intro h; obtain ⟨Γ, hΓ⟩ := lindenbaum $ iff_consistent_neg_singleton_unprovable.mpr h; use Γ; - apply iff_mem_neg_not_mem.mp; + apply iff_mem_neg.mp; simpa using hΓ; . intro h Γ; apply iff_mem_provable.mpr; @@ -256,9 +256,9 @@ lemma iff_forall_mem_provable : (∀ Γ : MaximalConsistentSet 𝓢, φ ∈ Γ) @[grind] lemma mem_of_provable (h : 𝓢 ⊢ φ) : φ ∈ Γ := iff_forall_mem_provable.mpr h Γ -@[grind] lemma iff_mem_negneg_mem : (∼∼φ ∈ Γ) ↔ (φ ∈ Γ) := by grind +@[grind] lemma iff_mem_negneg : (∼∼φ ∈ Γ) ↔ (φ ∈ Γ) := by grind -@[grind] +@[grind ⇒] lemma iff_mem_imp : ((φ ➝ ψ) ∈ Γ) ↔ ((φ ∈ Γ) → (ψ ∈ Γ)) := by constructor; . intro hφψ hφ; @@ -266,7 +266,7 @@ lemma iff_mem_imp : ((φ ➝ ψ) ∈ Γ) ↔ ((φ ∈ Γ) → (ψ ∈ Γ)) := by 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_not_mem.mpr 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; @@ -277,7 +277,7 @@ lemma iff_mem_imp : ((φ ➝ ψ) ∈ Γ) ↔ ((φ ∈ Γ) → (ψ ∈ Γ)) := by @[grind] lemma mdp (hφψ : (φ ➝ ψ) ∈ Γ) (hφ : φ ∈ Γ) : ψ ∈ Γ := iff_mem_imp.mp hφψ hφ -@[grind] +@[grind ⇒] lemma iff_mem_and : ((φ ⋏ ψ) ∈ Γ) ↔ (φ ∈ Γ) ∧ (ψ ∈ Γ) := by constructor; . intro hφψ; @@ -287,15 +287,15 @@ lemma iff_mem_and : ((φ ⋏ ψ) ∈ Γ) ↔ (φ ∈ Γ) ∧ (ψ ∈ Γ) := by rintro ⟨hφ, hψ⟩; cl_prover [hφ, hψ]; -@[grind] +@[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_not_mem.mpr hφ; - replace hψ := iff_mem_provable.mp $ iff_mem_neg_not_mem.mpr 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]; @@ -312,6 +312,10 @@ lemma imp_of_provable_C (hφψ : Γ *⊢[𝓢] (φ ➝ ψ)) : (φ ∈ Γ) → ( 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 From b4ca2546c116f97cf016089771f1bf36275b7154 Mon Sep 17 00:00:00 2001 From: SnO2WMaN Date: Sat, 1 Nov 2025 01:20:30 +0900 Subject: [PATCH 8/8] refactor --- .../InterpretabilityLogic/Formula/Basic.lean | 17 +- .../Formula/Complement.lean | 89 +++ .../Formula/Subformula.lean | 99 +++ .../Veltman/Logic/IL/Completeness.lean | 619 +----------------- .../CCCF.lean => Propositional/CMCF.lean} | 96 +-- 5 files changed, 275 insertions(+), 645 deletions(-) create mode 100644 Foundation/InterpretabilityLogic/Formula/Complement.lean create mode 100644 Foundation/InterpretabilityLogic/Formula/Subformula.lean rename Foundation/{Logic/CCCF.lean => Propositional/CMCF.lean} (86%) 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/Veltman/Logic/IL/Completeness.lean b/Foundation/InterpretabilityLogic/Veltman/Logic/IL/Completeness.lean index ba1620e33..67301c7e6 100644 --- a/Foundation/InterpretabilityLogic/Veltman/Logic/IL/Completeness.lean +++ b/Foundation/InterpretabilityLogic/Veltman/Logic/IL/Completeness.lean @@ -1,400 +1,7 @@ import Foundation.InterpretabilityLogic.Veltman.Logic.IL.Soundness - - -namespace LO - -class Compl (F : Type*) [Tilde F] where - compl : F → F - -prefix:120 "-" => Compl.compl - - - -namespace Entailment - -class ComplEquiv [LogicalConnective F] [Compl F] [Entailment S F] (𝓢 : S) where - compl_equiv! {φ : F} : 𝓢 ⊢! ∼φ ⭤ -φ -export ComplEquiv (compl_equiv!) - - -section - -variable {F S : Type*} [LogicalConnective F] [Compl F] [Entailment S F] - {𝓢 : S} {φ : F} [ComplEquiv 𝓢] - -@[simp] lemma compl_equiv : 𝓢 ⊢ ∼φ ⭤ -φ := ⟨compl_equiv!⟩ - - -section - -variable [Entailment.Minimal 𝓢] - -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 - -end Entailment - - - -namespace CCCF - -open LO.Entailment LO.Entailment.Context LO.Modal.Entailment - - -variable {F} [LogicalConnective F] [DecidableEq F] - {S} [Entailment S F] -variable {𝓢 : S} {Γ Δ : Finset F} {φ ψ : F} - -def Consistent (𝓢 : S) (Γ : 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; - - -def Inconsistent (𝓢 : S) (Γ : Finset F) : Prop := ¬(Consistent 𝓢 Γ) - -lemma def_inconsistent [Entailment.Minimal 𝓢] : Inconsistent 𝓢 Γ ↔ ∃ Δ : Finset F, (Δ ⊆ Γ) ∧ (Δ *⊢[𝓢] ⊥) := by - rw [Inconsistent, def_consistent]; - push_neg; - simp; - - -def Maximal (𝓢 : S) (Γ : Finset F) : Prop := ∀ Δ, Γ ⊂ Δ → Inconsistent 𝓢 Δ - -def ComplementBounded [Compl F] (Γ Φ : Finset F) : Prop := Γ ⊆ (Φ ∪ Φ.image (-·)) - -/-- For every `φ` in `Δ`, `φ` or `-φ` is in `Γ` -/ -def ComplementClosed [Compl F] (Γ Φ : Finset F) : Prop := ∀ φ ∈ Φ, φ ∈ Γ ∨ -φ ∈ Γ - - -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; - -end - - -section - -variable [Compl F] [Entailment.Cl 𝓢] [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 - - -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 𝓢 Γ') ∧ (ComplementClosed Γ' Φ) := by - use enum 𝓢 Γ Φ.toList; - refine ⟨?_, ?_, ?_⟩; - . simp; - . grind; - . intro φ hφ; - apply of_mem_seed; - simpa; - -section - -omit [DecidableEq F] -variable [Compl F] {Φ : Finset F} - -abbrev ConsistentComplementClosedFinset (𝓢 : S) (Φ : Finset F) := { Γ : Finset F // (Consistent 𝓢 Γ) ∧ (ComplementClosed Γ Φ) } - -variable {Γ Γ₁ Γ₂ Δ : ConsistentComplementClosedFinset 𝓢 Φ} {φ ψ : F} - -namespace ConsistentComplementClosedFinset - -instance : Membership (F) (ConsistentComplementClosedFinset 𝓢 Φ) := ⟨λ X φ => φ ∈ X.1⟩ - -@[simp] lemma consistent (Γ : ConsistentComplementClosedFinset 𝓢 Φ) : 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 (Γ : ConsistentComplementClosedFinset 𝓢 Φ) : ComplementClosed Γ Φ := Γ.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 𝓢 Γ) - : ∃ Γ' : ConsistentComplementClosedFinset 𝓢 Φ, Γ ⊆ Γ'.1 := by - obtain ⟨Γ', ⟨_, _⟩⟩ := exists_consistent_complement_closed Γ_consis; - use ⟨Γ', ?_⟩; - assumption; - -noncomputable instance [DecidableEq F] [Entailment.Consistent 𝓢] : Inhabited (ConsistentComplementClosedFinset 𝓢 Φ) := ⟨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 ConsistentComplementClosedFinset - -end - -end CCCF - -end LO - - - - - +import Foundation.InterpretabilityLogic.Formula.Subformula +import Foundation.InterpretabilityLogic.Formula.Complement +import Foundation.Propositional.CMCF namespace LO.InterpretabilityLogic @@ -404,175 +11,8 @@ variable {𝓢 : S} open Modal (Kripke.Frame Kripke.Model) -namespace Formula - -variable {φ ψ χ : 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_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_neg (h : (∼ψ) ∈ φ.subformulas) : ψ ∈ φ.subformulas := (mem_imp h).1 -@[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 - -@[simp, grind] lemma eq_falsum : (falsum : Formula α) = ⊥ := rfl -@[simp, grind] lemma eq_or (φ ψ : Formula α) : or φ ψ = φ ⋎ ψ := rfl -@[simp, grind] lemma eq_and (φ ψ : Formula α) : and φ ψ = φ ⋏ ψ := rfl -@[simp, grind] lemma eq_imp (φ ψ : Formula α) : imp φ ψ = φ ➝ ψ := rfl -@[simp, grind] lemma eq_neg (φ : Formula α) : neg φ = ∼φ := rfl -@[simp, grind] lemma eq_box (φ : Formula α) : box φ = □φ := rfl -@[simp, grind] lemma eq_dia (φ : Formula α) : dia φ = ◇φ := rfl - -def complement : Formula α → Formula α - | ∼φ => φ - | φ => ∼φ -instance : Compl (Formula α) where - compl := complement - -namespace complement - -omit [DecidableEq α] -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 - - -@[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 ψ) - -end Formula - - namespace FormulaFinset -variable {Φ Φ₁ Φ₂ : FormulaFinset α} - -class SubformulaClosed (Φ : FormulaFinset α) where - subfml_closed : ∀ φ ∈ Φ, φ.subformulas ⊆ Φ - -namespace SubformulaClosed - -variable [Φ.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 SubformulaClosed - - class Adequate (Φ : FormulaFinset α) extends Φ.SubformulaClosed where compl_closed : ∀ φ ∈ Φ, -φ ∈ Φ mem_top_rhd_top : ⊤ ▷ ⊤ ∈ Φ @@ -587,7 +27,7 @@ attribute [simp] Adequate.mem_top_rhd_top namespace Adequate -variable [Φ.Adequate] +variable {Φ : FormulaFinset α} [Φ.Adequate] @[grind ⇒] lemma mem_imp (h : φ ➝ ψ ∈ Φ) : φ ∈ Φ ∧ ψ ∈ Φ := SubformulaClosed.mem_imp h @[grind ⇒] lemma mem_box (h : □φ ∈ Φ) : φ ∈ Φ := SubformulaClosed.mem_box h @@ -595,22 +35,9 @@ variable [Φ.Adequate] end Adequate -open LO.Entailment in -instance [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; - -def Consistent (𝓢 : S) (Φ : FormulaFinset α) : Prop := Φ *⊬[𝓢] ⊥ -def Inconsistent (𝓢 : S) (Φ : FormulaFinset α) : Prop := ¬Consistent 𝓢 Φ +end FormulaFinset -def Maximal (𝓢 : S) (Φ : FormulaFinset α) := ∀ Ψ, Φ ⊂ Ψ → Inconsistent 𝓢 Ψ -end FormulaFinset section @@ -627,18 +54,19 @@ variable {Φ : AdequateSet α} end AdequateSet -open LO.CCCF +open Finset.LO +open LO.ComplementMaximalConsistentFinset -- def MaximalConsistentSet (𝓢 : S) (Φ : AdequateSet α) := { Ψ : FormulaFinset α // Ψ ⊆ Φ.1 ∧ Ψ.Maximal 𝓢 ∧ Ψ.Consistent 𝓢 } -variable {Φ : AdequateSet α} {Γ Δ Θ : { Γ : ConsistentComplementClosedFinset 𝓢 Φ.1 // Γ.1 ⊆ Φ.1 }} +variable {Φ : AdequateSet α} {Γ Δ Θ : { Γ : ComplementMaximalConsistentFinset 𝓢 Φ.1 // Γ.1 ⊆ Φ.1 }} -structure ILSuccessor (Γ Δ : { Γ : ConsistentComplementClosedFinset 𝓢 Φ.1 // Γ.1 ⊆ Φ.1 }) : Prop where +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}) (Γ Δ : { Γ : ConsistentComplementClosedFinset 𝓢 Φ.1 // Γ.1 ⊆ Φ.1 }) extends Γ ≺ Δ where +structure ILCriticalSuccessor (χ : { χ : Formula α // χ ∈ Φ.1}) (Γ Δ : { Γ : ComplementMaximalConsistentFinset 𝓢 Φ.1 // Γ.1 ⊆ Φ.1 }) extends Γ ≺ Δ where prop3 : ∀ φ, φ ▷ χ.1 ∈ Γ.1 → -φ ∈ Δ.1 ∧ □-φ ∈ Δ.1 notation Γ:max " ≺[" χ "] " Δ:max => ILCriticalSuccessor χ Γ Δ @@ -686,9 +114,9 @@ lemma claim3 [Entailment.IL 𝓢] (h₁ : ∼(φ ▷ χ.1) ∈ Γ.1) : ∃ Δ, ( have : □-φ ∈ Φ.1 := Φ.2.mem_part₁ this |>.1; have : □-φ ∉ Γ.1 := by by_contra hC; - replace hC : Γ *⊢[𝓢] □-φ := ConsistentComplementClosedFinset.membership_iff (by simpa) |>.mp hC; - apply ConsistentComplementClosedFinset.iff_mem_compl (by simpa) |>.mpr $ Formula.complement.rhd_def ▸ h₁; - apply ConsistentComplementClosedFinset.membership_iff (by simpa) |>.mpr; + 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!; @@ -702,7 +130,7 @@ lemma claim3 [Entailment.IL 𝓢] (h₁ : ∼(φ ▷ χ.1) ∈ Γ.1) : ∃ Δ, ( let Δ₄ : FormulaFinset _ := Ξ₂.image (λ ξ => -ξ) let Δ₅ : FormulaFinset _ := Ξ₂.image (λ ξ => □(-ξ)) let Δ : FormulaFinset _ := Δ₁ ∪ Δ₂ ∪ Δ₃ ∪ Δ₄ ∪ Δ₅ - have Δ_consis : Δ.Consistent 𝓢 := by + have Δ_consis : Consistent 𝓢 Δ := by by_contra!; obtain ⟨Θ, hΘ₁, H⟩ := def_inconsistent.mp this; replace H : Δ *⊢[𝓢] ⊥ := Context.weakening! hΘ₁ H; @@ -727,7 +155,7 @@ lemma claim3 [Entailment.IL 𝓢] (h₁ : ∼(φ ▷ χ.1) ∈ Γ.1) : ∃ Δ, ( . sorry; . sorry; . sorry; - obtain ⟨Ω, hΩ⟩ : ∃ Ω : ConsistentComplementClosedFinset 𝓢 Φ.1, Δ ⊆ Ω.1 := ConsistentComplementClosedFinset.lindenbaum Δ_consis; + obtain ⟨Ω, hΩ⟩ : ∃ Ω : ComplementMaximalConsistentFinset 𝓢 Φ.1, Δ ⊆ Ω.1 := ComplementMaximalConsistentFinset.lindenbaum Δ_consis; sorry; /- use ⟨Δ, by sorry⟩; @@ -782,8 +210,8 @@ lemma claim4 (h₁ : (φ ▷ ψ) ∈ Γ.1) (h₂ : φ ∈ Δ.1) (h₃ : Γ ≺[ ((Γ.1.1.preimage (λ ξ => ξ ▷ χ) (by simp)) |>.image (λ ξ => -ξ)) ∪ ((Γ.1.1.preimage (λ ξ => ξ ▷ χ) (by simp)) |>.image (λ ξ => □-ξ)) - have Δ₀_consis : Δ₀.Consistent 𝓢 := by sorry; - obtain ⟨Δ, hΔ⟩ : ∃ Δ : ConsistentComplementClosedFinset 𝓢 Φ.1, Δ₀ ⊆ Δ.1 := by + have Δ₀_consis : Consistent 𝓢 Δ := by sorry; + obtain ⟨Δ, hΔ⟩ : ∃ Δ : ComplementMaximalConsistentFinset 𝓢 Φ.1, Δ₀ ⊆ Δ.1 := by sorry; use ⟨Δ, by sorry⟩; refine ⟨?_, ?_, ?_⟩; @@ -830,19 +258,17 @@ open Veltman namespace Veltman -open LO.CCCF - variable {α : Type*} [DecidableEq α] variable [Entailment S (Formula ℕ)] -variable {Φ : AdequateSet _} {𝓢 : S} {Γ : { Γ : ConsistentComplementClosedFinset 𝓢 Φ.1 // Γ.1 ⊆ Φ.1 }} +variable {Φ : AdequateSet _} {𝓢 : S} {Γ : { Γ : ComplementMaximalConsistentFinset 𝓢 Φ.1 // Γ.1 ⊆ Φ.1 }} -protected inductive ILMiniCanonicalModel.IsWorld (Γ : { Γ : ConsistentComplementClosedFinset 𝓢 Φ.1 // Γ.1 ⊆ Φ.1 }) - : { Γ : ConsistentComplementClosedFinset 𝓢 Φ.1 // Γ.1 ⊆ Φ.1 } × List { φ // φ ∈ Φ.1 } → Prop +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 (Γ : { Γ : ConsistentComplementClosedFinset 𝓢 Φ.1 // Γ.1 ⊆ Φ.1 }) : Veltman.Model where +def ILMiniCanonicalModel (Γ : { Γ : ComplementMaximalConsistentFinset 𝓢 Φ.1 // Γ.1 ⊆ Φ.1 }) : Veltman.Model where toKripkeFrame := { World := { P // ILMiniCanonicalModel.IsWorld Γ P } world_nonempty := ⟨⟨(Γ, []), ILMiniCanonicalModel.IsWorld.i₁⟩⟩ @@ -935,7 +361,6 @@ lemma ILMiniCanonicalModel.truthlemma [Entailment.IL 𝓢] {X : ILMiniCanonicalM end Veltman -open LO.CCCF open Formula.Veltman in instance IL.Veltman.finite_complete : Complete InterpretabilityLogic.IL Veltman.FrameClass.FiniteIL := by constructor; @@ -944,7 +369,7 @@ instance IL.Veltman.finite_complete : Complete InterpretabilityLogic.IL Veltman. intro hφ; apply not_validOnFrameClass_of_exists_model_world; let Φ : AdequateSet ℕ := ⟨{-φ}, by sorry⟩ - obtain ⟨Γ, hΓ⟩ : ∃ Γ : ConsistentComplementClosedFinset (InterpretabilityLogic.IL) Φ.1, {-φ} ⊆ Γ.1 := ConsistentComplementClosedFinset.lindenbaum (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; diff --git a/Foundation/Logic/CCCF.lean b/Foundation/Propositional/CMCF.lean similarity index 86% rename from Foundation/Logic/CCCF.lean rename to Foundation/Propositional/CMCF.lean index 50ffeaa88..3ea707042 100644 --- a/Foundation/Logic/CCCF.lean +++ b/Foundation/Propositional/CMCF.lean @@ -1,31 +1,35 @@ +/- + 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*) [Tilde F] where +class Compl (F : Type*) where compl : F → F prefix:120 "-" => Compl.compl - - namespace Entailment -class ComplEquiv [LogicalConnective F] [Compl F] [Entailment S F] (𝓢 : S) where +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 {F S : Type*} [LogicalConnective F] [Compl F] [Entailment S F] - {𝓢 : S} {φ : F} [ComplEquiv 𝓢] - -@[simp] lemma compl_equiv : 𝓢 ⊢ ∼φ ⭤ -φ := ⟨compl_equiv!⟩ - - -variable [Entailment.Minimal 𝓢] +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⟩ @@ -47,19 +51,26 @@ end end Entailment +end LO -namespace CCCF open LO.Entailment LO.Entailment.Context +namespace Finset.LO -variable {F} [LogicalConnective F] [DecidableEq F] - {S} [Entailment S F] -variable {𝓢 : S} {Γ Δ : Finset F} {φ ψ : F} +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Δ; @@ -72,23 +83,12 @@ lemma def_consistent [Entailment.Minimal 𝓢] : Consistent 𝓢 Γ ↔ ∀ Δ : push_neg; simpa using h; - -def Inconsistent (𝓢 : S) (Γ : Finset F) : Prop := ¬(Consistent 𝓢 Γ) - lemma def_inconsistent [Entailment.Minimal 𝓢] : Inconsistent 𝓢 Γ ↔ ∃ Δ : Finset F, (Δ ⊆ Γ) ∧ (Δ *⊢[𝓢] ⊥) := by rw [Inconsistent, def_consistent]; push_neg; simp; -def Maximal (𝓢 : S) (Γ : Finset F) : Prop := ∀ Δ, Γ ⊂ Δ → Inconsistent 𝓢 Δ - -def ComplementBounded [Compl F] (Γ Φ : Finset F) : Prop := Γ ⊆ (Φ ∪ Φ.image (-·)) - -/-- For every `φ` in `Δ`, `φ` or `-φ` is in `Γ` -/ -def ComplementClosed [Compl F] (Γ Φ : Finset F) : Prop := ∀ φ ∈ Φ, φ ∈ Γ ∨ -φ ∈ Γ - - section variable [Entailment.Cl 𝓢] @@ -162,12 +162,9 @@ lemma neg_provable_iff_insert_not_consistent : Inconsistent 𝓢 (insert φ Γ) . tauto; . apply N!_iff_CO!.mp h; -end - - section -variable [Compl F] [Entailment.Cl 𝓢] [ComplEquiv 𝓢] +variable [Compl F] [ComplEquiv 𝓢] @[grind] lemma not_mem_compl_of_mem (Γ_consis : Consistent 𝓢 Γ) (h : φ ∈ Γ) : (-φ) ∉ Γ := by @@ -191,6 +188,8 @@ lemma not_mem_of_mem_compl (Γ_consis : Consistent 𝓢 Γ) (h : -φ ∈ Γ) : end +end + namespace exists_consistent_complement_closed @@ -267,10 +266,9 @@ 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 𝓢 Γ') ∧ (ComplementClosed Γ' Φ) := by + : ∃ Γ', (Γ ⊆ Γ') ∧ (Consistent 𝓢 Γ') ∧ (ComplementMaximal Γ' Φ) := by use enum 𝓢 Γ Φ.toList; refine ⟨?_, ?_, ?_⟩; . simp; @@ -279,24 +277,30 @@ theorem exists_consistent_complement_closed [Compl F] [ComplEquiv 𝓢] [Entailm apply of_mem_seed; simpa; -section +end Finset.LO + + + + +namespace LO + +open Finset.LO -omit [DecidableEq F] variable [Compl F] {Φ : Finset F} -abbrev ConsistentComplementClosedFinset (𝓢 : S) (Φ : Finset F) := { Γ : Finset F // (Consistent 𝓢 Γ) ∧ (ComplementClosed Γ Φ) } +abbrev ComplementMaximalConsistentFinset (𝓢 : S) (Φ : Finset F) := { Γ : Finset F // (Consistent 𝓢 Γ) ∧ (ComplementMaximal Γ Φ) } -variable {Γ Γ₁ Γ₂ Δ : ConsistentComplementClosedFinset 𝓢 Φ} {φ ψ : F} +variable {Γ Γ₁ Γ₂ Δ : ComplementMaximalConsistentFinset 𝓢 Φ} {φ ψ : F} -namespace ConsistentComplementClosedFinset +namespace ComplementMaximalConsistentFinset -instance : Membership (F) (ConsistentComplementClosedFinset 𝓢 Φ) := ⟨λ X φ => φ ∈ X.1⟩ +instance : Membership (F) (ComplementMaximalConsistentFinset 𝓢 Φ) := ⟨λ X φ => φ ∈ X.1⟩ -@[simp] lemma consistent (Γ : ConsistentComplementClosedFinset 𝓢 Φ) : Consistent 𝓢 Γ := Γ.2.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 (Γ : ConsistentComplementClosedFinset 𝓢 Φ) : ComplementClosed Γ Φ := Γ.2.2 +@[simp] lemma maximal (Γ : ComplementMaximalConsistentFinset 𝓢 Φ) : ComplementMaximal Γ Φ := Γ.2.2 @[grind] lemma mem_compl_of_not_mem (hs : ψ ∈ Φ) : ψ ∉ Γ → -ψ ∈ Γ := by @@ -317,12 +321,12 @@ lemma equality_def : Γ₁ = Γ₂ ↔ Γ₁.1 = Γ₂.1 := by variable [Entailment.ComplEquiv 𝓢] [Entailment.Cl 𝓢] theorem lindenbaum [DecidableEq F] {Γ : Finset F} (Γ_consis : Consistent 𝓢 Γ) - : ∃ Γ' : ConsistentComplementClosedFinset 𝓢 Φ, Γ ⊆ Γ'.1 := by + : ∃ Γ' : ComplementMaximalConsistentFinset 𝓢 Φ, Γ ⊆ Γ'.1 := by obtain ⟨Γ', ⟨_, _⟩⟩ := exists_consistent_complement_closed Γ_consis; use ⟨Γ', ?_⟩; assumption; -noncomputable instance [DecidableEq F] [Entailment.Consistent 𝓢] : Inhabited (ConsistentComplementClosedFinset 𝓢 Φ) := ⟨lindenbaum (Γ := ∅) (by simp) |>.choose⟩ +noncomputable instance [DecidableEq F] [Entailment.Consistent 𝓢] : Inhabited (ComplementMaximalConsistentFinset 𝓢 Φ) := ⟨lindenbaum (Γ := ∅) (by simp) |>.choose⟩ variable [DecidableEq F] @@ -379,10 +383,8 @@ lemma iff_mem_imp (hφψΦ : (φ ➝ ψ) ∈ Φ) (hφΦ : φ ∈ Φ) (hψΦ : ψ apply membership_iff hψΦ |>.mp; assumption; -end ConsistentComplementClosedFinset - -end - -end CCCF +end ComplementMaximalConsistentFinset end LO + +end