From 8e483667380081d39ef53bc4cd7c7288cea30204 Mon Sep 17 00:00:00 2001
From: Jesse Alama <hello@jessealama.net>
Date: Fri, 23 Oct 2026 19:18:48 +0200
Subject: [PATCH 1/8] feat(Logic): truth values of Kleene's strong three-valued
 logic

---
 Cslib.lean                     |   1 +
 Cslib/Logics/Kleene/Basic.lean | 245 +++++++++++++++++++++++++++++++++
 references.bib                 |  10 ++
 3 files changed, 256 insertions(+)
 create mode 100644 Cslib/Logics/Kleene/Basic.lean

diff --git a/Cslib.lean b/Cslib.lean
index 1c70985ff2..311aaf53c6 100644
--- a/Cslib.lean
+++ b/Cslib.lean
@@ -249,6 +249,7 @@ 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.LinearLogic.CLL.Basic
 public import Cslib.Logics.LinearLogic.CLL.CutElimination
 public import Cslib.Logics.LinearLogic.CLL.EtaExpansion
diff --git a/Cslib/Logics/Kleene/Basic.lean b/Cslib/Logics/Kleene/Basic.lean
new file mode 100644
index 0000000000..2bed6bf44f
--- /dev/null
+++ b/Cslib/Logics/Kleene/Basic.lean
@@ -0,0 +1,245 @@
+/-
+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`. These are the semantic domain for the propositions in
+`Cslib.Logics.Kleene.Semantics`.
+
+## 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`.
+
+## 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.
+
+## 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 and_comm (a b : Value) : (a ∧ b) = (b ∧ a) := inf_comm a b
+protected theorem or_comm (a b : Value) : (a ∨ b) = (b ∨ a) := sup_comm a b
+
+protected theorem and_assoc (a b c : Value) : ((a ∧ b) ∧ c) = (a ∧ b ∧ c) := inf_assoc a b c
+protected theorem or_assoc (a b c : Value) : ((a ∨ b) ∨ c) = (a ∨ b ∨ c) := sup_assoc a b c
+
+protected theorem and_or_left (a b c : Value) : (a ∧ (b ∨ c)) = (a ∧ b ∨ a ∧ c) :=
+  inf_sup_left a b c
+protected theorem or_and_left (a b c : Value) : (a ∨ b ∧ c) = ((a ∨ b) ∧ (a ∨ c)) :=
+  sup_inf_left a b c
+
+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 grind
+
+@[simp] theorem not_eq_false_iff {a : Value} : (¬a) = .false ↔ a = .true := by grind
+
+/-! ### 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 grind [cases Bool]
+
+@[simp, scoped grind =]
+theorem ofBool_not (b : Bool) : ofBool (!b) = ¬ofBool b := by grind [cases Bool]
+
+@[simp, scoped grind =]
+theorem ofBool_and (a b : Bool) : ofBool (a && b) = (ofBool a ∧ ofBool b) := by grind [cases Bool]
+
+@[simp, scoped grind =]
+theorem ofBool_or (a b : Bool) : ofBool (a || b) = (ofBool a ∨ ofBool b) := by grind [cases Bool]
+
+end Value
+
+end Cslib.Logic.Kleene
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}
+}

From 4f26f83e16fabb2260fd311dcf9c6499b37b6d0c Mon Sep 17 00:00:00 2001
From: Jesse Alama <hello@jessealama.net>
Date: Fri, 23 Oct 2026 19:21:34 +0200
Subject: [PATCH 2/8] feat(Logic): Kleene semantics for propositional logic

---
 Cslib.lean                         |   1 +
 Cslib/Logics/Kleene/Semantics.lean | 144 +++++++++++++++++++++++++++++
 2 files changed, 145 insertions(+)
 create mode 100644 Cslib/Logics/Kleene/Semantics.lean

