diff --git a/Cslib.lean b/Cslib.lean
index 1c70985ff2..a12616955f 100644
--- a/Cslib.lean
+++ b/Cslib.lean
@@ -154,6 +154,7 @@ public import Cslib.Foundations.Data.Polynomial.Monotone
 public import Cslib.Foundations.Data.Set.Saturation
 public import Cslib.Foundations.Data.StackTape
 public import Cslib.Foundations.Lint.Basic
+public import Cslib.Foundations.Logic.Consequence
 public import Cslib.Foundations.Logic.InferenceSystem
 public import Cslib.Foundations.Logic.LogicalEquivalence
 public import Cslib.Foundations.Logic.Operators
@@ -249,6 +250,8 @@ public import Cslib.Languages.Mech.LocalComputation
 public import Cslib.Languages.StatefulProcesses.Basic
 public import Cslib.Languages.StatefulProcesses.Network
 public import Cslib.Logics.HML.Basic
+public import Cslib.Logics.Kleene.Basic
+public import Cslib.Logics.Kleene.Semantics
 public import Cslib.Logics.LinearLogic.CLL.Basic
 public import Cslib.Logics.LinearLogic.CLL.CutElimination
 public import Cslib.Logics.LinearLogic.CLL.EtaExpansion
diff --git a/Cslib/Foundations/Logic/Consequence.lean b/Cslib/Foundations/Logic/Consequence.lean
new file mode 100644
index 0000000000..c918c720c3
--- /dev/null
+++ b/Cslib/Foundations/Logic/Consequence.lean
@@ -0,0 +1,101 @@
+/-
+Copyright (c) 2026 Jesse Alama. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Jesse Alama
+-/
+
+module
+
+public import Cslib.Foundations.Syntax.Context
+public import Cslib.Foundations.Logic.InferenceSystem
+
+/-! # Semantic consequence
+
+Semantic consequence and validity for inference systems whose judgements pair a model with a
+proposition. The model is captured as a judgemental context (`HasHContext Judgement α`): a
+judgement with the proposition missing. A proposition is a consequence of a set of premises when
+every context deriving all the premises derives it, and it is valid when every context derives it.
+Both notions can be restricted to a class of contexts, which is how consequence over the two-valued
+valuations of a many-valued logic, or over a frame class in modal logic, arises.
+
+Derivations are required to be propositions (`InferenceSystem.{_, _, 0}`), as they are for
+satisfaction judgements. Proof systems whose derivations are data are not covered.
+
+## Main definitions
+
+- `Cslib.Logic.EntailsWithin`: consequence over a class of judgemental contexts.
+- `Cslib.Logic.Entails`: consequence over all judgemental contexts.
+- `Cslib.Logic.ValidWithin`: validity over a class of judgemental contexts.
+- `Cslib.Logic.Valid`: validity, that is, derivability in every judgemental context.
+
+## Main results
+
+- `Cslib.Logic.validWithin_iff_entailsWithin_empty`: validity is consequence from no premises.
+- `Cslib.Logic.EntailsWithin.mono` and `Cslib.Logic.EntailsWithin.trans`: weakening and cut.
+- `Cslib.Logic.EntailsWithin.anti`: consequence over a class of contexts is consequence over any
+  subclass.
+- `Cslib.Logic.entailsWithin_of_incompatible`: incompatible premises entail everything.
+-/
+
+@[expose] public section
+
+namespace Cslib.Logic
+
+open scoped InferenceSystem
+
+variable (J : Type*) {α : Type*} (S : Type*) [HasHContext J α] [InferenceSystem.{_, _, 0} S J]
+
+/-- Consequence over a class `C` of judgemental contexts: every context in `C` deriving all the
+premises in `Γ` derives `φ`. -/
+def EntailsWithin (C : Set (HasHContext.Context J α)) (Γ : Set α) (φ : α) : Prop :=
+  ∀ c ∈ C, (∀ ψ ∈ Γ, S⇓(c<[ψ])) → S⇓(c<[φ])
+
+/-- Consequence over all judgemental contexts. -/
+abbrev Entails (Γ : Set α) (φ : α) : Prop := EntailsWithin J S Set.univ Γ φ
+
+/-- Validity over a class `C` of judgemental contexts: every context in `C` derives `φ`. -/
+def ValidWithin (C : Set (HasHContext.Context J α)) (φ : α) : Prop := ∀ c ∈ C, S⇓(c<[φ])
+
+/-- Validity: derivable in every judgemental context. -/
+abbrev Valid (φ : α) : Prop := ValidWithin J S Set.univ φ
+
+variable {J S}
+
+/-- Validity over a class of contexts is consequence from no premises over that class. -/
+theorem validWithin_iff_entailsWithin_empty {C : Set (HasHContext.Context J α)} {φ : α} :
+    ValidWithin J S C φ ↔ EntailsWithin J S C ∅ φ :=
+  ⟨fun h c hc _ => h c hc, fun h c hc => h c hc fun _ h => h.elim⟩
+
+/-- Validity is consequence from no premises. -/
+theorem valid_iff_entails_empty {φ : α} : Valid J S φ ↔ Entails J S ∅ φ :=
+  validWithin_iff_entailsWithin_empty
+
+/-- Every premise is a consequence. -/
+theorem entailsWithin_of_mem {C : Set (HasHContext.Context J α)} {Γ : Set α} {φ : α}
+    (h : φ ∈ Γ) : EntailsWithin J S C Γ φ :=
+  fun _ _ hΓ => hΓ _ h
+
+/-- Weakening: consequence is preserved by adding premises. -/
+theorem EntailsWithin.mono {C : Set (HasHContext.Context J α)} {Γ Δ : Set α} {φ : α}
+    (hΓ : EntailsWithin J S C Γ φ) (h : Γ ⊆ Δ) : EntailsWithin J S C Δ φ :=
+  fun c hc hv => hΓ c hc fun ψ hψ => hv ψ (h hψ)
+
+/-- Cut: if every premise in `Δ` is a consequence of `Γ`, so is every consequence of `Δ`. -/
+theorem EntailsWithin.trans {C : Set (HasHContext.Context J α)} {Γ Δ : Set α} {φ : α}
+    (h₁ : ∀ ψ ∈ Δ, EntailsWithin J S C Γ ψ) (h₂ : EntailsWithin J S C Δ φ) :
+    EntailsWithin J S C Γ φ :=
+  fun c hc hv => h₂ c hc fun ψ hψ => h₁ ψ hψ c hc hv
+
+/-- Consequence over a class of contexts is consequence over any subclass. -/
+theorem EntailsWithin.anti {C D : Set (HasHContext.Context J α)} {Γ : Set α} {φ : α}
+    (h : EntailsWithin J S D Γ φ) (hCD : C ⊆ D) : EntailsWithin J S C Γ φ :=
+  fun c hc => h c (hCD hc)
+
+/-- Incompatible premises entail everything: if `φ` and `ψ` are premises and no context in `C`
+derives both, then every proposition is a consequence over `C`. -/
+theorem entailsWithin_of_incompatible {C : Set (HasHContext.Context J α)} {Γ : Set α} {φ ψ : α}
+    (h₁ : φ ∈ Γ) (h₂ : ψ ∈ Γ) (h : ∀ c ∈ C, S⇓(c<[φ]) → ¬S⇓(c<[ψ])) (χ : α) :
+    EntailsWithin J S C Γ χ :=
+  fun _ hc hΓ => absurd (hΓ _ h₂) (h _ hc (hΓ _ h₁))
+
+end Cslib.Logic
diff --git a/Cslib/Logics/Kleene/Basic.lean b/Cslib/Logics/Kleene/Basic.lean
new file mode 100644
index 0000000000..5b9b5eebbf
--- /dev/null
+++ b/Cslib/Logics/Kleene/Basic.lean
@@ -0,0 +1,388 @@
+/-
+Copyright (c) 2026 Jesse Alama. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Jesse Alama
+-/
+
+module
+
+public import Cslib.Init
+public import Cslib.Foundations.Logic.Operators
+public import Mathlib.Tactic.DeriveFintype
+
+/-! # Truth values of Kleene's strong three-valued logic
+
+The truth values and connectives of Kleene's strong three-valued logic (K3) [Kleene1952], with the
+truth order `false < unknown < true` and the information order `unknown ⊑ true`,
+`unknown ⊑ false`. These are the semantic domain for the propositions in
+`Cslib.Logics.Kleene.Semantics`.
+
+The truth order is the `LE` instance: `∧` and `∨` are its meet and join, and negation reverses
+it. In the information order `⊑`, `unknown` lies below both definite values; every connective
+is monotone in it, and `∧`, `∨` and `¬` are the greatest monotone extensions of `&&`, `||`
+and `!`.
+
+## Main definitions
+
+- `Kleene.Value`: the three truth values.
+- `Kleene.Value.not`, `Kleene.Value.and`, `Kleene.Value.or`, `Kleene.Value.imp`,
+  `Kleene.Value.iff`: the connectives.
+- `Kleene.Value.ofBool`: the embedding of `Bool`.
+- `Kleene.Value.InfoLE`, written `⊑`: the information order.
+- `Kleene.Value.equivOptionBool`: the equivalence with `Option Bool`, `unknown` as `none`.
+
+## Main results
+
+- `LinearOrder Kleene.Value`, `BoundedOrder Kleene.Value`: the truth order, with `∧` as meet and
+  `∨` as join.
+- `Kleene.Value.ofBool_and` and friends: `ofBool` commutes with the connectives.
+- `IsPartialOrder Kleene.Value Kleene.Value.InfoLE`, `Kleene.Value.InfoLE.and` and friends: the
+  information order is a partial order in which every connective is monotone.
+- `Kleene.Value.infoLE_and_of_extends` and friends: `∧`, `∨` and `¬` are the greatest monotone
+  extensions of `&&`, `||` and `!`.
+- `Kleene.Value.eq_not_of_extends`: `¬` is the only monotone extension of `!`.
+
+## References
+
+- [Kleene1952] S. C. Kleene, *Introduction to Metamathematics*, §64.
+-/
+
+@[expose] public section
+
+namespace Cslib.Logic.Kleene
+
+-- Needed by the `Fintype` derive handler, as for Mathlib's `SignType`.
+set_option backward.isDefEq.respectTransparency false in
+/-- A truth value of Kleene's strong three-valued logic. -/
+inductive Value where
+  | true
+  | false
+  | unknown
+  deriving DecidableEq, Repr, Fintype
+
+namespace Value
+
+/-- Kleene negation. -/
+def not : Value → Value
+  | .true => .false
+  | .false => .true
+  | .unknown => .unknown
+
+/-- Kleene conjunction. -/
+def and : Value → Value → Value
+  | .true, b => b
+  | .false, _ => .false
+  | .unknown, .false => .false
+  | .unknown, _ => .unknown
+
+/-- Kleene disjunction. -/
+def or : Value → Value → Value
+  | .true, _ => .true
+  | .false, b => b
+  | .unknown, .true => .true
+  | .unknown, _ => .unknown
+
+instance : HasNot Value := ⟨not⟩
+instance : HasAnd Value := ⟨and⟩
+instance : HasOr Value := ⟨or⟩
+
+/-- Kleene implication, `¬a ∨ b`. -/
+def imp (a b : Value) : Value := ¬a ∨ b
+
+instance : HasImp Value := ⟨imp⟩
+
+/-- Bi-implication, `(a → b) ∧ (b → a)`. -/
+def iff (a b : Value) : Value := (a → b) ∧ (b → a)
+
+instance : HasIff Value := ⟨iff⟩
+
+@[simp, scoped grind =] protected theorem not_def (a : Value) : not a = ¬a := rfl
+@[simp, scoped grind =] protected theorem and_def (a b : Value) : and a b = (a ∧ b) := rfl
+@[simp, scoped grind =] protected theorem or_def (a b : Value) : or a b = (a ∨ b) := rfl
+@[simp, scoped grind =] protected theorem imp_def (a b : Value) : imp a b = (a → b) := rfl
+@[simp, scoped grind =] protected theorem iff_def (a b : Value) : iff a b = (a ↔ b) := rfl
+
+/-! ### The truth order -/
+
+/-- The truth order `false < unknown < true`. -/
+instance : LE Value := ⟨fun a b => a = b ∨ a = .false ∨ b = .true⟩
+
+theorem le_def {a b : Value} : a ≤ b ↔ a = b ∨ a = .false ∨ b = .true := Iff.rfl
+
+instance : DecidableLE Value := fun _ _ => inferInstanceAs (Decidable (_ ∨ _))
+
+instance : LinearOrder Value where
+  le_refl _ := Or.inl rfl
+  le_trans := by decide
+  le_antisymm := by decide
+  le_total := by decide
+  toDecidableLE := inferInstance
+  toDecidableEq := inferInstance
+  min := and
+  max := or
+  min_def := by decide
+  max_def := by decide
+
+instance : BoundedOrder Value where
+  top := .true
+  le_top _ := Or.inr (Or.inr rfl)
+  bot := .false
+  bot_le _ := Or.inr (Or.inl rfl)
+
+@[simp, scoped grind =] theorem top_eq_true : (⊤ : Value) = .true := rfl
+@[simp, scoped grind =] theorem bot_eq_false : (⊥ : Value) = .false := rfl
+
+@[simp, scoped grind =] theorem inf_eq_and (a b : Value) : a ⊓ b = (a ∧ b) := rfl
+
+@[simp, scoped grind =] theorem sup_eq_or (a b : Value) : a ⊔ b = (a ∨ b) := rfl
+
+theorem false_lt_unknown : (.false : Value) < .unknown := by decide
+
+theorem unknown_lt_true : (.unknown : Value) < .true := by decide
+
+/-- Negation reverses the truth order. -/
+theorem not_antitone : Antitone fun a : Value => ¬a := by decide
+
+/-! ### Truth tables -/
+
+@[simp, scoped grind =] protected theorem not_true : (¬Value.true) = .false := rfl
+@[simp, scoped grind =] protected theorem not_false : (¬Value.false) = .true := rfl
+@[simp, scoped grind =] theorem not_unknown : (¬Value.unknown) = .unknown := rfl
+
+@[simp, scoped grind =] protected theorem false_and (a : Value) : (Value.false ∧ a) = .false :=
+  rfl
+@[simp, scoped grind =] protected theorem and_false (a : Value) : (a ∧ Value.false) = .false :=
+  inf_bot_eq a
+@[simp, scoped grind =] protected theorem true_and (a : Value) : (Value.true ∧ a) = a := rfl
+@[simp, scoped grind =] protected theorem and_true (a : Value) : (a ∧ Value.true) = a :=
+  inf_top_eq a
+
+@[simp, scoped grind =] protected theorem true_or (a : Value) : (Value.true ∨ a) = .true := rfl
+@[simp, scoped grind =] protected theorem or_true (a : Value) : (a ∨ Value.true) = .true :=
+  sup_top_eq a
+@[simp, scoped grind =] protected theorem false_or (a : Value) : (Value.false ∨ a) = a := rfl
+@[simp, scoped grind =] protected theorem or_false (a : Value) : (a ∨ Value.false) = a :=
+  sup_bot_eq a
+
+/-! ### Laws -/
+
+@[simp, scoped grind =] protected theorem not_not (a : Value) : (¬¬a) = a := by decide +revert
+
+@[simp, scoped grind =] protected theorem and_self (a : Value) : (a ∧ a) = a := inf_idem a
+@[simp, scoped grind =] protected theorem or_self (a : Value) : (a ∨ a) = a := sup_idem a
+
+protected theorem not_and (a b : Value) : (¬(a ∧ b)) = (¬a ∨ ¬b) := not_antitone.map_min
+protected theorem not_or (a b : Value) : (¬(a ∨ b)) = (¬a ∧ ¬b) := not_antitone.map_max
+
+/-! ### Implication -/
+
+@[scoped grind =]
+theorem imp_eq_not_or (a b : Value) : (a → b) = (¬a ∨ b) := rfl
+
+@[simp, scoped grind =] protected theorem false_imp (a : Value) : (Value.false → a) = .true :=
+  rfl
+@[simp, scoped grind =] protected theorem imp_true (a : Value) : (a → Value.true) = .true :=
+  sup_top_eq _
+@[simp, scoped grind =] protected theorem true_imp (a : Value) : (Value.true → a) = a := rfl
+@[simp, scoped grind =] protected theorem imp_false (a : Value) : (a → Value.false) = ¬a :=
+  sup_bot_eq _
+
+@[simp, scoped grind =]
+theorem unknown_imp_unknown : (Value.unknown → Value.unknown) = .unknown := rfl
+
+@[simp, scoped grind =] protected theorem true_iff (a : Value) : (Value.true ↔ a) = a := by
+  decide +revert
+@[simp, scoped grind =] protected theorem iff_true (a : Value) : (a ↔ Value.true) = a := by
+  decide +revert
+@[simp, scoped grind =] protected theorem false_iff (a : Value) : (Value.false ↔ a) = ¬a := by
+  decide +revert
+@[simp, scoped grind =] protected theorem iff_false (a : Value) : (a ↔ Value.false) = ¬a := by
+  decide +revert
+
+@[simp, scoped grind =]
+theorem unknown_iff_unknown : (Value.unknown ↔ Value.unknown) = .unknown := rfl
+
+/-! ### Testing against `true` and `false` -/
+
+@[simp] theorem and_eq_true_iff {a b : Value} : (a ∧ b) = .true ↔ a = .true ∧ b = .true :=
+  inf_eq_top_iff
+
+@[simp] theorem or_eq_true_iff {a b : Value} : (a ∨ b) = .true ↔ a = .true ∨ b = .true :=
+  max_eq_top
+
+@[simp] theorem or_eq_false_iff {a b : Value} : (a ∨ b) = .false ↔ a = .false ∧ b = .false :=
+  sup_eq_bot_iff
+
+@[simp] theorem not_eq_true_iff {a : Value} : (¬a) = .true ↔ a = .false := by decide +revert
+
+@[simp] theorem not_eq_false_iff {a : Value} : (¬a) = .false ↔ a = .true := by decide +revert
+
+/-! ### The embedding of `Bool` -/
+
+/-- The embedding of `Bool`. -/
+def ofBool : Bool → Value
+  | Bool.true => .true
+  | Bool.false => .false
+
+@[simp, scoped grind =] theorem ofBool_true : ofBool Bool.true = .true := rfl
+@[simp, scoped grind =] theorem ofBool_false : ofBool Bool.false = .false := rfl
+
+theorem ofBool_injective : Function.Injective ofBool := by decide
+
+@[simp] theorem ofBool_inj {a b : Bool} : ofBool a = ofBool b ↔ a = b := ofBool_injective.eq_iff
+
+@[simp] theorem ofBool_ne_unknown (b : Bool) : ofBool b ≠ .unknown := by decide +revert
+@[simp] theorem unknown_ne_ofBool (b : Bool) : .unknown ≠ ofBool b := (ofBool_ne_unknown b).symm
+
+@[simp, scoped grind =]
+theorem ofBool_not (b : Bool) : ofBool (!b) = ¬ofBool b := by decide +revert
+
+@[simp, scoped grind =]
+theorem ofBool_and (a b : Bool) : ofBool (a && b) = (ofBool a ∧ ofBool b) := by decide +revert
+
+@[simp, scoped grind =]
+theorem ofBool_or (a b : Bool) : ofBool (a || b) = (ofBool a ∨ ofBool b) := by decide +revert
+
+/-! ### The information order -/
+
+/-- The information order: `unknown` lies below every value, and the definite values are
+incomparable. It is distinct from the truth order `≤`. -/
+def InfoLE (a b : Value) : Prop := a = .unknown ∨ a = b
+
+@[inherit_doc] scoped infix:50 " ⊑ " => InfoLE
+
+theorem infoLE_def {a b : Value} : a ⊑ b ↔ a = .unknown ∨ a = b := Iff.rfl
+
+instance : DecidableRel InfoLE := fun _ _ => inferInstanceAs (Decidable (_ ∨ _))
+
+protected theorem InfoLE.refl (a : Value) : a ⊑ a := Or.inr rfl
+
+protected theorem InfoLE.trans {a b c : Value} : a ⊑ b → b ⊑ c → a ⊑ c := by decide +revert
+
+protected theorem InfoLE.antisymm {a b : Value} : a ⊑ b → b ⊑ a → a = b := by decide +revert
+
+instance : IsPartialOrder Value InfoLE where
+  refl := InfoLE.refl
+  trans _ _ _ := InfoLE.trans
+  antisymm _ _ := InfoLE.antisymm
+
+/-- `unknown` is the least informative value. -/
+@[simp] theorem unknown_infoLE (a : Value) : .unknown ⊑ a := Or.inl rfl
+
+@[simp] theorem infoLE_unknown_iff {a : Value} : a ⊑ .unknown ↔ a = .unknown := by
+  decide +revert
+
+/-- Definite values are maximal in the information order. -/
+@[simp] theorem ofBool_infoLE_iff {x : Bool} {b : Value} : ofBool x ⊑ b ↔ b = ofBool x := by
+  decide +revert
+
+@[simp] theorem true_infoLE_iff {b : Value} : .true ⊑ b ↔ b = .true := by decide +revert
+@[simp] theorem false_infoLE_iff {b : Value} : .false ⊑ b ↔ b = .false := by decide +revert
+
+/-! ### Monotonicity in the information order -/
+
+protected theorem InfoLE.not {a a' : Value} (h : a ⊑ a') : (¬a) ⊑ (¬a') := by decide +revert
+
+protected theorem InfoLE.and {a a' b b' : Value} (ha : a ⊑ a') (hb : b ⊑ b') :
+    (a ∧ b) ⊑ (a' ∧ b') := by decide +revert
+
+protected theorem InfoLE.or {a a' b b' : Value} (ha : a ⊑ a') (hb : b ⊑ b') :
+    (a ∨ b) ⊑ (a' ∨ b') := by decide +revert
+
+protected theorem InfoLE.imp {a a' b b' : Value} (ha : a ⊑ a') (hb : b ⊑ b') :
+    (a → b) ⊑ (a' → b') := ha.not.or hb
+
+protected theorem InfoLE.iff {a a' b b' : Value} (ha : a ⊑ a') (hb : b ⊑ b') :
+    (a ↔ b) ⊑ (a' ↔ b') := (ha.imp hb).and (hb.imp ha)
+
+/-! ### Greatest monotone extensions -/
+
+/-- Kleene negation is the greatest extension of Boolean negation that is monotone in the
+information order. -/
+theorem infoLE_not_of_extends {f : Value → Value}
+    (mono : ∀ {a a'}, a ⊑ a' → f a ⊑ f a')
+    (ext : ∀ x : Bool, f (ofBool x) = ofBool (!x)) (a : Value) : f a ⊑ (¬a) := by
+  have key (x : Bool) (ha : a ⊑ ofBool x) : f a ⊑ ofBool (!x) := ext x ▸ mono ha
+  cases a <;> simp [infoLE_def, Bool.forall_bool] at key ⊢ <;> grind
+
+/-- Kleene negation is the only extension of Boolean negation that is monotone in the information
+order. -/
+theorem eq_not_of_extends {f : Value → Value}
+    (mono : ∀ {a a'}, a ⊑ a' → f a ⊑ f a')
+    (ext : ∀ x : Bool, f (ofBool x) = ofBool (!x)) (a : Value) : f a = ¬a := by
+  have h := infoLE_not_of_extends mono ext a
+  cases a <;> simp_all
+
+/-- Kleene conjunction is the greatest extension of Boolean conjunction that is monotone in the
+information order. -/
+theorem infoLE_and_of_extends {f : Value → Value → Value}
+    (mono : ∀ {a a' b b'}, a ⊑ a' → b ⊑ b' → f a b ⊑ f a' b')
+    (ext : ∀ x y : Bool, f (ofBool x) (ofBool y) = ofBool (x && y))
+    (a b : Value) : f a b ⊑ (a ∧ b) := by
+  have key (x y : Bool) (ha : a ⊑ ofBool x) (hb : b ⊑ ofBool y) : f a b ⊑ ofBool (x && y) :=
+    ext x y ▸ mono ha hb
+  cases a <;> cases b <;> simp [infoLE_def, Bool.forall_bool] at key ⊢ <;> grind
+
+/-- Kleene disjunction is the greatest extension of Boolean disjunction that is monotone in the
+information order. -/
+theorem infoLE_or_of_extends {f : Value → Value → Value}
+    (mono : ∀ {a a' b b'}, a ⊑ a' → b ⊑ b' → f a b ⊑ f a' b')
+    (ext : ∀ x y : Bool, f (ofBool x) (ofBool y) = ofBool (x || y))
+    (a b : Value) : f a b ⊑ (a ∨ b) := by
+  have key (x y : Bool) (ha : a ⊑ ofBool x) (hb : b ⊑ ofBool y) : f a b ⊑ ofBool (x || y) :=
+    ext x y ▸ mono ha hb
+  cases a <;> cases b <;> simp [infoLE_def, Bool.forall_bool] at key ⊢ <;> grind
+
+/-! ### The equivalence with `Option Bool` -/
+
+/-- The definite values as `some`, `unknown` as `none`. -/
+def toOption : Value → Option Bool
+  | .true => some Bool.true
+  | .false => some Bool.false
+  | .unknown => none
+
+/-- `some b` as `ofBool b`, `none` as `unknown`. -/
+def ofOption : Option Bool → Value
+  | some b => ofBool b
+  | none => .unknown
+
+@[simp, scoped grind =] theorem ofOption_some (b : Bool) : ofOption (some b) = ofBool b := rfl
+@[simp, scoped grind =] theorem ofOption_none : ofOption none = .unknown := rfl
+
+@[simp, scoped grind =] theorem toOption_ofBool (b : Bool) : toOption (ofBool b) = some b := by
+  cases b <;> rfl
+@[simp, scoped grind =] theorem toOption_true : toOption .true = some Bool.true := rfl
+@[simp, scoped grind =] theorem toOption_false : toOption .false = some Bool.false := rfl
+@[simp, scoped grind =] theorem toOption_unknown : toOption .unknown = none := rfl
+
+@[simp] theorem toOption_eq_none_iff {a : Value} : toOption a = none ↔ a = .unknown := by
+  cases a <;> simp [toOption]
+
+@[simp] theorem toOption_eq_some_iff {a : Value} {b : Bool} :
+    toOption a = some b ↔ a = ofBool b := by
+  cases a <;> cases b <;> simp [toOption]
+
+@[simp, scoped grind =] theorem toOption_not (a : Value) :
+    toOption (¬a) = (toOption a).map Bool.not := by cases a <;> rfl
+
+@[simp, scoped grind =] theorem ofOption_toOption (a : Value) : ofOption (toOption a) = a := by
+  cases a <;> rfl
+@[simp, scoped grind =] theorem toOption_ofOption (o : Option Bool) :
+    toOption (ofOption o) = o := by cases o <;> simp
+
+/-- `Kleene.Value` is `Option Bool` with `unknown` as `none`. -/
+@[simps (attr := scoped grind =)]
+def equivOptionBool : Value ≃ Option Bool where
+  toFun := toOption
+  invFun := ofOption
+  left_inv := ofOption_toOption
+  right_inv := toOption_ofOption
+
+/-- The information order, read through `ofOption`. -/
+@[simp] theorem ofOption_infoLE_iff {o o' : Option Bool} :
+    ofOption o ⊑ ofOption o' ↔ o = none ∨ o = o' := by
+  cases o <;> cases o' <;> simp [infoLE_def]
+
+end Value
+
+end Cslib.Logic.Kleene
diff --git a/Cslib/Logics/Kleene/Semantics.lean b/Cslib/Logics/Kleene/Semantics.lean
new file mode 100644
index 0000000000..fd7f30f392
--- /dev/null
+++ b/Cslib/Logics/Kleene/Semantics.lean
@@ -0,0 +1,310 @@
+/-
+Copyright (c) 2026 Jesse Alama. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Jesse Alama
+-/
+
+module
+
+public import Cslib.Logics.Kleene.Basic
+public import Cslib.Logics.Propositional.Defs
+public import Cslib.Foundations.Logic.InferenceSystem
+public import Cslib.Foundations.Logic.Consequence
+
+/-! # Kleene semantics for propositional logic
+
+Propositions of CSLib's propositional logic (`PL.Proposition`) are evaluated in `Kleene.Value` by
+the strong truth tables of Kleene's three-valued logic (K3) [Kleene1952]. The falsum `⊥` is an atom,
+and negation is the defined connective `¬A := A → ⊥`. Since Kleene's implication satisfies
+`a → false = ¬a`, negation is Kleene negation under valuations sending `⊥` to `false`
+(`Valuation.respectsBot`).
+
+## Main definitions
+
+- `Kleene.Valuation`: valuations of atoms in `Kleene.Value`.
+- `Kleene.Valuation.eval`: evaluation of a proposition under a valuation.
+- `Kleene.Valuation.respectsBot`: the valuations sending `⊥` to `false`.
+- `Kleene.Satisfies`, with the notation `⇓K3[v ⊨ A]`: satisfaction.
+- `Kleene.Valid`: validity, that is, satisfaction under every falsum-respecting valuation.
+- `Kleene.IsBotFree`: the propositions in which `⊥` does not occur.
+- `Kleene.Entails`: consequence, the generic notion over `Valuation.respectsBot`.
+- `Kleene.Valuation.classical` and `Kleene.ClassicalEntails`: the two-valued falsum-respecting
+  valuations, and consequence over them.
+
+## Main results
+
+- `Kleene.Valuation.eval_not`: under a falsum-respecting valuation, `¬A` evaluates to the Kleene
+  negation of the value of `A`.
+- `Kleene.Satisfies.and_iff_and` and friends: satisfaction of compound propositions in terms of
+  their components.
+- `Kleene.not_valid_of_isBotFree` and `Kleene.valid_bot_imp`: no `⊥`-free proposition is valid,
+  while `⊥ → A` is valid for every `A`.
+- `Kleene.Valuation.eval_infoLE`: evaluation is monotone in the information order `⊑` on
+  `Kleene.Value`.
+- `Kleene.not_deduction_theorem`: `A` entails `A`, but `A → A` is not valid for `⊥`-free `A`.
+- `Kleene.entails_of_mem_of_mem_not`: explosion, from `A` and `¬A` together.
+- `Kleene.Entails.classicalEntails` and `Kleene.not_entails_of_classicalEntails`: Kleene
+  consequence is strictly sub-classical. Excluded middle separates the two: it holds classically
+  for every proposition, and fails in Kleene for every `⊥`-free one.
+
+## References
+
+- [Kleene1952] S. C. Kleene, *Introduction to Metamathematics*, §64.
+-/
+
+@[expose] public section
+
+universe u
+
+namespace Cslib.Logic.Kleene
+
+open scoped InferenceSystem Value
+
+variable {Atom : Type u}
+
+/-! ### Valuations and evaluation -/
+
+/-- A valuation assigns a truth value to each atom. -/
+abbrev Valuation (Atom : Type u) := Atom → Value
+
+/-- Evaluation of a proposition under a valuation, by the truth tables of `Value`. -/
+def Valuation.eval (v : Valuation Atom) : PL.Proposition Atom → Value
+  | .atom p => v p
+  | .and A B => v.eval A ∧ v.eval B
+  | .or A B => v.eval A ∨ v.eval B
+  | .imp A B => v.eval A → v.eval B
+
+@[simp, scoped grind =]
+theorem Valuation.eval_atom (v : Valuation Atom) (p : Atom) : v.eval (.atom p) = v p := rfl
+
+@[simp, scoped grind =]
+theorem Valuation.eval_and (v : Valuation Atom) (A B : PL.Proposition Atom) :
+    v.eval (A ∧ B) = (v.eval A ∧ v.eval B) := rfl
+
+@[simp, scoped grind =]
+theorem Valuation.eval_or (v : Valuation Atom) (A B : PL.Proposition Atom) :
+    v.eval (A ∨ B) = (v.eval A ∨ v.eval B) := rfl
+
+@[simp, scoped grind =]
+theorem Valuation.eval_imp (v : Valuation Atom) (A B : PL.Proposition Atom) :
+    v.eval (A → B) = (v.eval A → v.eval B) := rfl
+
+@[simp, scoped grind =]
+theorem Valuation.eval_bot [Bot Atom] (v : Valuation Atom) : v.eval ⊥ = v ⊥ := rfl
+
+/-- Under a valuation sending `⊥` to `false`, the defined negation `¬A := A → ⊥` is Kleene
+negation. -/
+theorem Valuation.eval_not [Bot Atom] {v : Valuation Atom} (hv : v ⊥ = .false)
+    (A : PL.Proposition Atom) : v.eval (¬A) = ¬v.eval A := by
+  simp [← PL.not_eq, hv]
+
+/-- The valuations sending `⊥` to `false`. -/
+def Valuation.respectsBot [Bot Atom] : Set (Valuation Atom) := {v | v ⊥ = .false}
+
+theorem Valuation.mem_respectsBot [Bot Atom] {v : Valuation Atom} :
+    v ∈ Valuation.respectsBot ↔ v ⊥ = .false := Iff.rfl
+
+/-! ### Satisfaction -/
+
+/-- `Satisfies v A` means that `A` evaluates to `true` under the valuation `v`. -/
+def Satisfies (v : Valuation Atom) (A : PL.Proposition Atom) : Prop := v.eval A = .true
+
+/-- A judgement `K3[v ⊨ A]`, pairing a valuation with a proposition. -/
+structure Judgement (Atom : Type u) where
+  /-- The valuation. -/
+  v : Valuation Atom
+  /-- The proposition. -/
+  A : PL.Proposition Atom
+
+@[inherit_doc Judgement] scoped notation "K3[" v " ⊨ " A "]" => Judgement.mk v A
+
+instance : HasInferenceSystem (Judgement Atom) := ⟨fun j => Satisfies j.v j.A⟩
+
+@[scoped grind =]
+theorem Satisfies.eval_eq_true_iff {v : Valuation Atom} {A : PL.Proposition Atom} :
+    ⇓K3[v ⊨ A] ↔ v.eval A = .true := Iff.rfl
+
+@[simp, scoped grind =]
+theorem Satisfies.atom_iff {v : Valuation Atom} {p : Atom} :
+    ⇓K3[v ⊨ .atom p] ↔ v p = .true := Iff.rfl
+
+@[scoped grind =]
+theorem Satisfies.and_iff_and {v : Valuation Atom} {A B : PL.Proposition Atom} :
+    ⇓K3[v ⊨ A ∧ B] ↔ ⇓K3[v ⊨ A] ∧ ⇓K3[v ⊨ B] := Value.and_eq_true_iff
+
+@[scoped grind =]
+theorem Satisfies.or_iff_or {v : Valuation Atom} {A B : PL.Proposition Atom} :
+    ⇓K3[v ⊨ A ∨ B] ↔ ⇓K3[v ⊨ A] ∨ ⇓K3[v ⊨ B] := Value.or_eq_true_iff
+
+@[scoped grind =]
+theorem Satisfies.imp_iff {v : Valuation Atom} {A B : PL.Proposition Atom} :
+    ⇓K3[v ⊨ A → B] ↔ v.eval A = .false ∨ ⇓K3[v ⊨ B] := by
+  simp [Satisfies.eval_eq_true_iff, Value.imp_eq_not_or]
+
+@[scoped grind =]
+theorem Satisfies.not_iff_eval_eq_false [Bot Atom] {v : Valuation Atom} (hv : v ⊥ = .false)
+    {A : PL.Proposition Atom} : ⇓K3[v ⊨ ¬A] ↔ v.eval A = .false := by
+  rw [Satisfies.eval_eq_true_iff, Valuation.eval_not hv, Value.not_eq_true_iff]
+
+/-- The converse fails, since `A` may be `unknown`. -/
+theorem Satisfies.not_satisfies_of_not [Bot Atom] {v : Valuation Atom} (hv : v ⊥ = .false)
+    {A : PL.Proposition Atom} (h : ⇓K3[v ⊨ ¬A]) : ¬⇓K3[v ⊨ A] := by
+  grind [Satisfies.not_iff_eval_eq_false hv]
+
+/-! ### Judgemental contexts -/
+
+/-- A judgemental context is a valuation: the judgement `K3[v ⊨ A]` with the proposition missing. -/
+instance : HasHContext (Judgement Atom) (PL.Proposition Atom) :=
+  ⟨fun (v : Valuation Atom) A => K3[v ⊨ A]⟩
+
+@[simp, scoped grind =]
+theorem Judgement.fill_def {v : Valuation Atom} {A : PL.Proposition Atom} :
+    HasHContext.fill (α := Judgement Atom) v A = K3[v ⊨ A] := rfl
+
+/-! ### Validity -/
+
+/-- A proposition is valid if it is satisfied under every falsum-respecting valuation. -/
+abbrev Valid [Bot Atom] (A : PL.Proposition Atom) : Prop :=
+  ValidWithin (Judgement Atom) InferenceSystem.Default Valuation.respectsBot A
+
+/-- A proposition is `⊥`-free if the atom `⊥` does not occur in it. Since `¬A := A → ⊥`, no
+negation is `⊥`-free. -/
+inductive IsBotFree [Bot Atom] : PL.Proposition Atom → Prop
+  /-- An atom other than `⊥`. -/
+  | atom {p : Atom} (h : p ≠ ⊥) : IsBotFree (.atom p)
+  /-- Conjunction. -/
+  | and {A B : PL.Proposition Atom} (hA : IsBotFree A) (hB : IsBotFree B) : IsBotFree (A ∧ B)
+  /-- Disjunction. -/
+  | or {A B : PL.Proposition Atom} (hA : IsBotFree A) (hB : IsBotFree B) : IsBotFree (A ∨ B)
+  /-- Implication. -/
+  | imp {A B : PL.Proposition Atom} (hA : IsBotFree A) (hB : IsBotFree B) : IsBotFree (A → B)
+
+open Classical in
+/-- The valuation sending `⊥` to `false` and every other atom to `unknown`. -/
+noncomputable def Valuation.unknownExceptBot [Bot Atom] : Valuation Atom :=
+  fun p => if p = ⊥ then .false else .unknown
+
+theorem Valuation.unknownExceptBot_mem_respectsBot [Bot Atom] :
+    (Valuation.unknownExceptBot : Valuation Atom) ∈ Valuation.respectsBot := by
+  simp [Valuation.mem_respectsBot, Valuation.unknownExceptBot]
+
+theorem Valuation.eval_unknownExceptBot [Bot Atom] {A : PL.Proposition Atom} (h : IsBotFree A) :
+    Valuation.unknownExceptBot.eval A = .unknown := by
+  induction h <;> simp [Valuation.unknownExceptBot, *]
+
+theorem Valid.eval_unknownExceptBot [Bot Atom] {A : PL.Proposition Atom} (h : Valid A) :
+    Valuation.unknownExceptBot.eval A = .true :=
+  h _ Valuation.unknownExceptBot_mem_respectsBot
+
+/-- No `⊥`-free proposition is valid: all are `unknown` under `Valuation.unknownExceptBot`. -/
+theorem not_valid_of_isBotFree [Bot Atom] {A : PL.Proposition Atom} (h : IsBotFree A) :
+    ¬Valid A := fun hv => by
+  simpa [Valuation.eval_unknownExceptBot h] using hv.eval_unknownExceptBot
+
+/-- By contrast, explosion is valid, since `⊥` evaluates to `false`. -/
+theorem valid_bot_imp [Bot Atom] (A : PL.Proposition Atom) : Valid (⊥ → A) := fun _ hv => by
+  simp [Satisfies.eval_eq_true_iff, Valuation.mem_respectsBot.mp hv]
+
+/-- Excluded middle fails for `⊥`-free `A`. -/
+theorem not_valid_or_not [Bot Atom] {A : PL.Proposition Atom} (h : IsBotFree A) :
+    ¬Valid (A ∨ ¬A) := fun hv => by
+  simpa [Valuation.eval_not Valuation.unknownExceptBot_mem_respectsBot,
+    Valuation.eval_unknownExceptBot h] using hv.eval_unknownExceptBot
+
+/-- Even `A → A` fails for `⊥`-free `A`, since `unknown → unknown = unknown`. -/
+theorem not_valid_imp_self [Bot Atom] {A : PL.Proposition Atom} (h : IsBotFree A) :
+    ¬Valid (A → A) := fun hv => by
+  simpa [Valuation.eval_unknownExceptBot h] using hv.eval_unknownExceptBot
+
+/-! ### Monotonicity in the information order -/
+
+/-- Evaluation is monotone in the information order: refining the values of the atoms refines
+the value of every proposition. -/
+theorem Valuation.eval_infoLE {v v' : Valuation Atom} (h : ∀ p, v p ⊑ v' p)
+    (A : PL.Proposition Atom) : v.eval A ⊑ v'.eval A := by
+  induction A with
+  | atom p => exact h p
+  | and _ _ ih₁ ih₂ => exact ih₁.and ih₂
+  | or _ _ ih₁ ih₂ => exact ih₁.or ih₂
+  | imp _ _ ih₁ ih₂ => exact ih₁.imp ih₂
+
+/-! ### Consequence -/
+
+/-- Consequence over falsum-respecting valuations: every such valuation satisfying all the premises
+satisfies the conclusion. The structural lemmas are the generic `EntailsWithin.mono` (weakening)
+and `EntailsWithin.trans` (cut). -/
+abbrev Entails [Bot Atom] (Γ : Set (PL.Proposition Atom)) (A : PL.Proposition Atom) : Prop :=
+  EntailsWithin (Judgement Atom) InferenceSystem.Default Valuation.respectsBot Γ A
+
+/-- Explosion: `A` and `¬A` together entail everything, since no falsum-respecting valuation
+satisfies both. -/
+theorem entails_of_mem_of_mem_not [Bot Atom] {Γ : Set (PL.Proposition Atom)}
+    {A : PL.Proposition Atom} (h₁ : A ∈ Γ) (h₂ : (¬A) ∈ Γ) (B : PL.Proposition Atom) :
+    Entails Γ B :=
+  entailsWithin_of_incompatible h₁ h₂
+    (fun _ hv hA hnA => Satisfies.not_satisfies_of_not hv hnA hA) B
+
+/-- The deduction theorem fails: `A` entails `A`, but `A → A` is not valid for `⊥`-free `A`. -/
+theorem not_deduction_theorem [Bot Atom] {A : PL.Proposition Atom} (h : IsBotFree A) :
+    Entails {A} A ∧ ¬Valid (A → A) :=
+  ⟨entailsWithin_of_mem (Set.mem_singleton _), not_valid_imp_self h⟩
+
+/-! ### Comparison with classical consequence -/
+
+/-- The classical valuations: two-valued and falsum-respecting. -/
+def Valuation.classical [Bot Atom] : Set (Valuation Atom) :=
+  {v | (∃ b : Atom → Bool, v = Value.ofBool ∘ b) ∧ v ⊥ = .false}
+
+theorem Valuation.classical_subset_respectsBot [Bot Atom] :
+    (Valuation.classical : Set (Valuation Atom)) ⊆ Valuation.respectsBot :=
+  fun _ h => h.2
+
+/-- Consequence over classical valuations. -/
+abbrev ClassicalEntails [Bot Atom] (Γ : Set (PL.Proposition Atom)) (A : PL.Proposition Atom) :
+    Prop :=
+  EntailsWithin (Judgement Atom) InferenceSystem.Default Valuation.classical Γ A
+
+/-- Kleene consequence is sub-classical: whatever follows in Kleene follows classically. -/
+theorem Entails.classicalEntails [Bot Atom] {Γ : Set (PL.Proposition Atom)}
+    {A : PL.Proposition Atom} (h : Entails Γ A) : ClassicalEntails Γ A :=
+  h.anti Valuation.classical_subset_respectsBot
+
+/-- Under a two-valued valuation, every proposition evaluates to a classical truth value. -/
+theorem Valuation.exists_eval_ofBool_eq (b : Atom → Bool) (A : PL.Proposition Atom) :
+    ∃ c : Bool, Valuation.eval (Value.ofBool ∘ b) A = Value.ofBool c := by
+  induction A with
+  | atom p => exact ⟨b p, rfl⟩
+  | and _ _ ih₁ ih₂ =>
+    obtain ⟨c₁, hc₁⟩ := ih₁
+    obtain ⟨c₂, hc₂⟩ := ih₂
+    exact ⟨c₁ && c₂, by simp [Valuation.eval, hc₁, hc₂]⟩
+  | or _ _ ih₁ ih₂ =>
+    obtain ⟨c₁, hc₁⟩ := ih₁
+    obtain ⟨c₂, hc₂⟩ := ih₂
+    exact ⟨c₁ || c₂, by simp [Valuation.eval, hc₁, hc₂]⟩
+  | imp _ _ ih₁ ih₂ =>
+    obtain ⟨c₁, hc₁⟩ := ih₁
+    obtain ⟨c₂, hc₂⟩ := ih₂
+    exact ⟨!c₁ || c₂, by simp [Valuation.eval, hc₁, hc₂, Value.imp_eq_not_or]⟩
+
+/-- Excluded middle holds classically, for every proposition. -/
+theorem classicalEntails_or_not [Bot Atom] (A : PL.Proposition Atom) :
+    ClassicalEntails ∅ (A ∨ ¬A) := by
+  rintro v ⟨⟨b, rfl⟩, hv⟩ _
+  obtain ⟨c, hc⟩ := Valuation.exists_eval_ofBool_eq b A
+  cases c <;> simp [Satisfies.eval_eq_true_iff, Valuation.eval_not hv, hc]
+
+/-- Excluded middle fails in Kleene for `⊥`-free `A`. -/
+theorem not_entails_or_not [Bot Atom] {A : PL.Proposition Atom} (h : IsBotFree A) :
+    ¬Entails ∅ (A ∨ ¬A) :=
+  fun h' => not_valid_or_not h (validWithin_iff_entailsWithin_empty.mpr h')
+
+/-- Kleene consequence is strictly sub-classical. Some atom other than `⊥` is needed, since
+otherwise every proposition has its value fixed by `⊥`. -/
+theorem not_entails_of_classicalEntails [Bot Atom] [Nontrivial Atom] :
+    ¬∀ (Γ : Set (PL.Proposition Atom)) (A : PL.Proposition Atom),
+      ClassicalEntails Γ A → Entails Γ A := by
+  obtain ⟨p, hp⟩ := exists_ne (⊥ : Atom)
+  exact fun h => not_entails_or_not (IsBotFree.atom hp) (h ∅ _ (classicalEntails_or_not _))
+
+end Cslib.Logic.Kleene
diff --git a/Cslib/Logics/README.md b/Cslib/Logics/README.md
index 5837889a01..a69ad49afc 100644
--- a/Cslib/Logics/README.md
+++ b/Cslib/Logics/README.md
@@ -21,6 +21,8 @@ We adopt a unified approach to proof systems and semantics, whereby they instant
 
 When defining logical equivalence for a given inference system, instantiate `LogicalEquivalence`. This class also acts as a check that you use the correct APIs.
 
+When defining semantic consequence or validity, instantiate `HasHContext` for your judgements, with models as the judgemental contexts, and use `Entails` and `Valid` from [Foundations/Logic/Consequence](../Foundations/Logic/Consequence.lean). See [Kleene](Kleene) for an example.
+
 ### Proof relevance in proof systems
 
 A recurring choice when defining a proof system (like a sequent calculus) is whether they should go into `Prop` (proof irrelevance) or a `Type` (proof relevance).
diff --git a/references.bib b/references.bib
index 2191bd6fc6..e6f5bb478b 100644
--- a/references.bib
+++ b/references.bib
@@ -655,3 +655,13 @@ @article{Huntington1933b
  volume = {35},
  year = {1933}
 }
+
+@book{Kleene1952,
+  author    = {Kleene, Stephen Cole},
+  title     = {Introduction to Metamathematics},
+  publisher = {North-Holland},
+  address   = {Amsterdam},
+  year      = {1952},
+  series    = {Bibliotheca Mathematica},
+  volume    = {1}
+}