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-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.gap: abbreviation for .indet, used in homogeneity contexts
Truth3.neg, join, meet: Strong Kleene connectives
Lattice instances: false < indet < true

source

inductive Core.Duality.Truth3 :

Type

Three-valued truth.

true : Truth3
false : Truth3
indet : Truth3

Instances For

source

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

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.instBEqTruth3.beq :

Truth3 → Truth3 → Bool

Equations

Core.Duality.instBEqTruth3.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

Instances For

source

instance Core.Duality.instBEqTruth3 :

BEq Truth3

Equations

Core.Duality.instBEqTruth3 = { beq := Core.Duality.instBEqTruth3.beq }

source

def Core.Duality.instInhabitedTruth3.default :

Truth3

Equations

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

Instances For

source

instance Core.Duality.instInhabitedTruth3 :

Inhabited Truth3

Equations

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

source

@[reducible, inline]

abbrev Core.Duality.Truth3.gap :

Truth3

Alias for indet, used in homogeneity contexts where the third value represents a truth-value gap (some but not all atoms satisfy the predicate).

Equations

Core.Duality.Truth3.gap = Core.Duality.Truth3.indet

Instances For

source

def Core.Duality.Truth3.neg :

Truth3 → Truth3

Kleene strong negation.

Equations

Instances For

source

def Core.Duality.Truth3.join :

Truth3 → Truth3 → Truth3

Existential aggregation (Strong Kleene disjunction).

Equations

Instances For

source

def Core.Duality.Truth3.meet :

Truth3 → Truth3 → Truth3

Universal aggregation (Strong Kleene conjunction).

Equations

Instances For

source

def Core.Duality.Truth3.le :

Truth3 → Truth3 → Bool

Lattice ordering: false < indet < true.

Equations

Instances For

source

instance Core.Duality.Truth3.instLE :

LE Truth3

Equations

Core.Duality.Truth3.instLE = { le := fun (a b : Core.Duality.Truth3) => a.le b = true }

source

instance Core.Duality.Truth3.instPreorder :

Preorder Truth3

Equations

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

source

instance Core.Duality.Truth3.instPartialOrder :

PartialOrder Truth3

Equations

Core.Duality.Truth3.instPartialOrder = { toPreorder := Core.Duality.Truth3.instPreorder, le_antisymm := Core.Duality.Truth3.instPartialOrder._proof_1 }

source

instance Core.Duality.Truth3.instSemilatticeSup :

SemilatticeSup Truth3

Equations

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

source

instance Core.Duality.Truth3.instSemilatticeInf :

SemilatticeInf Truth3

Equations

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

source

instance Core.Duality.Truth3.instLattice :

Lattice Truth3

Equations

Core.Duality.Truth3.instLattice = { toSemilatticeSup := inferInstanceAs (SemilatticeSup Core.Duality.Truth3), inf := SemilatticeInf.inf, inf_le_left := ⋯, inf_le_right := ⋯, le_inf := ⋯ }

source

instance Core.Duality.Truth3.instBot :

Bot Truth3

Equations

Core.Duality.Truth3.instBot = { bot := Core.Duality.Truth3.false }

source

instance Core.Duality.Truth3.instTop :

Top Truth3

Equations

Core.Duality.Truth3.instTop = { top := Core.Duality.Truth3.true }

source

instance Core.Duality.Truth3.instOrderBot :

OrderBot Truth3

Equations

Core.Duality.Truth3.instOrderBot = { toBot := Core.Duality.Truth3.instBot, bot_le := Core.Duality.Truth3.instOrderBot._proof_1 }

source

instance Core.Duality.Truth3.instOrderTop :

OrderTop Truth3

Equations

Core.Duality.Truth3.instOrderTop = { toTop := Core.Duality.Truth3.instTop, le_top := Core.Duality.Truth3.instOrderTop._proof_1 }

source

instance Core.Duality.Truth3.instBoundedOrder :

BoundedOrder Truth3

Equations

Core.Duality.Truth3.instBoundedOrder = { toOrderTop := inferInstanceAs (OrderTop Core.Duality.Truth3), toOrderBot := inferInstanceAs (OrderBot Core.Duality.Truth3) }

source

@[simp]

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

a ⊔ true = true

source

@[simp]

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

true ⊔ a = true

source

@[simp]

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

a ⊓ false = false

source

@[simp]

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

false ⊓ a = false

source

def Core.Duality.Truth3.ofBool :

Bool → Truth3

Convert Bool to Truth3.

Equations

Instances For

source

def Core.Duality.Truth3.isDefined :

Truth3 → Bool

Check if defined (not indet).

Equations

Instances For

source

def Core.Duality.Truth3.toBoolOrFalse :

Truth3 → Bool

Convert to Bool if defined, else default to false.

Equations

Instances For

source

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

v.neg.neg = v

Negation is involutive.

source

theorem Core.Duality.Truth3.neg_indet :

indet.neg = indet

Negation preserves indet.

source

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

a.meet b = b.meet a

Conjunction is commutative.

source

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

a.join b = b.join a

Disjunction is commutative.

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

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

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

Conjunction agrees with Bool when both defined.

source

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

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

Disjunction agrees with Bool when both defined.

source

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

(ofBool a).neg = ofBool !a