diff --git a/Cslib.lean b/Cslib.lean
index 311aaf53c6..16d4db9ad0 100644
--- a/Cslib.lean
+++ b/Cslib.lean
@@ -250,6 +250,7 @@ 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/Logics/Kleene/Semantics.lean b/Cslib/Logics/Kleene/Semantics.lean
new file mode 100644
index 0000000000..39f0ea97f6
--- /dev/null
+++ b/Cslib/Logics/Kleene/Semantics.lean
@@ -0,0 +1,144 @@
+/-
+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
+
+/-! # 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`. This is a
+condition on valuations (`Valuation.respectsBot`), not built into the type of valuations.
+
+## 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.
+
+## 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. `¬A` is satisfied iff `A` evaluates to `false`; unlike classically, this is
+  stronger than `A` not being satisfied, since `A` may be `unknown`.
+
+## 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 derivation_def {v : Valuation Atom} {A : PL.Proposition Atom} :
+    Satisfies v A = ⇓K3[v ⊨ A] := rfl
+
+@[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 evaluate to `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]
+
+end Cslib.Logic.Kleene

From 7fc6eeba4682e135cfa622e76f0994efe9c3ebfb Mon Sep 17 00:00:00 2001
From: Jesse Alama <hello@jessealama.net>
Date: Fri, 23 Oct 2026 19:23:04 +0200
Subject: [PATCH 3/8] feat(Logic): validities in Kleene come only from falsum

---
 Cslib/Logics/Kleene/Semantics.lean | 64 ++++++++++++++++++++++++++++++
 1 file changed, 64 insertions(+)

diff --git a/Cslib/Logics/Kleene/Semantics.lean b/Cslib/Logics/Kleene/Semantics.lean
index 39f0ea97f6..dad464f0e6 100644
--- a/Cslib/Logics/Kleene/Semantics.lean
+++ b/Cslib/Logics/Kleene/Semantics.lean
@@ -24,6 +24,8 @@ condition on valuations (`Valuation.respectsBot`), not built into the type of va
 - `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.
 
 ## Main results
 
@@ -32,6 +34,9 @@ condition on valuations (`Valuation.respectsBot`), not built into the type of va
 - `Kleene.Satisfies.and_iff_and` and friends: satisfaction of compound propositions in terms of
   their components. `¬A` is satisfied iff `A` evaluates to `false`; unlike classically, this is
   stronger than `A` not being satisfied, since `A` may be `unknown`.
+- `Kleene.not_valid_of_isBotFree` and `Kleene.valid_bot_imp`: with a falsum in the language the
+  only validities come from `⊥`. No `⊥`-free proposition is valid, since the valuation sending every
+  other atom to `unknown` makes it `unknown`, while `⊥ → A` is valid for every `A`.
 
 ## References
 
@@ -141,4 +146,63 @@ theorem Satisfies.not_satisfies_of_not [Bot Atom] {v : Valuation Atom} (hv : v 
     {A : PL.Proposition Atom} (h : ⇓K3[v ⊨ ¬A]) : ¬⇓K3[v ⊨ A] := by
   grind [Satisfies.not_iff_eval_eq_false hv]
 
+/-! ### Validity -/
+
+/-- A proposition is valid if it is satisfied under every falsum-respecting valuation. -/
+def Valid [Bot Atom] (A : PL.Proposition Atom) : Prop := ∀ v ∈ Valuation.respectsBot, ⇓K3[v ⊨ 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)
+
+theorem isBotFree_atom_of_ne [Bot Atom] {p : Atom} (h : p ≠ ⊥) : IsBotFree (.atom p) :=
+  IsBotFree.atom h
+
+/-- The valuation sending `⊥` to `false` and every other atom to `unknown`. -/
+def Valuation.unknownExceptBot [Bot Atom] [DecidableEq Atom] : Valuation Atom :=
+  fun p => if p = ⊥ then .false else .unknown
+
+theorem Valuation.unknownExceptBot_mem_respectsBot [Bot Atom] [DecidableEq Atom] :
+    (Valuation.unknownExceptBot : Valuation Atom) ∈ Valuation.respectsBot := by
+  simp [Valuation.mem_respectsBot, Valuation.unknownExceptBot]
+
+theorem Valuation.eval_unknownExceptBot [Bot Atom] [DecidableEq Atom] {A : PL.Proposition Atom}
+    (h : IsBotFree A) : Valuation.unknownExceptBot.eval A = .unknown := by
+  induction h <;> simp [Valuation.unknownExceptBot, *]
+
+/-- 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
+  classical
+  have := hv _ Valuation.unknownExceptBot_mem_respectsBot
+  simp [Satisfies.eval_eq_true_iff, Valuation.eval_unknownExceptBot h] at this
+
+/-- 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`, which evaluates to `unknown` under
+`Valuation.unknownExceptBot`, as then does `A ∨ ¬A`. -/
+theorem not_valid_or_not [Bot Atom] {A : PL.Proposition Atom} (h : IsBotFree A) :
+    ¬Valid (A ∨ ¬A) := fun hv => by
+  classical
+  have := hv _ Valuation.unknownExceptBot_mem_respectsBot
+  simp [Satisfies.eval_eq_true_iff, Valuation.eval_not Valuation.unknownExceptBot_mem_respectsBot,
+    Valuation.eval_unknownExceptBot h] at this
+
+/-- 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
+  classical
+  have := hv _ Valuation.unknownExceptBot_mem_respectsBot
+  simp [Satisfies.eval_eq_true_iff, Valuation.eval_unknownExceptBot h] at this
+
 end Cslib.Logic.Kleene

From df3e1c3725267d611ee033963602107f2118218d Mon Sep 17 00:00:00 2001
From: Jesse Alama <hello@jessealama.net>
Date: Fri, 23 Oct 2026 20:06:11 +0200
Subject: [PATCH 4/8] refactor(Logic): trim Kleene three-valued logic

---
 Cslib/Logics/Kleene/Basic.lean     | 23 ++++---------
 Cslib/Logics/Kleene/Semantics.lean | 53 ++++++++++++------------------
 2 files changed, 27 insertions(+), 49 deletions(-)

diff --git a/Cslib/Logics/Kleene/Basic.lean b/Cslib/Logics/Kleene/Basic.lean
index 2bed6bf44f..84bbb36905 100644
--- a/Cslib/Logics/Kleene/Basic.lean
+++ b/Cslib/Logics/Kleene/Basic.lean
@@ -158,17 +158,6 @@ theorem not_antitone : Antitone fun a : Value => ¬a := by decide
 @[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 and_comm (a b : Value) : (a ∧ b) = (b ∧ a) := inf_comm a b
-protected theorem or_comm (a b : Value) : (a ∨ b) = (b ∨ a) := sup_comm a b
-
-protected theorem and_assoc (a b c : Value) : ((a ∧ b) ∧ c) = (a ∧ b ∧ c) := inf_assoc a b c
-protected theorem or_assoc (a b c : Value) : ((a ∨ b) ∨ c) = (a ∨ b ∨ c) := sup_assoc a b c
-
-protected theorem and_or_left (a b c : Value) : (a ∧ (b ∨ c)) = (a ∧ b ∨ a ∧ c) :=
-  inf_sup_left a b c
-protected theorem or_and_left (a b c : Value) : (a ∨ b ∧ c) = ((a ∨ b) ∧ (a ∨ c)) :=
-  sup_inf_left a b c
-
 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
 
@@ -211,9 +200,9 @@ theorem unknown_iff_unknown : (Value.unknown ↔ Value.unknown) = .unknown := rf
 @[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 grind
+@[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 grind
+@[simp] theorem not_eq_false_iff {a : Value} : (¬a) = .false ↔ a = .true := by decide +revert
 
 /-! ### The embedding of `Bool` -/
 
@@ -229,16 +218,16 @@ 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 grind [cases Bool]
+@[simp] theorem ofBool_ne_unknown (b : Bool) : ofBool b ≠ .unknown := by decide +revert
 
 @[simp, scoped grind =]
-theorem ofBool_not (b : Bool) : ofBool (!b) = ¬ofBool b := by grind [cases Bool]
+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 grind [cases Bool]
+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 grind [cases Bool]
+theorem ofBool_or (a b : Bool) : ofBool (a || b) = (ofBool a ∨ ofBool b) := by decide +revert
 
 end Value
 
diff --git a/Cslib/Logics/Kleene/Semantics.lean b/Cslib/Logics/Kleene/Semantics.lean
index dad464f0e6..5c208cf9c5 100644
--- a/Cslib/Logics/Kleene/Semantics.lean
+++ b/Cslib/Logics/Kleene/Semantics.lean
@@ -15,8 +15,8 @@ public import Cslib.Foundations.Logic.InferenceSystem
 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`. This is a
-condition on valuations (`Valuation.respectsBot`), not built into the type of valuations.
+`a → false = ¬a`, negation is Kleene negation under valuations sending `⊥` to `false`
+(`Valuation.respectsBot`).
 
 ## Main definitions
 
@@ -32,11 +32,9 @@ condition on valuations (`Valuation.respectsBot`), not built into the type of va
 - `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. `¬A` is satisfied iff `A` evaluates to `false`; unlike classically, this is
-  stronger than `A` not being satisfied, since `A` may be `unknown`.
-- `Kleene.not_valid_of_isBotFree` and `Kleene.valid_bot_imp`: with a falsum in the language the
-  only validities come from `⊥`. No `⊥`-free proposition is valid, since the valuation sending every
-  other atom to `unknown` makes it `unknown`, while `⊥ → A` is valid for every `A`.
+  their components.
+- `Kleene.not_valid_of_isBotFree` and `Kleene.valid_bot_imp`: no `⊥`-free proposition is valid,
+  while `⊥ → A` is valid for every `A`.
 
 ## References
 
@@ -49,7 +47,7 @@ universe u
 
 namespace Cslib.Logic.Kleene
 
-open scoped InferenceSystem Value
+open scoped InferenceSystem
 
 variable {Atom : Type u}
 
@@ -111,10 +109,6 @@ structure Judgement (Atom : Type u) where
 
 instance : HasInferenceSystem (Judgement Atom) := ⟨fun j => Satisfies j.v j.A⟩
 
-@[scoped grind =]
-theorem derivation_def {v : Valuation Atom} {A : PL.Proposition Atom} :
-    Satisfies v A = ⇓K3[v ⊨ A] := rfl
-
 @[scoped grind =]
 theorem Satisfies.eval_eq_true_iff {v : Valuation Atom} {A : PL.Proposition Atom} :
     ⇓K3[v ⊨ A] ↔ v.eval A = .true := Iff.rfl
@@ -141,7 +135,7 @@ theorem Satisfies.not_iff_eval_eq_false [Bot Atom] {v : Valuation Atom} (hv : v
     {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 evaluate to `unknown`. -/
+/-- 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]
@@ -163,46 +157,41 @@ inductive IsBotFree [Bot Atom] : PL.Proposition Atom → Prop
   /-- Implication. -/
   | imp {A B : PL.Proposition Atom} (hA : IsBotFree A) (hB : IsBotFree B) : IsBotFree (A → B)
 
-theorem isBotFree_atom_of_ne [Bot Atom] {p : Atom} (h : p ≠ ⊥) : IsBotFree (.atom p) :=
-  IsBotFree.atom h
-
+open Classical in
 /-- The valuation sending `⊥` to `false` and every other atom to `unknown`. -/
-def Valuation.unknownExceptBot [Bot Atom] [DecidableEq Atom] : Valuation Atom :=
+noncomputable def Valuation.unknownExceptBot [Bot Atom] : Valuation Atom :=
   fun p => if p = ⊥ then .false else .unknown
 
-theorem Valuation.unknownExceptBot_mem_respectsBot [Bot Atom] [DecidableEq Atom] :
+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] [DecidableEq Atom] {A : PL.Proposition Atom}
-    (h : IsBotFree A) : Valuation.unknownExceptBot.eval A = .unknown := by
+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
-  classical
-  have := hv _ Valuation.unknownExceptBot_mem_respectsBot
-  simp [Satisfies.eval_eq_true_iff, Valuation.eval_unknownExceptBot h] at this
+  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`, which evaluates to `unknown` under
-`Valuation.unknownExceptBot`, as then does `A ∨ ¬A`. -/
+/-- 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
-  classical
-  have := hv _ Valuation.unknownExceptBot_mem_respectsBot
-  simp [Satisfies.eval_eq_true_iff, Valuation.eval_not Valuation.unknownExceptBot_mem_respectsBot,
-    Valuation.eval_unknownExceptBot h] at this
+  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
-  classical
-  have := hv _ Valuation.unknownExceptBot_mem_respectsBot
-  simp [Satisfies.eval_eq_true_iff, Valuation.eval_unknownExceptBot h] at this
+  simpa [Valuation.eval_unknownExceptBot h] using hv.eval_unknownExceptBot
 
 end Cslib.Logic.Kleene

From d15b27b8a78e6bba0bd697f97d261a2ecc4e1117 Mon Sep 17 00:00:00 2001
From: Jesse Alama <hello@jessealama.net>
Date: Thu, 22 Oct 2026 15:32:08 +0200
Subject: [PATCH 5/8] feat(Logic): information order for Kleene

---
 Cslib/Logics/Kleene/Basic.lean | 63 +++++++++++++++++++++++++++++++++-
 1 file changed, 62 insertions(+), 1 deletion(-)

diff --git a/Cslib/Logics/Kleene/Basic.lean b/Cslib/Logics/Kleene/Basic.lean
index 84bbb36905..0adbd933ce 100644
--- a/Cslib/Logics/Kleene/Basic.lean
+++ b/Cslib/Logics/Kleene/Basic.lean
@@ -13,21 +13,29 @@ 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`. These are the semantic domain for the propositions in
+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.
+
 ## 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.
 
 ## 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.
 
 ## References
 
@@ -219,6 +227,7 @@ 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
@@ -229,6 +238,58 @@ theorem ofBool_and (a b : Bool) : ofBool (a && b) = (ofBool a ∧ ofBool b) := b
 @[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)
+
 end Value
 
 end Cslib.Logic.Kleene

From a9a985d96d1b0237721bdfb67ac9e1c554918c7d Mon Sep 17 00:00:00 2001
From: Jesse Alama <hello@jessealama.net>
Date: Thu, 22 Oct 2026 15:32:21 +0200
Subject: [PATCH 6/8] feat(Logic): Kleene connectives as greatest monotone
 extensions

---
 Cslib/Logics/Kleene/Basic.lean | 44 +++++++++++++++++++++++++++++++++-
 1 file changed, 43 insertions(+), 1 deletion(-)

diff --git a/Cslib/Logics/Kleene/Basic.lean b/Cslib/Logics/Kleene/Basic.lean
index 0adbd933ce..aabe4b2c5f 100644
--- a/Cslib/Logics/Kleene/Basic.lean
+++ b/Cslib/Logics/Kleene/Basic.lean
@@ -19,7 +19,8 @@ truth order `false < unknown < true` and the information order `unknown ⊑ true
 
 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.
+is monotone in it, and `∧`, `∨` and `¬` are the greatest monotone extensions of `&&`, `||`
+and `!`.
 
 ## Main definitions
 
@@ -36,6 +37,9 @@ is monotone in it.
 - `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
 
@@ -290,6 +294,44 @@ protected theorem InfoLE.imp {a a' b b' : Value} (ha : a ⊑ a') (hb : b ⊑ b')
 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
+
 end Value
 
 end Cslib.Logic.Kleene

From cf05ece6d74f2f756a3ea2d862e252ada008c149 Mon Sep 17 00:00:00 2001
From: Jesse Alama <hello@jessealama.net>
Date: Thu, 22 Oct 2026 15:32:42 +0200
Subject: [PATCH 7/8] feat(Logic): equivalence of Kleene with Option Bool

---
 Cslib/Logics/Kleene/Basic.lean | 51 ++++++++++++++++++++++++++++++++++
 1 file changed, 51 insertions(+)

diff --git a/Cslib/Logics/Kleene/Basic.lean b/Cslib/Logics/Kleene/Basic.lean
index aabe4b2c5f..5b9b5eebbf 100644
--- a/Cslib/Logics/Kleene/Basic.lean
+++ b/Cslib/Logics/Kleene/Basic.lean
@@ -29,6 +29,7 @@ and `!`.
   `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
 
@@ -332,6 +333,56 @@ theorem infoLE_or_of_extends {f : Value → Value → Value}
     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

From 5a66fc24b4626585b679fe002d0b9d6a09439389 Mon Sep 17 00:00:00 2001
From: Jesse Alama <hello@jessealama.net>
Date: Fri, 23 Oct 2026 19:24:10 +0200
Subject: [PATCH 8/8] feat(Logic): Kleene evaluation is monotone in the
 information order

---
 Cslib/Logics/Kleene/Semantics.lean | 16 +++++++++++++++-
 1 file changed, 15 insertions(+), 1 deletion(-)

diff --git a/Cslib/Logics/Kleene/Semantics.lean b/Cslib/Logics/Kleene/Semantics.lean
index 5c208cf9c5..295e24e08c 100644
--- a/Cslib/Logics/Kleene/Semantics.lean
+++ b/Cslib/Logics/Kleene/Semantics.lean
@@ -35,6 +35,8 @@ and negation is the defined connective `¬A := A → ⊥`. Since Kleene's implic
   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`.
 
 ## References
 
@@ -47,7 +49,7 @@ universe u
 
 namespace Cslib.Logic.Kleene
 
-open scoped InferenceSystem
+open scoped InferenceSystem Value
 
 variable {Atom : Type u}
 
@@ -194,4 +196,16 @@ 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₂
+
 end Cslib.Logic.Kleene