Three-valued truth

Trivalent is the three-element bounded chain false < indet < true: the value space of strong Kleene logic ([Kle52]), the bilattice literature's THREE ([Fit94]), and the consistent fragment of Belnap's FOUR. Strong Kleene conjunction and disjunction are the chain's ⊓/⊔; the carrier is logic-neutral, hosting the rival trivalent connective families — Weak Kleene ([Boc37]), Middle Kleene ([Pet79]), Belnap conditional assertion ([Bel70]) — and the partiality operators ∂ and 𝒜 of [BK01].

The upstreamable algebra is the Order.KleeneAlgebra class (Core/Order/DeMorganAlgebra/Defs.lean), of which Trivalent is the canonical non-Boolean instance. The dedicated carrier with truth-named constructors is this library's ergonomic choice; the name follows the Boolean precedent — an adjective nominalized as its truth-value type — with the Trivalent namespace hosting the whole trivalent development (this file's algebra, Core/ModelTheory/Trivalent.lean's formulas).

Main definitions

• Trivalent — three-valued truth (.true, .false, .indet), a LinearOrder and BoundedOrder. Trivalent propositions W → Trivalent live in Core/Logic/Trivalent/Prop3.lean.
• Trivalent.neg — Strong Kleene negation: involutive (neg_neg), antitone (neg_antitone), De Morgan (neg_inf/neg_sup), satisfying the Kleene law (inf_neg_le_sup_neg) — so Trivalent is an Order.KleeneAlgebra, the canonical non-Boolean instance (inf_compl_indet_ne_bot).
• Trivalent.meetWeak/joinWeak, meetMiddle/joinMiddle, meetBelnap/joinBelnap, xor — the rival connective families.
• Trivalent.presuppose, Trivalent.metaAssert — the ∂ and 𝒜 operators of [BK01].
• Trivalent.ofBool, Trivalent.ofBoolHom — Bool embeds as a bounded lattice homomorphism.

Main results

• Trivalent.orderIsoSignType — the truth order's mathlib carrier is SignType (-1 < 0 < 1), the iso commuting with negation. The knowledge order and the Kleene bilattice live in Core/Logic/Trivalent/Bilattice.lean.

References

[Kle52] [Boc37] [Bel70] [Pet79] [BK01] [CERvR12] [WD26]

inductive Trivalent : Type

Three-valued truth: the 3-element bounded chain false < indet < true. Strong Kleene logic ([Kle52]) corresponds to the order-derived operations: conjunction is ⊓ (= min), disjunction ⊔ (= max), and neg the order-reversing involution.

• true : Trivalent
• false : Trivalent
• indet : Trivalent

@[implicit_reducible]

instance instReprTrivalent : Repr Trivalent

Equations

• instReprTrivalent = { reprPrec := instReprTrivalent.repr }

def instReprTrivalent.repr : Trivalent → ℕ → Std.Format

Equations

• instReprTrivalent.repr Trivalent.true prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Trivalent.true")).group prec✝
• instReprTrivalent.repr Trivalent.false prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Trivalent.false")).group prec✝
• instReprTrivalent.repr Trivalent.indet prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Trivalent.indet")).group prec✝

@[implicit_reducible]

instance instDecidableEqTrivalent : DecidableEq Trivalent

Equations

• instDecidableEqTrivalent x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance instInhabitedTrivalent : Inhabited Trivalent

Equations

• instInhabitedTrivalent = { default := instInhabitedTrivalent.default }

@[implicit_reducible]

instance instFintypeTrivalent : Fintype Trivalent

Equations

• instFintypeTrivalent = { elems := { val := ↑Trivalent.enumList, nodup := Trivalent.enumList_nodup }, complete := instFintypeTrivalent._proof_1 }

The truth order

inductive Trivalent.LE : Trivalent → Trivalent → Prop

The less-than-or-equal relation on truth values: false < indet < true.

• of_false (a : Trivalent) : false.LE a
• indet : Trivalent.indet.LE Trivalent.indet
• of_true (a : Trivalent) : a.LE true

@[implicit_reducible]

instance Trivalent.instLE : LE Trivalent

Equations

• Trivalent.instLE = { le := Trivalent.LE }

@[implicit_reducible]

instance Trivalent.instDecidableLE : DecidableLE Trivalent

Equations

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

@[implicit_reducible]

instance Trivalent.instLinearOrder : LinearOrder Trivalent

