Three-Valued Truth #

@cite{kleene-1952}

Three-valued truth type for trivalent semantics across linglib. Used for:

Plural predication: homogeneity gaps (all satisfy → true, none → false, some but not all → gap). @cite{kriz-2016}, @cite{kriz-spector-2021}
Conditionals: indeterminacy under supervaluation when selection functions disagree. @cite{ramotowska-marty-romoli-santorio-2025}
Presupposition: undefined when presupposition fails.
Duality: existential vs universal aggregation over three-valued lists.

Main definitions #

Truth3: three-valued truth (.true, .false, .indet)
Truth3.neg, join, meet: Strong Kleene connectives
Lattice instances: false < indet < true

Three-valued truth: the 3-element bounded chain false < indet < true. Strong Kleene logic (@cite{kleene-1952}) corresponds to the order-derived operations: meet = min = ⊓, join = max = ⊔, neg is the order-reversing involution.

true : Truth3
false : Truth3
indet : Truth3

Instances For

source

@[implicit_reducible]

instance Core.Duality.instReprTruth3 :

Repr Truth3

Equations

Core.Duality.instReprTruth3 = { reprPrec := Core.Duality.instReprTruth3.repr }

source

def Core.Duality.instReprTruth3.repr :

Truth3 → ℕ → Std.Format

Equations

Core.Duality.instReprTruth3.repr Core.Duality.Truth3.true prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Core.Duality.Truth3.true")).group prec✝
Core.Duality.instReprTruth3.repr Core.Duality.Truth3.false prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Core.Duality.Truth3.false")).group prec✝
Core.Duality.instReprTruth3.repr Core.Duality.Truth3.indet prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Core.Duality.Truth3.indet")).group prec✝

Instances For

source

@[implicit_reducible]

instance Core.Duality.instDecidableEqTruth3 :

DecidableEq Truth3

Equations

Core.Duality.instDecidableEqTruth3 x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

source

def Core.Duality.instInhabitedTruth3.default :

Truth3

Equations

Core.Duality.instInhabitedTruth3.default = Core.Duality.Truth3.true

Instances For

source

@[implicit_reducible]

instance Core.Duality.instInhabitedTruth3 :

Inhabited Truth3

Equations

Core.Duality.instInhabitedTruth3 = { default := Core.Duality.instInhabitedTruth3.default }

source

def Core.Duality.Truth3.le :

Truth3 → Truth3 → Prop

Chain order: false < indet < true. Prop-valued (not Bool-wrapped) so the Decidable instance reduces under rfl and decide.

Equations

Core.Duality.Truth3.false.le x✝ = True
Core.Duality.Truth3.indet.le Core.Duality.Truth3.false = False
Core.Duality.Truth3.indet.le x✝ = True
Core.Duality.Truth3.true.le Core.Duality.Truth3.true = True
x✝¹.le x✝ = False

Instances For

source

@[implicit_reducible]

instance Core.Duality.Truth3.instLE :

LE Truth3

Equations

Core.Duality.Truth3.instLE = { le := Core.Duality.Truth3.le }

source

@[implicit_reducible]

instance Core.Duality.Truth3.instDecLE (a b : Truth3) :

Decidable (a ≤ b)

Term-mode Decidable instance — reduces eagerly under rfl/decide, enabling clean kernel-level computation through the chain order.

Equations

Core.Duality.Truth3.false.instDecLE b = isTrue trivial
Core.Duality.Truth3.indet.instDecLE Core.Duality.Truth3.false = isFalse not_false
Core.Duality.Truth3.indet.instDecLE Core.Duality.Truth3.indet = isTrue trivial
Core.Duality.Truth3.indet.instDecLE Core.Duality.Truth3.true = isTrue trivial
Core.Duality.Truth3.true.instDecLE Core.Duality.Truth3.false = isFalse not_false
Core.Duality.Truth3.true.instDecLE Core.Duality.Truth3.indet = isFalse not_false
Core.Duality.Truth3.true.instDecLE Core.Duality.Truth3.true = isTrue trivial