Negation agrees with Bool.

source

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

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

Conjunction is associative.

source

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

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

Disjunction is associative.

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: maps indet to false. Makes any trivalent value bivalent by treating undefinedness as falsity.

Equations

Instances For

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 = Bool.true

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 = Bool.true) :

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 = Bool.true) :

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 = Bool.true) :

a.joinMiddle b = a.join b

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

source

theorem Core.Duality.Truth3.weak_refines_middle_join (a b : Truth3) (h : a.joinWeak b ≠ indet) :

a.joinMiddle b = a.joinWeak b

Weak Kleene refines Middle Kleene disjunction: when Weak Kleene gives a defined answer, Middle Kleene agrees.

source

theorem Core.Duality.Truth3.middle_refines_strong_join (a b : Truth3) (h : a.joinMiddle b ≠ indet) :

a.join b = a.joinMiddle b

Middle Kleene refines Strong Kleene disjunction: when Middle Kleene gives a defined answer, Strong Kleene agrees.

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.Truth3.GapPolicy :

Type

How undefined/gap values behave under logical connectives.

Four truth-functional systems for three-valued logic:

Strong Kleene: gap propagates unless the defined operand forces the result (false ∧ _ = false, true ∨ _ = true)
Middle Kleene: left-gap absorbs; left-defined uses Strong Kleene. Both conjunction and disjunction are asymmetric. (@cite{peters-1979}, @cite{beaver-krahmer-2001})
Weak Kleene: gap always propagates (both operands must be defined)
Belnap: gap is skipped (only defined operands contribute; gap is the identity element for both ∧ and ∨)

Policy	gap ∧ T	gap ∧ F	F ∧ gap	T ∨ gap	gap ∨ T
Strong	gap	F	F	T	T
Middle	gap	gap	F	T	gap
Weak	gap	gap	gap	gap	gap
Belnap	T	F	F	T	T

strongKleene : GapPolicy
middleKleene : GapPolicy
weakKleene : GapPolicy
belnap : GapPolicy

Instances For

source

instance Core.Duality.Truth3.instDecidableEqGapPolicy :

DecidableEq GapPolicy

Equations

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

source

def Core.Duality.Truth3.instReprGapPolicy.repr :

GapPolicy → ℕ → Std.Format

Equations

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

Instances For

source

instance Core.Duality.Truth3.instReprGapPolicy :

Repr GapPolicy

Equations

Core.Duality.Truth3.instReprGapPolicy = { reprPrec := Core.Duality.Truth3.instReprGapPolicy.repr }

source

def Core.Duality.Truth3.instBEqGapPolicy.beq :

GapPolicy → GapPolicy → Bool

Equations

Core.Duality.Truth3.instBEqGapPolicy.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

Instances For

source

instance Core.Duality.Truth3.instBEqGapPolicy :

BEq GapPolicy

Equations

Core.Duality.Truth3.instBEqGapPolicy = { beq := Core.Duality.Truth3.instBEqGapPolicy.beq }

source

def Core.Duality.Truth3.meet3 :

GapPolicy → Truth3 → Truth3 → Truth3

Parametric conjunction indexed by gap policy.

Equations

Instances For

source

def Core.Duality.Truth3.join3 :

GapPolicy → Truth3 → Truth3 → Truth3

Parametric disjunction indexed by gap policy.

Equations

Instances For

source

theorem Core.Duality.Truth3.meet3_agree_defined (pol : GapPolicy) (a b : Bool) :

meet3 pol (ofBool a) (ofBool b) = ofBool (a && b)

All four gap policies agree on fully defined inputs.

source

theorem Core.Duality.Truth3.join3_agree_defined (pol : GapPolicy) (a b : Bool) :

join3 pol (ofBool a) (ofBool b) = ofBool (a || b)

All four gap policies agree on fully defined inputs (disjunction).

source

theorem Core.Duality.Truth3.strong_refines_belnap (a b : Truth3) (h : a.meet b ≠ indet) :

a.meetBelnap b = a.meet b

Strong Kleene refines Belnap: when Strong Kleene gives a defined answer, Belnap agrees.

source

theorem Core.Duality.Truth3.weak_refines_strong (a b : Truth3) (h : a.meetWeak b ≠ indet) :

a.meet b = a.meetWeak b

Weak Kleene refines Strong Kleene: when Weak Kleene gives a defined answer, Strong Kleene agrees.

The definedness hierarchy #

The four gap policies form a hierarchy in terms of how often they produce defined (non-#) results:

Weak Kleene ≤ Middle Kleene ≤ Strong Kleene ≤ Belnap

Weak Kleene: # is absorbing — both operands must be defined.
Middle Kleene: # absorbs from the left; if left is defined, Strong Kleene applies. The left-to-right asymmetry captures presupposition filtering (@cite{peters-1979}, @cite{beaver-krahmer-2001}, @cite{spector-2025}).
Strong Kleene: # propagates unless the defined operand forces the result (false ∧ # = false, true ∨ # = true).
Belnap: # is the identity — undefined operands are skipped entirely (@cite{belnap-1970}).

The refinement property: if a weaker system produces a defined result, every stronger system agrees on that result. The systems only disagree on cases where the weaker one yields # but the stronger one rescues a defined value.

source