Equations

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

@[implicit_reducible]

instance Trivalent.instBoundedOrder : BoundedOrder Trivalent

Equations

• Trivalent.instBoundedOrder = { top := Trivalent.true, le_top := ⋯, bot := Trivalent.false, bot_le := ⋯ }

Strong Kleene negation

Strong Kleene meet/join on a chain ARE min/max = ⊓/⊔; use the mathlib operations directly. Negation is the remaining primitive.

def Trivalent.neg : Trivalent → Trivalent

Strong Kleene negation: the order-reversing involution swapping false and true, fixing indet.

Equations

• Trivalent.true.neg = Trivalent.false
• Trivalent.indet.neg = Trivalent.indet
• Trivalent.false.neg = Trivalent.true

@[simp]

theorem Trivalent.neg_neg (a : Trivalent) : a.neg.neg = a

@[simp]

theorem Trivalent.neg_indet : indet.neg = indet

theorem Trivalent.neg_involutive : Function.Involutive neg

theorem Trivalent.neg_antitone : Antitone neg

Strong Kleene negation is antitone (order-reversing).

@[simp]

theorem Trivalent.neg_inf (a b : Trivalent) : (min a b).neg = max a.neg b.neg

De Morgan: negation swaps meet and join — from antitonicity alone.

@[simp]

theorem Trivalent.neg_sup (a b : Trivalent) : (max a b).neg = min a.neg b.neg

De Morgan: negation swaps join and meet.

theorem Trivalent.inf_neg_le_sup_neg (a b : Trivalent) : min a a.neg ≤ max b b.neg

The Kleene law a ⊓ ¬a ≤ b ⊔ ¬b.

@[implicit_reducible]

instance Trivalent.instCompl : Compl Trivalent

Equations

• Trivalent.instCompl = { compl := Trivalent.neg }

@[implicit_reducible]

instance Trivalent.instKleeneAlgebra : Order.KleeneAlgebra Trivalent

Trivalent is the canonical non-Boolean Kleene algebra (Order.KleeneAlgebra): a distributive chain with neg as the involutive antitone complement, failing complementation (inf_compl_indet_ne_bot). The ᶜ instance gives access to the class API (Core/Order/DeMorganAlgebra/Defs.lean); neg remains the simp-normal form.

Equations

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

theorem Trivalent.inf_compl_indet_ne_bot : min indet indetᶜ ≠ ⊥

Trivalent is not complemented — indet witnesses the gap between Kleene and Boolean (so Trivalent is no OrthocomplementedLattice either).

Constructor-literal simp lemmas

Inherited from BoundedOrder + Lattice + LinearOrder, restated with the constructor literals (⊤ = .true, ⊥ = .false) that goals actually mention.

@[simp]

theorem Trivalent.sup_true (a : Trivalent) : max a true = true

@[simp]

theorem Trivalent.true_sup (a : Trivalent) : max true a = true

@[simp]

theorem Trivalent.inf_false (a : Trivalent) : min a false = false

@[simp]

theorem Trivalent.false_inf (a : Trivalent) : min false a = false

theorem Trivalent.indet_inf (a : Trivalent) (h : a ≠ false) : min indet a = indet

indet propagates through ⊓ unless dominated by false.

theorem Trivalent.indet_sup (a : Trivalent) (h : a ≠ true) : max indet a = indet

indet propagates through ⊔ unless dominated by true.

Designated values