source

@[implicit_reducible]

instance Core.Duality.Truth3.instLinearOrder :

LinearOrder Truth3

Equations

One or more equations did not get rendered due to their size.

source

@[implicit_reducible]

instance Core.Duality.Truth3.instBoundedOrder :

BoundedOrder Truth3

Equations

One or more equations did not get rendered due to their size.

Strong Kleene operations #

Strong Kleene meet/join on a chain ARE min/max. The bespoke meet/join names are kept as @[reducible] defs so 91 downstream call sites continue to work, but the canonical mathlib operations (⊓/⊔/min/max) are preferred.

source

@[reducible]

def Core.Duality.Truth3.meet :

Truth3 → Truth3 → Truth3

Strong Kleene meet (= min on the chain false < indet < true).

Equations

Core.Duality.Truth3.meet = min

Instances For

source

@[reducible]

def Core.Duality.Truth3.join :

Truth3 → Truth3 → Truth3

Strong Kleene join (= max on the chain false < indet < true).

Equations

Core.Duality.Truth3.join = max

Instances For

source

def Core.Duality.Truth3.neg :

Truth3 → Truth3

Strong Kleene negation: order-reversing involution. false ↔ true, indet fixed.

Equations

Instances For

source

@[simp]

theorem Core.Duality.Truth3.neg_neg (a : Truth3) :

a.neg.neg = a

source

@[simp]

theorem Core.Duality.Truth3.neg_indet :

indet.neg = indet

source

theorem Core.Duality.Truth3.neg_involutive :

Function.Involutive neg

Mathlib-derived simp lemmas #

These are inherited from BoundedOrder + Lattice + LinearOrder and re-exposed under the bespoke meet/join names for downstream search.

source

@[simp]

theorem Core.Duality.Truth3.sup_true (a : Truth3) :

max a true = true

source

@[simp]

theorem Core.Duality.Truth3.true_sup (a : Truth3) :

max true a = true

source

@[simp]

theorem Core.Duality.Truth3.inf_false (a : Truth3) :

min a false = false

source

@[simp]

theorem Core.Duality.Truth3.false_inf (a : Truth3) :

min false a = false

source

def Core.Duality.Truth3.ofBool :

Bool → Truth3

Convert Bool to Truth3.

Equations

Core.Duality.Truth3.ofBool true = Core.Duality.Truth3.true
Core.Duality.Truth3.ofBool false = Core.Duality.Truth3.false

Instances For

source

def Core.Duality.Truth3.isDefined :

Truth3 → Prop

Check if defined (not indet).

Equations

Core.Duality.Truth3.true.isDefined = True
Core.Duality.Truth3.false.isDefined = True
Core.Duality.Truth3.indet.isDefined = False

Instances For

source

@[implicit_reducible]

instance Core.Duality.Truth3.instDecidablePredIsDefined :

DecidablePred isDefined

Equations

One or more equations did not get rendered due to their size.

source

def Core.Duality.Truth3.toBoolOrFalse :

Truth3 → Bool

Convert to Bool if defined, else default to false.

Equations

Core.Duality.Truth3.true.toBoolOrFalse = true
Core.Duality.Truth3.false.toBoolOrFalse = false
Core.Duality.Truth3.indet.toBoolOrFalse = false

Instances For

source

theorem Core.Duality.Truth3.meet_comm (a b : Truth3) :

a.meet b = b.meet a

Conjunction is commutative. (= min_comm)

source

theorem Core.Duality.Truth3.join_comm (a b : Truth3) :

a.join b = b.join a

Disjunction is commutative. (= max_comm)

source

theorem Core.Duality.Truth3.meet_false_left (a : Truth3) :

false.meet a = false

false is absorbing for conjunction.

source

theorem Core.Duality.Truth3.meet_false_right (a : Truth3) :

a.meet false = false

source

theorem Core.Duality.Truth3.join_true_left (a : Truth3) :

true.join a = true

true is absorbing for disjunction.

source

