From 26d5362c2639dbcc59cf3fc2522909aeb6d6840e Mon Sep 17 00:00:00 2001
From: twwar <tom.waring@unimelb.edu.au>
Date: Wed, 13 May 2026 21:22:02 +0200
Subject: [PATCH 1/4] 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 <tom.waring@unimelb.edu.au>
Date: Wed, 20 May 2026 19:54:59 +0200
Subject: [PATCH 2/4] 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

From c2f4157933d257c4b8e12c99fa313d58e634cc7d Mon Sep 17 00:00:00 2001
From: twwar <tom.waring@unimelb.edu.au>
Date: Thu, 21 May 2026 11:04:59 +0200
Subject: [PATCH 3/4] naming

---
 Cslib/Foundations/Logic/Model.lean | 52 +++++++++++++++---------------
 1 file changed, 26 insertions(+), 26 deletions(-)

diff --git a/Cslib/Foundations/Logic/Model.lean b/Cslib/Foundations/Logic/Model.lean
index 49c9a091d..104720613 100644
--- a/Cslib/Foundations/Logic/Model.lean
+++ b/Cslib/Foundations/Logic/Model.lean
@@ -18,22 +18,22 @@ 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
+class Models (α : outParam Type*) (β : Type*) where
+  /-- `Satisfies b a` has the intended semantics "`a` is valid in the model `b`". -/
+  Satisfies : β → α → Prop
 
-scoped notation "⊨[" b "] " a => ModelClass.Forces b a
+scoped notation "⊨[" b "] " a => Models.Satisfies b a
 
 /-- Objects of type `β` carry a forcing relation worlds of type `γ` and the proposition type `α`. -/
-class ParamModelClass (α : outParam Type*) (β : Type*) where
+class ParamModels (α : outParam Type*) (β : Type*) where
   Param : β → Type*
   /-- Forcing relation associated to each parameter. -/
-  ForcesAt (b : β) : (Param b) → α → Prop
+  SatisfiesAt (b : β) : (Param b) → α → Prop
 
-scoped notation w " ⊨[" b "] " a => ParamModelClass.ForcesAt b w a
+scoped notation w " ⊨[" b "] " a => ParamModels.SatisfiesAt b w a
 
-instance ParamModelClass.toModelClass {α β : Type*} [ParamModelClass α β] : ModelClass α β where
-  Forces M A := ∀ w : ParamModelClass.Param M, w ⊨[M] A
+instance ParamModels.toModels {α β : Type*} [ParamModels α β] : Models α β where
+  Satisfies M A := ∀ w : ParamModels.Param M, w ⊨[M] A
 
 /-- Bundled interpretation function. -/
 class HasInterp (α : outParam Type*) (β : Type*) where
@@ -44,12 +44,12 @@ class HasInterp (α : outParam Type*) (β : Type*) where
 
 /-- An `InterpModel` consists of an interpretation function, and a set specifying which
   interpretations are considered valid. -/
-class InterpModelClass (α : outParam (Type*)) (β : Type*) extends HasInterp α β where
+class InterpModels (α : outParam (Type*)) (β : Type*) extends HasInterp α β where
   /-- The set of valid interpretations. -/
   filter (b : β) : Set (Ground b)
 
-instance InterpModelClass.instModelClass {α β : Type*} [InterpModelClass α β] : ModelClass α β where
-  Forces b a := HasInterp.interp b a ∈ filter b
+instance InterpModels.instModels {α β : Type*} [InterpModels α β] : Models α β where
+  Satisfies b a := HasInterp.interp b a ∈ filter b
 
 namespace HasInterp
 
@@ -67,29 +67,29 @@ class AlgebraicNot (α β : Type*) [HasInterp α β] [HasNot α] [∀ b : β, Co
 
 end HasInterp
 
-open ModelClass ParamModelClass InferenceSystem
+open Models ParamModels InferenceSystem
 
-variable {α β T} [ModelClass α β] [InferenceSystem T α]
+variable {α β T} [Models α β] [InferenceSystem T α]
 
-def SoundFor (α β T) [ModelClass α β] [InferenceSystem T α] (S : Set β) : Prop :=
+def SoundFor (α β T) [Models α β] [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 CompleteFor (α β T : Type*) [ModelClass α β] [InferenceSystem T α] (S : Set β) : Prop :=
+def CompleteFor (α β T : Type*) [Models α β] [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 :=
+def IsCompleteModel (α β T) [Models α β] [InferenceSystem T α] (M : β) : Prop :=
   ∀ (A : α), (⊨[M] A) → DerivableIn T A
 
-def ParamModelClass.theory {α β : Type*} [ParamModelClass α β] {M : β} (w : Param M) : Set α :=
+def ParamModels.theory {α β : Type*} [ParamModels α β] {M : β} (w : Param M) : Set α :=
   {A : α | w ⊨[M] A}
 
-def ModelClass.logic {α β : Type*} [ModelClass α β] (S : Set β) : Set α := {A | ∀ b ∈ S, ⊨[b] A}
+def Models.logic {α β : Type*} [Models α β] (S : Set β) : Set α := {A | ∀ b ∈ S, ⊨[b] A}
 
 namespace Modal
 
@@ -100,18 +100,18 @@ structure BundledModel (Atom : Type*) where
 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
+instance {Atom : Type*} : ParamModels (Proposition Atom) (BundledModel Atom) where
   Param M := M.World
-  ForcesAt M w A := Satisfies M.model w A
+  SatisfiesAt 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]
+    logic S = Models.logic (Model.toBundledModel '' S) := by
+  simp [Models.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]
+    theory m w = ParamModels.theory (M := m.toBundledModel) w := by
+  simp [theory, ParamModels.theory]
   rfl
 
 end Modal
@@ -138,7 +138,7 @@ def HeytingModel.interp (M : HeytingModel Atom) : Proposition Atom → M.H
   | 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
+instance : InterpModels (Proposition Atom) (HeytingModel Atom) where
   Ground M := M.H
   interp := HeytingModel.interp
   filter _ := {⊤}

From b1261b7a0bf35c369441af9fe1aeb6207bbf677e Mon Sep 17 00:00:00 2001
From: twwar <tom.waring@unimelb.edu.au>
Date: Fri, 22 May 2026 08:58:33 +0200
Subject: [PATCH 4/4] classical example

---
 Cslib/Foundations/Logic/Model.lean | 13 +++++++++++++
 1 file changed, 13 insertions(+)

diff --git a/Cslib/Foundations/Logic/Model.lean b/Cslib/Foundations/Logic/Model.lean
index 104720613..eaf31c45f 100644
--- a/Cslib/Foundations/Logic/Model.lean
+++ b/Cslib/Foundations/Logic/Model.lean
@@ -165,6 +165,19 @@ theorem Theory.lindenbaum_complete [DecidableEq Atom] {T : Theory Atom} :
     IsCompleteModel (Proposition Atom) (HeytingModel Atom) T T.lindenbaum :=
   sorry -- also in a branch
 
+abbrev Valuation (Atom : Type*) := Atom → Prop
+
+def Valuation.interp (v : Valuation Atom) : Proposition Atom → Prop
+  | .atom x => v x
+  | .and A B => v.interp A ∧ v.interp B
+  | .or A B => v.interp A ∨ v.interp B
+  | .impl A B => v.interp A → v.interp B
+
+instance : InterpModels (Proposition Atom) (Valuation Atom) where
+  Ground _ := Prop
+  interp v A := v.interp A
+  filter _ := {True}
+
 end PL
 
 end Cslib.Logic