From 26d5362c2639dbcc59cf3fc2522909aeb6d6840e Mon Sep 17 00:00:00 2001 From: twwar Date: Wed, 13 May 2026 21:22:02 +0200 Subject: [PATCH 1/2] models and connectives --- Cslib/Foundations/Logic/Connectives.lean | 49 ++++++++++++ Cslib/Foundations/Logic/Model.lean | 98 ++++++++++++++++++++++++ 2 files changed, 147 insertions(+) create mode 100644 Cslib/Foundations/Logic/Connectives.lean create mode 100644 Cslib/Foundations/Logic/Model.lean diff --git a/Cslib/Foundations/Logic/Connectives.lean b/Cslib/Foundations/Logic/Connectives.lean new file mode 100644 index 000000000..b645ae772 --- /dev/null +++ b/Cslib/Foundations/Logic/Connectives.lean @@ -0,0 +1,49 @@ +/- +Copyright (c) 2025 Thomas Waring. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Thomas Waring +-/ + +module + +public import Cslib.Init +public import Mathlib.Order.Notation + +@[expose] public section + +namespace Cslib.Logic + +/-- Class for implication. -/ +class HasImpl (α : Type*) where + /-- Implication. -/ + impl : α → α → α + +@[inherit_doc] scoped infixr:25 " → " => HasImpl.impl + +/-- Class for conjunction. -/ +class HasAnd (α : Type*) where + /-- Conjunction. -/ + and : α → α → α + +@[inherit_doc] scoped infixr:35 " ∧ " => HasAnd.and + +/-- Class for disjunction. -/ +class HasOr (α : Type*) where + /-- Disjunction. -/ + or : α → α → α + +@[inherit_doc] scoped infixr:30 " ∨ " => HasOr.or + +/-- Class for negation. -/ +class HasNot (α : Type*) where + /-- Negation. -/ + not : α → α + +@[inherit_doc] scoped notation:max "¬" a:40 => HasNot.not a + +/-- Instantiate negation for types with implication and a bottom element. NB: this has a lower + instance priority to account for proposition types with inbuilt negation. -/ +instance (priority := 900) instNotImplBot (α : Type*) [HasImpl α] [Bot α] : HasNot α where + not a := a → ⊥ + +end Cslib.Logic diff --git a/Cslib/Foundations/Logic/Model.lean b/Cslib/Foundations/Logic/Model.lean new file mode 100644 index 000000000..a34b24f9e --- /dev/null +++ b/Cslib/Foundations/Logic/Model.lean @@ -0,0 +1,98 @@ +/- +Copyright (c) 2025 Thomas Waring. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Thomas Waring +-/ + +module + +public import Cslib.Foundations.Logic.Connectives +public import Cslib.Foundations.Logic.InferenceSystem +public import Cslib.Logics.Modal.Basic + +public section + +namespace Cslib.Logic + +/-- Objects of type `β` carry a forcing relation with the proposition type `α`. -/ +class ModelClass (α : outParam (Type*)) (β : Type*) where + /-- `Forces b a` has the intended semantics "`a` is valid in the model `b`". -/ + Forces : β → α → Prop + +scoped notation "⊨[" b "] " a => ModelClass.Forces b a + +/-- Objects of type `β` carry a forcing relation worlds of type `γ` and the proposition type `α`. -/ +class ParamModelClass (α : outParam (Type*)) (β : Type*) where + Param : β → Type* + /-- Forcing relation associated to each parameter. -/ + ForcesAt (b : β) : (Param b) → α → Prop + +scoped notation w " ⊨[" b "] " a => ParamModelClass.ForcesAt b w a + +instance ParamModelClass.toModelClass {α β : Type*} [ParamModelClass α β] : ModelClass α β where + Forces M A := ∀ w : ParamModelClass.Param M, w ⊨[M] A + +/-- Bundled interpretation function. -/ +structure Interp (α β : Type*) where + /-- Interpret a proposition in a model. -/ + interp : α → β + +/-- An `InterpModel` consists of an interpretation function, and a set specifying which + interpretations are considered valid. -/ +structure InterpModel (α β : Type*) extends Interp α β where + /-- The set of valid interpretations. -/ + filter : Set β + +instance {α β : Type*} : ModelClass α (InterpModel α β) where + Forces M a := M.interp a ∈ M.filter + +namespace Interp + +class AlgebraicAnd {α β : Type*} [HasAnd α] [Min β] (M : Interp α β) where + interp_and_eq (x y : α) : M.interp (x ∧ y) = M.interp x ⊓ M.interp y + +class AlgebraicOr {α β : Type*} [HasOr α] [Max β] (M : Interp α β) where + interp_or_eq (x y : α) : M.interp (x ∨ y) = M.interp x ⊔ M.interp y + +class AlgebraicImpl {α β : Type*} [HasImpl α] [HImp β] (M : Interp α β) where + interp_impl_eq (x y : α) : M.interp (x → y) = M.interp x ⇨ M.interp y + +class AlgebraicNot {α β : Type*} [HasNot α] [Compl β] (M : Interp α β) where + interp_not_eq (x : α) : M.interp (¬ x) = (M.interp x)ᶜ + +end Interp + +open ModelClass ParamModelClass InferenceSystem + +def Sound {α β S : Type*} [ModelClass α β] [InferenceSystem S α] : Prop := + ∀ (A : α) (b : β) , DerivableIn S A → ⊨[b] A + +def Complete {α β S : Type*} [ModelClass α β] [InferenceSystem S α] : Prop := + ∀ A : α, (∀ b : β, ⊨[b] A) → DerivableIn S A + +def ParamModelClass.theory {α β : Type*} [ParamModelClass α β] {M : β} (w : Param M) : Set α := + {A : α | w ⊨[M] A} + +def ModelClass.logic {α β : Type*} [ModelClass α β] (S : Set β) : Set α := {A | ∀ b ∈ S, ⊨[b] A} + +namespace Modal + +structure BundledModel (Atom : Type*) where + World : Type* + model : Model World Atom + +def Model.toBundledModel {World Atom : Type*} (M : Model World Atom) : BundledModel Atom := + {World := World, model := M} + +instance {Atom : Type*} : ParamModelClass (Proposition Atom) (BundledModel Atom) where + Param M := M.World + ForcesAt M w A := Satisfies M.model w A + +example {World Atom : Type*} (S : Set (Model World Atom)) : + logic S = ModelClass.logic (Model.toBundledModel '' S) := by + simp [ModelClass.logic] + rfl + +end Modal + +end Cslib.Logic From 0d30187b366989d61f37b5669c21d60fc9acc826 Mon Sep 17 00:00:00 2001 From: twwar Date: Wed, 20 May 2026 19:54:59 +0200 Subject: [PATCH 2/2] docs --- Cslib/Foundations/Logic/Connectives.lean | 5 +- Cslib/Foundations/Logic/Model.lean | 116 ++++++++++++++++++----- 2 files changed, 98 insertions(+), 23 deletions(-) diff --git a/Cslib/Foundations/Logic/Connectives.lean b/Cslib/Foundations/Logic/Connectives.lean index b645ae772..e028e53f9 100644 --- a/Cslib/Foundations/Logic/Connectives.lean +++ b/Cslib/Foundations/Logic/Connectives.lean @@ -9,6 +9,8 @@ module public import Cslib.Init public import Mathlib.Order.Notation +/-! # Notation classes for logical connectives -/ + @[expose] public section namespace Cslib.Logic @@ -42,7 +44,8 @@ class HasNot (α : Type*) where @[inherit_doc] scoped notation:max "¬" a:40 => HasNot.not a /-- Instantiate negation for types with implication and a bottom element. NB: this has a lower - instance priority to account for proposition types with inbuilt negation. -/ + instance priority to account for proposition types with inbuilt negation. Possibly it should be + a `def` instead? -/ instance (priority := 900) instNotImplBot (α : Type*) [HasImpl α] [Bot α] : HasNot α where not a := a → ⊥ diff --git a/Cslib/Foundations/Logic/Model.lean b/Cslib/Foundations/Logic/Model.lean index a34b24f9e..49c9a091d 100644 --- a/Cslib/Foundations/Logic/Model.lean +++ b/Cslib/Foundations/Logic/Model.lean @@ -9,20 +9,23 @@ module public import Cslib.Foundations.Logic.Connectives public import Cslib.Foundations.Logic.InferenceSystem public import Cslib.Logics.Modal.Basic +public import Cslib.Logics.Propositional.NaturalDeduction.Basic + +/-! # Semantics for logical systems -/ public section namespace Cslib.Logic /-- Objects of type `β` carry a forcing relation with the proposition type `α`. -/ -class ModelClass (α : outParam (Type*)) (β : Type*) where +class ModelClass (α : outParam Type*) (β : Type*) where /-- `Forces b a` has the intended semantics "`a` is valid in the model `b`". -/ Forces : β → α → Prop scoped notation "⊨[" b "] " a => ModelClass.Forces b a /-- Objects of type `β` carry a forcing relation worlds of type `γ` and the proposition type `α`. -/ -class ParamModelClass (α : outParam (Type*)) (β : Type*) where +class ParamModelClass (α : outParam Type*) (β : Type*) where Param : β → Type* /-- Forcing relation associated to each parameter. -/ ForcesAt (b : β) : (Param b) → α → Prop @@ -33,42 +36,55 @@ instance ParamModelClass.toModelClass {α β : Type*} [ParamModelClass α β] : Forces M A := ∀ w : ParamModelClass.Param M, w ⊨[M] A /-- Bundled interpretation function. -/ -structure Interp (α β : Type*) where +class HasInterp (α : outParam Type*) (β : Type*) where + /-- Type carrying interpretation. -/ + Ground : β → Type* /-- Interpret a proposition in a model. -/ - interp : α → β + interp : (b : β) → α → Ground b /-- An `InterpModel` consists of an interpretation function, and a set specifying which interpretations are considered valid. -/ -structure InterpModel (α β : Type*) extends Interp α β where +class InterpModelClass (α : outParam (Type*)) (β : Type*) extends HasInterp α β where /-- The set of valid interpretations. -/ - filter : Set β + filter (b : β) : Set (Ground b) -instance {α β : Type*} : ModelClass α (InterpModel α β) where - Forces M a := M.interp a ∈ M.filter +instance InterpModelClass.instModelClass {α β : Type*} [InterpModelClass α β] : ModelClass α β where + Forces b a := HasInterp.interp b a ∈ filter b -namespace Interp +namespace HasInterp -class AlgebraicAnd {α β : Type*} [HasAnd α] [Min β] (M : Interp α β) where - interp_and_eq (x y : α) : M.interp (x ∧ y) = M.interp x ⊓ M.interp y +class AlgebraicAnd (α β : Type*) [HasInterp α β] [HasAnd α] [∀ b : β, Min (Ground b)] where + interp_and_eq (M : β) (x y : α) : interp M (x ∧ y) = interp M x ⊓ interp M y -class AlgebraicOr {α β : Type*} [HasOr α] [Max β] (M : Interp α β) where - interp_or_eq (x y : α) : M.interp (x ∨ y) = M.interp x ⊔ M.interp y +class AlgebraicOr (α β : Type*) [HasInterp α β] [HasOr α] [∀ b : β, Max (Ground b)] where + interp_or_eq (M : β) (x y : α) : interp M (x ∨ y) = interp M x ⊔ interp M y -class AlgebraicImpl {α β : Type*} [HasImpl α] [HImp β] (M : Interp α β) where - interp_impl_eq (x y : α) : M.interp (x → y) = M.interp x ⇨ M.interp y +class AlgebraicImpl (α β : Type*) [HasInterp α β] [HasImpl α] [∀ b : β, HImp (Ground b)] where + interp_impl_eq (M : β) (x y : α) : interp M (x → y) = interp M x ⇨ interp M y -class AlgebraicNot {α β : Type*} [HasNot α] [Compl β] (M : Interp α β) where - interp_not_eq (x : α) : M.interp (¬ x) = (M.interp x)ᶜ +class AlgebraicNot (α β : Type*) [HasInterp α β] [HasNot α] [∀ b : β, Compl (Ground b)] where + interp_not_eq (M : β) (x y : α) : interp M (¬ x) = (interp M x)ᶜ -end Interp +end HasInterp open ModelClass ParamModelClass InferenceSystem -def Sound {α β S : Type*} [ModelClass α β] [InferenceSystem S α] : Prop := - ∀ (A : α) (b : β) , DerivableIn S A → ⊨[b] A +variable {α β T} [ModelClass α β] [InferenceSystem T α] + +def SoundFor (α β T) [ModelClass α β] [InferenceSystem T α] (S : Set β) : Prop := + ∀ (A : α), DerivableIn T A → ∀ M ∈ S, ⊨[M] A + +lemma SoundFor.subset {S S' : Set β} (hS : S ⊆ S') : SoundFor α β T S' → SoundFor α β T S := + fun h A hA M hM => h A hA M (hS hM) -def Complete {α β S : Type*} [ModelClass α β] [InferenceSystem S α] : Prop := - ∀ A : α, (∀ b : β, ⊨[b] A) → DerivableIn S A +def CompleteFor (α β T : Type*) [ModelClass α β] [InferenceSystem T α] (S : Set β) : Prop := + ∀ A : α, (∀ M ∈ S, ⊨[M] A) → DerivableIn T A + +lemma CompleteFor.supset {S S' : Set β} (hS : S ⊆ S') : + CompleteFor α β T S → CompleteFor α β T S' := fun h A hA => h A (fun M hM => hA M (hS hM)) + +def IsCompleteModel (α β T) [ModelClass α β] [InferenceSystem T α] (M : β) : Prop := + ∀ (A : α), (⊨[M] A) → DerivableIn T A def ParamModelClass.theory {α β : Type*} [ParamModelClass α β] {M : β} (w : Param M) : Set α := {A : α | w ⊨[M] A} @@ -93,6 +109,62 @@ example {World Atom : Type*} (S : Set (Model World Atom)) : simp [ModelClass.logic] rfl +example {World Atom : Type*} (m : Model World Atom) (w : World) : + theory m w = ParamModelClass.theory (M := m.toBundledModel) w := by + simp [theory, ParamModelClass.theory] + rfl + end Modal +namespace PL + +variable {Atom : Type*} + +instance : HasAnd (Proposition Atom) := ⟨Proposition.and⟩ +instance : HasOr (Proposition Atom) := ⟨Proposition.or⟩ +instance : HasImpl (Proposition Atom) := ⟨Proposition.impl⟩ +instance [Bot Atom] : HasNot (Proposition Atom) := ⟨Proposition.neg⟩ + +structure HeytingModel (Atom : Type*) where + H : Type* + [inst : GeneralizedHeytingAlgebra H] + v : Atom → H + +instance (M : HeytingModel Atom) : GeneralizedHeytingAlgebra M.H := M.inst + +def HeytingModel.interp (M : HeytingModel Atom) : Proposition Atom → M.H + | Proposition.atom x => M.v x + | Proposition.and A B => M.interp A ⊓ M.interp B + | Proposition.or A B => M.interp A ⊔ M.interp B + | Proposition.impl A B => M.interp A ⇨ M.interp B + +instance : InterpModelClass (Proposition Atom) (HeytingModel Atom) where + Ground M := M.H + interp := HeytingModel.interp + filter _ := {⊤} + +instance (M : HeytingModel Atom) : GeneralizedHeytingAlgebra (HasInterp.Ground M) := M.inst + +instance : HasInterp.AlgebraicAnd (Proposition Atom) (HeytingModel Atom) where + interp_and_eq _ _ _ := rfl + +instance : HasInterp.AlgebraicOr (Proposition Atom) (HeytingModel Atom) where + interp_or_eq _ _ _ := rfl + +instance : HasInterp.AlgebraicImpl (Proposition Atom) (HeytingModel Atom) where + interp_impl_eq _ _ _ := rfl + +theorem HeytingModel.sound [DecidableEq Atom] {T : Theory Atom} : + SoundFor (Proposition Atom) (HeytingModel Atom) T {M | ∀ A ∈ T, interp M A = ⊤} := + sorry -- i have this in a branch + +def Theory.lindenbaum [DecidableEq Atom] (T : Theory Atom) : HeytingModel Atom := + sorry -- usual Heyting-algebra of propositions modulo equivalence + +theorem Theory.lindenbaum_complete [DecidableEq Atom] {T : Theory Atom} : + IsCompleteModel (Proposition Atom) (HeytingModel Atom) T T.lindenbaum := + sorry -- also in a branch + +end PL + end Cslib.Logic