Matrix semantics fixes an upward-closed set of designated values; on a chain every such set is principal, so a designation standard is just a threshold. K3 (strong Kleene) designates {.true} and preserves truth; LP (Priest's Logic of Paradox) designates {.indet, .true} and preserves non-falsity ([CERvR12]). Same algebra, dual logics — and every designation law is an order law.

inductive Trivalent.Designation : Type

A designation standard, identified by its least designated value (threshold).

• k3 : Designation
• lp : Designation

@[implicit_reducible]

instance Trivalent.instReprDesignation : Repr Designation

Equations

• Trivalent.instReprDesignation = { reprPrec := Trivalent.instReprDesignation.repr }

def Trivalent.instReprDesignation.repr : Designation → ℕ → Std.Format

Equations

• Trivalent.instReprDesignation.repr Trivalent.Designation.k3 prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Trivalent.Designation.k3")).group prec✝
• Trivalent.instReprDesignation.repr Trivalent.Designation.lp prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Trivalent.Designation.lp")).group prec✝

@[implicit_reducible]

instance Trivalent.instDecidableEqDesignation : DecidableEq Designation

Equations

• Trivalent.instDecidableEqDesignation x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance Trivalent.instInhabitedDesignation : Inhabited Designation

Equations

• Trivalent.instInhabitedDesignation = { default := Trivalent.instInhabitedDesignation.default }

@[implicit_reducible]

instance Trivalent.instFintypeDesignation : Fintype Designation

Equations

• Trivalent.instFintypeDesignation = { elems := { val := ↑Trivalent.Designation.enumList, nodup := Trivalent.Designation.enumList_nodup }, complete := Trivalent.instFintypeDesignation._proof_1 }

def Trivalent.Designation.threshold : Designation → Trivalent

The threshold (least designated value) of a standard.

Equations

• Trivalent.Designation.k3.threshold = Trivalent.true
• Trivalent.Designation.lp.threshold = Trivalent.indet

def Trivalent.Designation.dual : Designation → Designation

The K3/LP duality as an involution on standards.

Equations

• Trivalent.Designation.k3.dual = Trivalent.Designation.lp
• Trivalent.Designation.lp.dual = Trivalent.Designation.k3

@[simp]

theorem Trivalent.Designation.dual_dual (d : Designation) : d.dual.dual = d

@[simp]

theorem Trivalent.Designation.dual_k3 : k3.dual = lp

@[simp]

theorem Trivalent.Designation.dual_lp : lp.dual = k3

def Trivalent.designated (d : Designation) (v : Trivalent) : Prop

v is designated at d iff it clears the threshold — the designated set is the principal filter above d.threshold.

Equations

• Trivalent.designated d v = (d.threshold ≤ v)

@[implicit_reducible]

instance Trivalent.instDecidableDesignated (d : Designation) (v : Trivalent) : Decidable (designated d v)

Equations

• Trivalent.instDecidableDesignated d v = Trivalent.instDecidableDesignated._aux_1 d v

@[simp]

theorem Trivalent.designated_k3_iff (v : Trivalent) : designated Designation.k3 v ↔ v = true

K3-designation is truth.

@[simp]

theorem Trivalent.designated_lp_iff (v : Trivalent) : designated Designation.lp v ↔ v ≠ false

LP-designation is non-falsity.

theorem Trivalent.designated_neg_iff (d : Designation) (v : Trivalent) : designated d.dual v.neg ↔ ¬designated d v

K3/LP duality via negation: negation swaps the standards (the antitone involution neg fixes indet, exchanging the two principal filters' complements).

theorem Trivalent.designated_inf (d : Designation) (v w : Trivalent) : designated d (min v w) ↔ designated d v ∧ designated d w

Designation distributes over ⊓: the designated set is a filter (le_inf_iff).

theorem Trivalent.designated_sup (d : Designation) (v w : Trivalent) : designated d (max v w) ↔ designated d v ∨ designated d w

Designation distributes over ⊔: thresholds are prime on a chain (le_sup_iff).

theorem Trivalent.designated_lp_of_k3 {v : Trivalent} (h : designated Designation.k3 v) : designated Designation.lp v

K3 is the stronger standard: its threshold dominates LP's.

Conversion from Bool

def Trivalent.ofBool : Bool → Trivalent

The two-valued fragment: Bool.true ↦ .true, Bool.false ↦ .false.

Equations

• Trivalent.ofBool true = Trivalent.true
• Trivalent.ofBool false = Trivalent.false

@[implicit_reducible]

instance Trivalent.instCoeBool : Coe Bool Trivalent

Equations

• Trivalent.instCoeBool = { coe := Trivalent.ofBool }

def Trivalent.isDefined : Trivalent → Prop

A value is defined when it is not indet.

Equations

• Trivalent.true.isDefined = True
• Trivalent.false.isDefined = True
• Trivalent.indet.isDefined = False

@[implicit_reducible]

instance Trivalent.instDecidablePredIsDefined : DecidablePred isDefined

Equations

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

def Trivalent.toBoolOrFalse : Trivalent → Bool

Project to Bool, sending indet to false.

Equations

• Trivalent.true.toBoolOrFalse = true
• Trivalent.false.toBoolOrFalse = false
• Trivalent.indet.toBoolOrFalse = false

@[simp]

theorem Trivalent.ofBool_inf (a b : Bool) : min (ofBool a) (ofBool b) = ofBool (a && b)

Trivalent.ofBool preserves ⊓/&&.

@[simp]

theorem Trivalent.ofBool_sup (a b : Bool) : max (ofBool a) (ofBool b) = ofBool (a || b)

Trivalent.ofBool preserves ⊔/||.

theorem Trivalent.neg_ofBool (a : Bool) : (ofBool a).neg = ofBool !a

Negation agrees with Bool.

theorem Trivalent.designated_ofBool (d : Designation) (b : Bool) : designated d (ofBool b) ↔ b = Bool.true

The designation standards agree on the two-valued fragment.

def Trivalent.ofBoolHom : BoundedLatticeHom Bool Trivalent

Trivalent.ofBool as a bounded lattice homomorphism, onto the {⊥, ⊤} sublattice of Trivalent — so consumers can appeal to the general LatticeHom API.

Equations

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

Exclusive disjunction

def Trivalent.xor : Trivalent → Trivalent → Trivalent

Strong Kleene exclusive disjunction: true when exactly one operand is true, undefined when either operand is. Unlike ⊔, XOR cannot "see past" an undefined operand — .true ⊔ .indet = .true, but xor .true .indet = .indet ([WD26], Figure 2).

Equations

• Trivalent.true.xor Trivalent.false = Trivalent.true
• Trivalent.false.xor Trivalent.true = Trivalent.true
• Trivalent.true.xor Trivalent.true = Trivalent.false
• Trivalent.false.xor Trivalent.false = Trivalent.false
• x✝¹.xor x✝ = Trivalent.indet

theorem Trivalent.xor_comm (a b : Trivalent) : a.xor b = b.xor a

XOR is commutative.

theorem Trivalent.xor_eq_sup_inf_neg (a b : Trivalent) : a.xor b = min (max a b) (min a b).neg

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

theorem Trivalent.xor_indet_left (a : Trivalent) : indet.xor a = indet

XOR propagates indet unconditionally from the left.

theorem Trivalent.xor_indet_right (a : Trivalent) : a.xor indet = indet

XOR propagates indet unconditionally from the right.

theorem Trivalent.xor_ofBool (a b : Bool) : (ofBool a).xor (ofBool b) = ofBool (a ^^ b)

XOR agrees with Bool XOR on defined inputs.

theorem Trivalent.xor_indet_iff (a b : Trivalent) : a.xor b = indet ↔ a = indet ∨ b = indet

XOR is undefined iff at least one operand is — so exclusive disjunction never filters undefinedness, in contrast with ⊔ (.true ⊔ .indet = .true) ([WD26]).

The truth order as SignType

Mathlib's carrier for a three-element chain with an involutive order-reversing negation fixing the midpoint is SignType (-1 < 0 < 1).

def Trivalent.orderIsoSignType : Trivalent ≃o SignType

The truth-order carrier iso: false ↔ -1, indet ↔ 0, true ↔ 1, with Kleene negation corresponding to SignType negation (orderIsoSignType_neg). The knowledge-order counterpart is equivFlatBool.

Equations

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

@[simp]

theorem Trivalent.orderIsoSignType_neg (a : Trivalent) : orderIsoSignType a.neg = -orderIsoSignType a

theorem Trivalent.orderIsoSignType_xor (a b : Trivalent) : orderIsoSignType (a.xor b) = -(orderIsoSignType a * orderIsoSignType b)

SignType multiplication transports to the Strong Kleene biconditional, so Trivalent.xor is its negation.

Weak Kleene and the Beaver-Krahmer operators

The Weak Kleene "internal" connectives originate with [Boc37] (Russian original; English translation by Bergmann 1981) and are discussed by [Kle52]: indet propagates unconditionally, matching Bochvar's "nonsense" reading of paradox-prone statements. metaAssert and presuppose are the 𝒜 and ∂ operators of [BK01] §2.

def Trivalent.joinWeak : Trivalent → Trivalent → Trivalent

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

Equations

• Trivalent.true.joinWeak Trivalent.true = Trivalent.true
• Trivalent.true.joinWeak Trivalent.false = Trivalent.true
• Trivalent.false.joinWeak Trivalent.true = Trivalent.true
• Trivalent.false.joinWeak Trivalent.false = Trivalent.false
• x✝¹.joinWeak x✝ = Trivalent.indet

def Trivalent.meetWeak : Trivalent → Trivalent → Trivalent

Weak Kleene conjunction: indet is absorbing.

Equations

• Trivalent.true.meetWeak Trivalent.true = Trivalent.true
• Trivalent.true.meetWeak Trivalent.false = Trivalent.false
• Trivalent.false.meetWeak Trivalent.true = Trivalent.false
• Trivalent.false.meetWeak Trivalent.false = Trivalent.false
• x✝¹.meetWeak x✝ = Trivalent.indet

theorem Trivalent.joinWeak_comm (a b : Trivalent) : a.joinWeak b = b.joinWeak a

theorem Trivalent.meetWeak_comm (a b : Trivalent) : a.meetWeak b = b.meetWeak a

def Trivalent.metaAssert : Trivalent → Trivalent

Meta-assertion: the 𝒜 (assertion) operator of [BK01] §2, closing a trivalent value to bivalent by treating undefinedness as falsity.

Equations

• Trivalent.true.metaAssert = Trivalent.true
• Trivalent.false.metaAssert = Trivalent.false
• Trivalent.indet.metaAssert = Trivalent.false

@[simp]

theorem Trivalent.metaAssert_true : true.metaAssert = true

@[simp]

theorem Trivalent.metaAssert_false : false.metaAssert = false

@[simp]

theorem Trivalent.metaAssert_indet : indet.metaAssert = false

theorem Trivalent.metaAssert_defined (v : Trivalent) : v.metaAssert.isDefined

Meta-assertion always produces a defined value.

theorem Trivalent.metaAssert_idempotent (v : Trivalent) : v.metaAssert.metaAssert = v.metaAssert

Meta-assertion is idempotent.

theorem Trivalent.metaAssert_of_defined (v : Trivalent) (h : v.isDefined) : v.metaAssert = v

Meta-assertion preserves defined values.

def Trivalent.presuppose : Trivalent → Trivalent

Presupposition: the ∂ operator of [BK01] §2, the companion of metaAssert — asserts a true value, undefined otherwise (T ↦ T, F ↦ #, # ↦ #).

Equations

• Trivalent.true.presuppose = Trivalent.true
• x✝.presuppose = Trivalent.indet

@[simp]

theorem Trivalent.presuppose_true : true.presuppose = true

@[simp]

theorem Trivalent.presuppose_false : false.presuppose = indet

@[simp]

theorem Trivalent.presuppose_indet : indet.presuppose = indet

theorem Trivalent.metaAssert_presuppose (v : Trivalent) : v.presuppose.metaAssert = if v = true then true else false

Meta-asserting a presupposed value falsifies undefinedness: 𝒜 ∘ ∂ sends exactly .true to .true.

Middle Kleene

The asymmetric left-to-right connectives of [Pet79], the trivalent face of Karttunen filtering ([BK01], [Spe25]): an undefined first operand absorbs; a defined one proceeds by Strong Kleene.

def Trivalent.meetMiddle : Trivalent → Trivalent → Trivalent

Middle Kleene conjunction: left-undefined absorbs, left-defined proceeds by Strong Kleene. Asymmetric — meetMiddle .false .indet = .false but meetMiddle .indet .false = .indet ([Pet79]).

Equations

• Trivalent.indet.meetMiddle x✝ = Trivalent.indet
• x✝¹.meetMiddle x✝ = min x✝¹ x✝

def Trivalent.joinMiddle : Trivalent → Trivalent → Trivalent

Middle Kleene disjunction: left-undefined absorbs, left-defined proceeds by Strong Kleene — a defined first disjunct can settle the result even when the second is undefined, the left-to-right filtering pattern ([Pet79]).

Equations

• Trivalent.indet.joinMiddle x✝ = Trivalent.indet
• x✝¹.joinMiddle x✝ = max x✝¹ x✝

theorem Trivalent.meetMiddle_not_comm : ¬∀ (a b : Trivalent), a.meetMiddle b = b.meetMiddle a

Middle Kleene conjunction is not commutative.

theorem Trivalent.joinMiddle_not_comm : ¬∀ (a b : Trivalent), a.joinMiddle b = b.joinMiddle a

Middle Kleene disjunction is not commutative.

theorem Trivalent.meetMiddle_eq_inf_of_left_defined (a b : Trivalent) (h : a.isDefined) : a.meetMiddle b = min a b

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

theorem Trivalent.joinMiddle_eq_sup_of_left_defined (a b : Trivalent) (h : a.isDefined) : a.joinMiddle b = max a b

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

theorem Trivalent.meetMiddle_indet_left (a : Trivalent) : indet.meetMiddle a = indet

Left-undefined absorbs Middle Kleene conjunction.

theorem Trivalent.joinMiddle_indet_left (a : Trivalent) : indet.joinMiddle a = indet

Left-undefined absorbs Middle Kleene disjunction.

theorem Trivalent.meetMiddle_true_left (a : Trivalent) : true.meetMiddle a = a

true is a left identity for Middle Kleene conjunction.

theorem Trivalent.meetMiddle_false_left (a : Trivalent) : false.meetMiddle a = false

false is a left zero for Middle Kleene conjunction — the key asymmetry against Weak Kleene, where meetWeak .false .indet = .indet.

theorem Trivalent.joinMiddle_false_left (a : Trivalent) : false.joinMiddle a = a

false is a left identity for Middle Kleene disjunction.

theorem Trivalent.meetMiddle_ofBool (a b : Bool) : (ofBool a).meetMiddle (ofBool b) = ofBool (a && b)

Middle Kleene conjunction agrees with Bool on defined inputs.

theorem Trivalent.joinMiddle_ofBool (a b : Bool) : (ofBool a).joinMiddle (ofBool b) = ofBool (a || b)

Middle Kleene disjunction agrees with Bool on defined inputs.

Belnap conditional assertion

[Bel70]'s connectives skip undefined operands: a compound is assertive iff at least one operand is, and asserts the combination of the assertive operands only — indet is the identity element. Contrast Strong Kleene (indet propagates unless dominated) and Weak Kleene (indet always propagates).

def Trivalent.meetBelnap : Trivalent → Trivalent → Trivalent

Belnap conjunction: undefined operands are skipped; indet is the identity ([Bel70], (8)).

Equations

• Trivalent.indet.meetBelnap x✝ = x✝
• x✝.meetBelnap Trivalent.indet = x✝
• x✝¹.meetBelnap x✝ = min x✝¹ x✝

def Trivalent.joinBelnap : Trivalent → Trivalent → Trivalent

Belnap disjunction: undefined operands are skipped; indet is the identity ([Bel70], (9)).

Equations

• Trivalent.indet.joinBelnap x✝ = x✝
• x✝.joinBelnap Trivalent.indet = x✝
• x✝¹.joinBelnap x✝ = max x✝¹ x✝

theorem Trivalent.meetBelnap_indet_left (a : Trivalent) : indet.meetBelnap a = a

indet is a left identity for Belnap conjunction.

theorem Trivalent.meetBelnap_indet_right (a : Trivalent) : a.meetBelnap indet = a

indet is a right identity for Belnap conjunction.

theorem Trivalent.meetBelnap_comm (a b : Trivalent) : a.meetBelnap b = b.meetBelnap a

Belnap conjunction is commutative.

theorem Trivalent.joinBelnap_indet_left (a : Trivalent) : indet.joinBelnap a = a

indet is a left identity for Belnap disjunction.

theorem Trivalent.joinBelnap_indet_right (a : Trivalent) : a.joinBelnap indet = a

indet is a right identity for Belnap disjunction.

theorem Trivalent.joinBelnap_comm (a b : Trivalent) : a.joinBelnap b = b.joinBelnap a

Belnap disjunction is commutative.

theorem Trivalent.meetBelnap_ofBool (a b : Bool) : (ofBool a).meetBelnap (ofBool b) = ofBool (a && b)

Belnap conjunction agrees with Bool on defined inputs.

theorem Trivalent.joinBelnap_ofBool (a b : Bool) : (ofBool a).joinBelnap (ofBool b) = ofBool (a || b)

Belnap disjunction agrees with Bool on defined inputs.

Projection behaviour

inductive Trivalent.ProjectionType : Type

How truth values aggregate through an operator: conjunctive (universal-like, all must succeed) or disjunctive (existential-like, one must succeed).

• conjunctive : ProjectionType
• disjunctive : ProjectionType

@[implicit_reducible]

instance Trivalent.instReprProjectionType : Repr ProjectionType

Equations

• Trivalent.instReprProjectionType = { reprPrec := Trivalent.instReprProjectionType.repr }

def Trivalent.instReprProjectionType.repr : ProjectionType → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Trivalent.instDecidableEqProjectionType : DecidableEq ProjectionType

Equations

• Trivalent.instDecidableEqProjectionType x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