theorem Core.Duality.Truth3.join_true_right (a : Truth3) :

a.join true = true

source

theorem Core.Duality.Truth3.meet_true_left (a : Truth3) :

true.meet a = a

true is identity for conjunction.

source

theorem Core.Duality.Truth3.meet_true_right (a : Truth3) :

a.meet true = a

source

theorem Core.Duality.Truth3.join_false_left (a : Truth3) :

false.join a = a

false is identity for disjunction.

source

theorem Core.Duality.Truth3.join_false_right (a : Truth3) :

a.join false = a

source

theorem Core.Duality.Truth3.meet_indet_left (a : Truth3) (h : a ≠ false) :

indet.meet a = indet

indet propagates in conjunction (when not dominated by false).

source

theorem Core.Duality.Truth3.join_indet_left (a : Truth3) (h : a ≠ true) :

indet.join a = indet

indet propagates in disjunction (when not dominated by true).

source

@[simp]

theorem Core.Duality.Truth3.ofBool_inf (a b : Bool) :

min (ofBool a) (ofBool b) = ofBool (a && b)

Truth3.ofBool preserves ⊓/&& (canonical typeclass form).

source

@[simp]

theorem Core.Duality.Truth3.ofBool_sup (a b : Bool) :

max (ofBool a) (ofBool b) = ofBool (a || b)

Truth3.ofBool preserves ⊔/|| (canonical typeclass form).

source

theorem Core.Duality.Truth3.neg_ofBool (a : Bool) :

(ofBool a).neg = ofBool !a

Negation agrees with Bool.

source

def Core.Duality.Truth3.ofBoolHom :

BoundedLatticeHom Bool Truth3

Truth3.ofBool is a bounded lattice homomorphism from Bool into the {⊥, ⊤} sublattice of Truth3. The four homomorphism conditions follow from ofBool_sup, ofBool_inf, and the fact that ofBool false = ⊥ and ofBool true = ⊤ definitionally.

Registering this instance lets downstream consumers (e.g., Core.Duality.aggregate_*_map_ofBool) appeal to the general LatticeHom API rather than to bespoke case-split lemmas.

Equations

One or more equations did not get rendered due to their size.

Instances For

source

theorem Core.Duality.Truth3.meet_assoc (a b c : Truth3) :

(a.meet b).meet c = a.meet (b.meet c)

Conjunction is associative. (= min_assoc)

source

theorem Core.Duality.Truth3.join_assoc (a b c : Truth3) :

(a.join b).join c = a.join (b.join c)

Disjunction is associative. (= max_assoc)

source

def Core.Duality.Truth3.xor :

Truth3 → Truth3 → Truth3

Strong Kleene exclusive disjunction.

True when exactly one operand is true; false when both or neither; undefined when either operand is undefined.

Unlike inclusive disjunction (join), XOR cannot "see past" an undefined operand: join .true .indet = .true (the true operand settles the result), but xor .true .indet = .indet (we need to know the other's value to determine XOR).

@cite{wang-davidson-2026} Figure 2.

Equations

Instances For

source

theorem Core.Duality.Truth3.xor_comm (a b : Truth3) :

a.xor b = b.xor a

XOR is commutative.

source

theorem Core.Duality.Truth3.xor_eq_join_meet_neg (a b : Truth3) :

a.xor b = (a.join b).meet (a.meet b).neg

XOR decomposes as (a ∨ b) ∧ ¬(a ∧ b) under Strong Kleene.

source

theorem Core.Duality.Truth3.xor_indet_left (a : Truth3) :

indet.xor a = indet

XOR propagates indet unconditionally from the left.

source

theorem Core.Duality.Truth3.xor_indet_right (a : Truth3) :

a.xor indet = indet

XOR propagates indet unconditionally from the right.

source

theorem Core.Duality.Truth3.xor_ofBool (a b : Bool) :

(ofBool a).xor (ofBool b) = ofBool (a ^^ b)

XOR agrees with Bool XOR on defined inputs.

source

theorem Core.Duality.Truth3.xor_indet_iff (a b : Truth3) :

a.xor b = indet ↔ a = indet ∨ b = indet

Uniform projection under XOR: XOR returns undefined iff at least one operand is undefined. This is the semantic core of @cite{wang-davidson-2026}'s prediction: exclusive disjunction does not filter presuppositions.

Contrast with inclusive disjunction (join), where join .true .indet = .true — a true first disjunct "filters" the second's presupposition failure.

source

def Core.Duality.Truth3.joinWeak :

Truth3 → Truth3 → Truth3

Weak Kleene disjunction: indet is absorbing (both operands must be defined).

Equations

Instances For

source

def Core.Duality.Truth3.meetWeak :

Truth3 → Truth3 → Truth3

Weak Kleene conjunction: indet is absorbing.

Equations

Instances For

source

def Core.Duality.Truth3.metaAssert :

Truth3 → Truth3

Meta-assertion operator: the 𝒜 (assertion) operator of @cite{beaver-krahmer-2001} §2. Maps .indet to .false, making any trivalent value bivalent by treating undefinedness as falsity. Used for "transplication" / closing trivalent contexts to Bool.

Equations

Instances For

source

@[simp]

theorem Core.Duality.Truth3.metaAssert_true :

true.metaAssert = true

source

@[simp]

theorem Core.Duality.Truth3.metaAssert_false :

false.metaAssert = false

source

@[simp]

theorem Core.Duality.Truth3.metaAssert_indet :

indet.metaAssert = false

source

theorem Core.Duality.Truth3.joinWeak_comm (a b : Truth3) :

a.joinWeak b = b.joinWeak a

source

theorem Core.Duality.Truth3.meetWeak_comm (a b : Truth3) :

a.meetWeak b = b.meetWeak a

source

theorem Core.Duality.Truth3.metaAssert_defined (v : Truth3) :

v.metaAssert.isDefined

Meta-assertion always produces a defined value.

source

theorem Core.Duality.Truth3.metaAssert_idempotent (v : Truth3) :

v.metaAssert.metaAssert = v.metaAssert

Meta-assertion is idempotent.

source

theorem Core.Duality.Truth3.metaAssert_of_defined (v : Truth3) (h : v.isDefined) :

v.metaAssert = v

Meta-assertion preserves defined values.

source

def Core.Duality.Truth3.meetMiddle :

Truth3 → Truth3 → Truth3

Middle Kleene conjunction: left-undefined absorbs; left-defined follows Strong Kleene. Asymmetric: false ∧ # = false but # ∧ false = #.

This captures left-to-right evaluation for conjunction (@cite{peters-1979}, @cite{beaver-krahmer-2001}, @cite{spector-2025}): if the first conjunct is undefined, the result is undefined regardless of the second. If the first conjunct is defined, Strong Kleene applies.

meetMiddle	true	false	indet
true	true	false	indet
false	false	false	false
indet	indet	indet	indet

Equations

Core.Duality.Truth3.indet.meetMiddle x✝ = Core.Duality.Truth3.indet
x✝¹.meetMiddle x✝ = x✝¹.meet x✝

Instances For

source

def Core.Duality.Truth3.joinMiddle :

Truth3 → Truth3 → Truth3

Middle Kleene disjunction: left-undefined absorbs; left-defined follows Strong Kleene. Asymmetric: true ∨ # = true but # ∨ true = #.

This captures left-to-right presupposition filtering (@cite{peters-1979}): if the first disjunct is defined, its truth value can settle the result even when the second is undefined. But if the first is undefined, the whole disjunction is undefined regardless of the second.

joinMiddle	true	false	indet
true	true	true	true
false	true	false	indet
indet	indet	indet	indet

Equations

Core.Duality.Truth3.indet.joinMiddle x✝ = Core.Duality.Truth3.indet
x✝¹.joinMiddle x✝ = x✝¹.join x✝

Instances For

source

theorem Core.Duality.Truth3.meetMiddle_not_comm :

¬∀ (a b : Truth3), a.meetMiddle b = b.meetMiddle a

Middle Kleene conjunction is NOT commutative. meetMiddle false indet = false but meetMiddle indet false = indet.

source

theorem Core.Duality.Truth3.meetMiddle_eq_meet_of_left_defined (a b : Truth3) (h : a.isDefined) :

a.meetMiddle b = a.meet b

When the left operand is defined, Middle Kleene conjunction equals Strong Kleene conjunction.

source

theorem Core.Duality.Truth3.joinMiddle_not_comm :

¬∀ (a b : Truth3), a.joinMiddle b = b.joinMiddle a

Middle Kleene disjunction is NOT commutative. joinMiddle true indet = true but joinMiddle indet true = indet.

source

theorem Core.Duality.Truth3.meetMiddle_indet_left (a : Truth3) :

indet.meetMiddle a = indet

Left-undefined absorbs Middle Kleene conjunction.

source

theorem Core.Duality.Truth3.joinMiddle_indet_left (a : Truth3) :

indet.joinMiddle a = indet

Left-undefined absorbs Middle Kleene disjunction.

source

theorem Core.Duality.Truth3.meetMiddle_true_left (a : Truth3) :

true.meetMiddle a = a

true is left identity for Middle Kleene conjunction: true ∧ ψ = ψ. When the first conjunct is true, the result is just the second conjunct.

source

theorem Core.Duality.Truth3.meetMiddle_false_left (a : Truth3) :

false.meetMiddle a = false

false is left zero for Middle Kleene conjunction: false ∧ ψ = false for all ψ. This is the key asymmetry vs Weak Kleene: meetMiddle false indet = false (defined operand absorbs via Strong Kleene) whereas meetWeak false indet = indet.

source

theorem Core.Duality.Truth3.joinMiddle_false_left (a : Truth3) :

false.joinMiddle a = a

false is left identity for Middle Kleene disjunction: false ∨ ψ = ψ. When the first disjunct is false, the result is just the second disjunct.

source

theorem Core.Duality.Truth3.meetMiddle_ofBool (a b : Bool) :

(ofBool a).meetMiddle (ofBool b) = ofBool (a && b)

Middle Kleene conjunction agrees with Bool on defined inputs.

source

theorem Core.Duality.Truth3.joinMiddle_ofBool (a b : Bool) :

(ofBool a).joinMiddle (ofBool b) = ofBool (a || b)

Middle Kleene disjunction agrees with Bool on defined inputs.

source

theorem Core.Duality.Truth3.joinMiddle_eq_join_of_left_defined (a b : Truth3) (h : a.isDefined) :

a.joinMiddle b = a.join b

When the left operand is defined, Middle Kleene disjunction equals Strong Kleene disjunction.

source

def Core.Duality.Truth3.meetBelnap :

Truth3 → Truth3 → Truth3

Belnap conjunction: undefined operands are skipped.

If one operand is undefined, the result equals the other. If both are undefined, the result is undefined. This models @cite{belnap-1970}'s (8): conjunction is assertive iff at least one conjunct is assertive; what it asserts = conjunction of assertive conjuncts only. indet is the identity element.

meetBelnap	true	false	indet
true	true	false	true
false	false	false	false
indet	true	false	indet

Contrast: Strong Kleene meet (indet propagates unless dominated), Weak Kleene meetWeak (indet always propagates).

Equations

Core.Duality.Truth3.indet.meetBelnap x✝ = x✝
x✝.meetBelnap Core.Duality.Truth3.indet = x✝
x✝¹.meetBelnap x✝ = x✝¹.meet x✝

Instances For

source

def Core.Duality.Truth3.joinBelnap :

Truth3 → Truth3 → Truth3

Belnap disjunction: undefined operands are skipped.

Models @cite{belnap-1970}'s (9): disjunction is assertive iff at least one disjunct is assertive; what it asserts = disjunction of assertive disjuncts only. indet is the identity element.

Equations

Core.Duality.Truth3.indet.joinBelnap x✝ = x✝
x✝.joinBelnap Core.Duality.Truth3.indet = x✝
x✝¹.joinBelnap x✝ = x✝¹.join x✝

Instances For

source

theorem Core.Duality.Truth3.meetBelnap_indet_left (a : Truth3) :

indet.meetBelnap a = a

indet is left identity for Belnap conjunction.

source

theorem Core.Duality.Truth3.meetBelnap_indet_right (a : Truth3) :

a.meetBelnap indet = a

indet is right identity for Belnap conjunction.

source

theorem Core.Duality.Truth3.meetBelnap_comm (a b : Truth3) :

a.meetBelnap b = b.meetBelnap a

Belnap conjunction is commutative.

source

theorem Core.Duality.Truth3.joinBelnap_indet_left (a : Truth3) :

indet.joinBelnap a = a

indet is left identity for Belnap disjunction.

source

theorem Core.Duality.Truth3.joinBelnap_indet_right (a : Truth3) :

a.joinBelnap indet = a

indet is right identity for Belnap disjunction.

source

theorem Core.Duality.Truth3.joinBelnap_comm (a b : Truth3) :

a.joinBelnap b = b.joinBelnap a

Belnap disjunction is commutative.

source

theorem Core.Duality.Truth3.meetBelnap_ofBool (a b : Bool) :

(ofBool a).meetBelnap (ofBool b) = ofBool (a && b)

Belnap conjunction agrees with Bool on defined inputs.

source

theorem Core.Duality.Truth3.joinBelnap_ofBool (a b : Bool) :

(ofBool a).joinBelnap (ofBool b) = ofBool (a || b)

Belnap disjunction agrees with Bool on defined inputs.

source

inductive Core.Duality.ProjectionType :

Type

How truth values aggregate through an operator. Conjunctive (universal-like): all must succeed. Disjunctive (existential-like): one must succeed.

conjunctive : ProjectionType
disjunctive : ProjectionType

Instances For

source

@[implicit_reducible]

instance Core.Duality.instReprProjectionType :

Repr ProjectionType

Equations

Core.Duality.instReprProjectionType = { reprPrec := Core.Duality.instReprProjectionType.repr }

source

def Core.Duality.instReprProjectionType.repr :

ProjectionType → ℕ → Std.Format

Equations

One or more equations did not get rendered due to their size.

Instances For

source

@[implicit_reducible]

instance Core.Duality.instDecidableEqProjectionType :

DecidableEq ProjectionType

Equations

Core.Duality.instDecidableEqProjectionType x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

source

@[reducible, inline]

abbrev Core.Duality.Prop3 (W : Type u_1) :

Type u_1

Three-valued propositions: functions from worlds to Truth3.

Equations

Core.Duality.Prop3 W = (W → Core.Duality.Truth3)

Instances For

Prop3 W := W → Truth3 is a Pi type. The Lattice (W → Truth3) instance auto-derives from Pi.instLattice once Truth3 has Lattice (via LinearOrder), so (p ⊔ q) w = p w ⊔ q w and (p ⊓ q) w = p w ⊓ q w come for free from mathlib's Pi.sup_apply / Pi.inf_apply. Use · ⊔ · / · ⊓ · directly instead of bespoke Prop3.or/Prop3.and wrappers.

The only Truth3-specific operation that needs a pointwise lift here
is `metaAssert` (Beaver-Krahmer 𝒜) — there's no `Pi`-equivalent of
a unary type-collapsing operator.

source

def Core.Duality.Prop3.metaAssert {W : Type u_1} (p : Prop3 W) :

Prop3 W

Pointwise meta-assertion (Beaver-Krahmer 𝒜 operator).

Equations

p.metaAssert w = (p w).metaAssert

Instances For

source

@[simp]

theorem Core.Duality.Prop3.metaAssert_apply {W : Type u_1} (p : Prop3 W) (w : W) :

p.metaAssert w = (p w).metaAssert

Documentation

Linglib.Core.Logic.Truth3

Three-Valued Truth #

Main definitions #

Strong Kleene operations #

Mathlib-derived simp lemmas #