Three-valued truth

Three-valued truth adds a value between falsity and truth. Mathlib's SignType represents it, with -1, 0 and 1 for false, undefined and true: the order's meet and join are Kleene's strong conjunction and disjunction, negation is his negation, and multiplication is the biconditional, so SignType is a Kleene algebra that is not Boolean. The other three-valued conjunctions and disjunctions differ from Kleene's only in when a compound is undefined.

Main definitions

• Trivalent.Designation: the K3 and LP standards, each named by its least designated value.
• SignType.ofProp: the two-valued fragment.
• SignType.meetWith, SignType.joinWith: the conjunction and disjunction undefined exactly where a given condition fails.
• SignType.meetWeak, SignType.meetMiddle, SignType.meetBelnap and their joins: the Weak Kleene, Middle Kleene and Belnap connectives.
• SignType.condAssert: conditional assertion at a designation standard, de Finetti's conditional at K3 and Cooper's at LP.
• SignType.supervaluation: the value of a predicate over a finite family of valuations.
• Trivalent.Connectives: an interpretation of the binary connectives by truth tables, with the Strong, Weak and Middle Kleene, Cooper and de Finetti instances.

Main results

• SignType.eq_of_eq_zero_iff_of_eq_one_iff: a value is fixed by whether it is 0 and whether it is 1.
• Trivalent.Designation.dual_threshold_le_neg_iff: negation exchanges the K3 and LP standards.
• SignType.meetWeak_eq_meetWith and companions: each connective is meetWith or joinWith at its definedness condition.
• SignType.neg_condAssert, SignType.condAssert_condAssert: conditional assertion commutes with negation and satisfies Import-Export.

Implementation notes

Operations that are expressions in the order and arithmetic get no definition: Strong Kleene conjunction, disjunction and negation are ⊓, ⊔ and -, exclusive disjunction is -(a * b), Bochvar's assertion operator is ofProp (a = 1), Beaver's presupposition operator is a ⊔ 0, designation at a standard d is d.threshold ≤ a, and a Boolean b has value ofProp b. The complement of the Kleene algebra is -. Every other connective keeps a pattern-matched definition, so that rfl and decide evaluate it.

References

• [Kle52]
• [Boc38]
• [Pet79]
• [Bel70]
• [dF36]
• [Coo68]
• [Pri79]
• [CERvR12]
• [Kal58]
• [Bea92]
• [BK01]
• [vF66]

Kleene's negation

theorem SignType.eq_of_eq_zero_iff_of_eq_one_iff {a b : SignType} (h₀ : a = 0 ↔ b = 0) (h₁ : a = 1 ↔ b = 1) : a = b

Two values agree once they agree on being 0 and on being 1.

@[simp]

theorem SignType.neg_zero : -0 = 0

@[simp]

theorem SignType.neg_eq_one_iff {a : SignType} : -a = 1 ↔ a = -1

@[simp]

theorem SignType.neg_eq_neg_one_iff {a : SignType} : -a = -1 ↔ a = 1

@[simp]

theorem SignType.sup_one (a : SignType) : max a 1 = 1

@[simp]

theorem SignType.one_sup (a : SignType) : max 1 a = 1

@[simp]

theorem SignType.inf_neg_one (a : SignType) : min a (-1) = -1

@[simp]

theorem SignType.neg_one_inf (a : SignType) : min (-1) a = -1

@[simp]

theorem SignType.neg_one_ne_one : -1 ≠ 1

@[simp]

theorem SignType.one_ne_neg_one : 1 ≠ -1

@[simp]

theorem SignType.neg_one_ne_zero : -1 ≠ 0

@[simp]

theorem SignType.zero_ne_neg_one : 0 ≠ -1

@[simp]

theorem SignType.inf_one (a : SignType) : min a 1 = a

@[simp]

theorem SignType.one_inf (a : SignType) : min 1 a = a

@[simp]

theorem SignType.sup_neg_one (a : SignType) : max a (-1) = a

@[simp]

theorem SignType.neg_one_sup (a : SignType) : max (-1) a = a

@[simp]

theorem SignType.inf_eq_one_iff {a b : SignType} : min a b = 1 ↔ a = 1 ∧ b = 1

@[simp]

theorem SignType.sup_eq_neg_one_iff {a b : SignType} : max a b = -1 ↔ a = -1 ∧ b = -1

@[simp]

theorem SignType.sup_eq_one_iff {a b : SignType} : max a b = 1 ↔ a = 1 ∨ b = 1

@[simp]

theorem SignType.inf_eq_neg_one_iff {a b : SignType} : min a b = -1 ↔ a = -1 ∨ b = -1

@[simp]

theorem SignType.inf_eq_zero_iff {a b : SignType} : min a b = 0 ↔ a = 0 ∧ b ≠ -1 ∨ b = 0 ∧ a ≠ -1

@[simp]

theorem SignType.sup_eq_zero_iff {a b : SignType} : max a b = 0 ↔ a = 0 ∧ b ≠ 1 ∨ b = 0 ∧ a ≠ 1

theorem SignType.neg_antitone : Antitone Neg.neg

Negation is antitone.

@[simp]

theorem SignType.neg_inf (a b : SignType) : -min a b = max (-a) (-b)

Negation sends a meet to the join of the negations.

@[simp]

theorem SignType.neg_sup (a b : SignType) : -max a b = min (-a) (-b)

Negation sends a join to the meet of the negations.

@[instance_reducible]

instance SignType.instInvolutiveCompl : InvolutiveCompl SignType

Negation is the complement of the Kleene algebra.

Equations

• SignType.instInvolutiveCompl = { compl := Neg.neg, compl_compl := SignType.instInvolutiveCompl._proof_1, compl_le_compl := ⋯ }

@[simp]

theorem SignType.compl_eq_neg (a : SignType) : aᶜ = -a

instance SignType.instIsKleene : IsKleene SignType

SignType is [Kal58]'s three-element Kleene algebra.

theorem SignType.inf_compl_zero_ne_bot : min 0 0ᶜ ≠ ⊥

SignType is not Boolean, since 0 meets its complement above ⊥.

The two-valued fragment

def SignType.ofProp (P : Prop) [Decidable P] : SignType

The value of a decidable proposition is 1 or -1.

Equations

• SignType.ofProp P = if P then 1 else -1

@[simp]

theorem SignType.ofProp_eq_one_iff {P : Prop} [Decidable P] : ofProp P = 1 ↔ P

@[simp]

theorem SignType.ofProp_eq_neg_one_iff {P : Prop} [Decidable P] : ofProp P = -1 ↔ ¬P

@[simp]

theorem SignType.ofProp_ne_zero {P : Prop} [Decidable P] : ofProp P ≠ 0

@[simp]

theorem SignType.zero_le_ofProp_iff {P : Prop} [Decidable P] : 0 ≤ ofProp P ↔ P

A two-valued proposition is non-false exactly when it holds.

theorem SignType.ofProp_eq_one_of_ne_zero {a : SignType} [Decidable (a = 1)] (h : a ≠ 0) : ofProp (a = 1) = a

A defined value is the value of its own truth.

theorem SignType.ofProp_congr {P Q : Prop} [Decidable P] [Decidable Q] (h : P ↔ Q) : ofProp P = ofProp Q

Equivalent propositions have the same value, which lets simp rewrite inside ofProp.

@[simp]

theorem SignType.ofProp_true : ofProp True = 1

@[simp]

theorem SignType.ofProp_false : ofProp False = -1

@[simp]

theorem SignType.ofProp_and {P Q : Prop} [Decidable P] [Decidable Q] : ofProp (P ∧ Q) = min (ofProp P) (ofProp Q)

@[simp]

theorem SignType.ofProp_or {P Q : Prop} [Decidable P] [Decidable Q] : ofProp (P ∨ Q) = max (ofProp P) (ofProp Q)

@[simp]

theorem SignType.ofProp_not {P : Prop} [Decidable P] : (ofProp ¬P) = -ofProp P

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, and a value v is designated at d when d.threshold ≤ v. K3, Strong Kleene logic, designates {1} and preserves truth; LP, [Pri79]'s Logic of Paradox, designates {0, 1} and preserves non-falsity. The two standards give dual logics over one algebra ([CERvR12]), and every law of designation is a law of the order.

inductive Trivalent.Designation : Type

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

• k3 : Designation
• lp : Designation

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✝

@[instance_reducible]

instance Trivalent.instReprDesignation : Repr Designation

Equations

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

@[instance_reducible]

instance Trivalent.instDecidableEqDesignation : DecidableEq Designation

Equations

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

@[instance_reducible]

instance Trivalent.instInhabitedDesignation : Inhabited Designation

Equations

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

@[instance_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 → SignType

The least designated value of a standard.

Equations

• Trivalent.Designation.k3.threshold = 1
• Trivalent.Designation.lp.threshold = 0

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

@[simp]

theorem Trivalent.Designation.threshold_k3 : k3.threshold = 1

@[simp]

theorem Trivalent.Designation.threshold_lp : lp.threshold = 0

theorem Trivalent.Designation.dual_threshold_le_neg_iff (d : Designation) (v : SignType) : d.dual.threshold ≤ -v ↔ ¬d.threshold ≤ v

Negation swaps the designation standards, fixing 0 and exchanging the complements of the two principal filters.

theorem Trivalent.Designation.threshold_le_ofProp_iff (d : Designation) (P : Prop) [Decidable P] : d.threshold ≤ SignType.ofProp P ↔ P

The standards agree on the two-valued fragment.

Definedness conditions

The binary conjunctions share one truth rule, false when either operand is and true otherwise, and differ only in where they are undefined. Strong Kleene conjunction is defined whenever the operands settle the value, Weak Kleene's demands both operands defined, Belnap's demands one, and Middle Kleene's is defined when the left operand is and either settles the value or the right operand is defined too. meetWith makes the conjunction a function of that condition.

def SignType.meetWith (D : Prop) [Decidable D] (a b : SignType) : SignType

The conjunction undefined unless D holds, and otherwise false exactly when an operand is.

Equations

• SignType.meetWith D a b = if D then if a = -1 ∨ b = -1 then -1 else 1 else 0

def SignType.joinWith (D : Prop) [Decidable D] (a b : SignType) : SignType

The disjunction undefined unless D holds, the dual of meetWith.

Equations

• SignType.joinWith D a b = -SignType.meetWith D (-a) (-b)

theorem SignType.meetWith_eq_zero_iff {D : Prop} [Decidable D] {a b : SignType} : meetWith D a b = 0 ↔ ¬D

theorem SignType.meetWith_eq_neg_one_iff {D : Prop} [Decidable D] {a b : SignType} : meetWith D a b = -1 ↔ D ∧ (a = -1 ∨ b = -1)

theorem SignType.meetWith_eq_one_iff {D : Prop} [Decidable D] {a b : SignType} : meetWith D a b = 1 ↔ D ∧ a ≠ -1 ∧ b ≠ -1

theorem SignType.joinWith_eq_zero_iff {D : Prop} [Decidable D] {a b : SignType} : joinWith D a b = 0 ↔ ¬D

theorem SignType.joinWith_eq_one_iff {D : Prop} [Decidable D] {a b : SignType} : joinWith D a b = 1 ↔ D ∧ (a = 1 ∨ b = 1)

theorem SignType.joinWith_eq_neg_one_iff {D : Prop} [Decidable D] {a b : SignType} : joinWith D a b = -1 ↔ D ∧ a ≠ 1 ∧ b ≠ 1

theorem SignType.inf_eq_meetWith (a b : SignType) : min a b = meetWith ((a = -1 ∨ b = -1) ∨ a = 1 ∧ b = 1) a b

Strong Kleene conjunction is meetWith defined whenever the operands settle the value.

theorem SignType.sup_eq_joinWith (a b : SignType) : max a b = joinWith ((a = 1 ∨ b = 1) ∨ a = -1 ∧ b = -1) a b

Strong Kleene disjunction, dually.

Weak Kleene

In the Weak Kleene connectives 0 is absorbing, so a compound is undefined as soon as an operand is. This is [Boc38]'s internal logic, which reads the third value as nonsense, and [Kle52]'s weak tables.

def SignType.joinWeak : SignType → SignType → SignType

In Weak Kleene disjunction 0 is absorbing, so both operands must be defined.

Equations

• SignType.pos.joinWeak SignType.pos = 1
• SignType.pos.joinWeak SignType.neg = 1
• SignType.neg.joinWeak SignType.pos = 1
• SignType.neg.joinWeak SignType.neg = -1
• x✝¹.joinWeak x✝ = 0

def SignType.meetWeak : SignType → SignType → SignType

In Weak Kleene conjunction 0 is absorbing.

Equations

• SignType.pos.meetWeak SignType.pos = 1
• SignType.pos.meetWeak SignType.neg = -1
• SignType.neg.meetWeak SignType.pos = -1
• SignType.neg.meetWeak SignType.neg = -1
• x✝¹.meetWeak x✝ = 0

theorem SignType.meetWeak_eq_meetWith (a b : SignType) : a.meetWeak b = meetWith (a ≠ 0 ∧ b ≠ 0) a b

Weak Kleene conjunction is meetWith demanding both operands defined.

theorem SignType.joinWeak_eq_joinWith (a b : SignType) : a.joinWeak b = joinWith (a ≠ 0 ∧ b ≠ 0) a b

Weak Kleene disjunction, dually.

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

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

theorem SignType.meetWeak_assoc (a b c : SignType) : (a.meetWeak b).meetWeak c = a.meetWeak (b.meetWeak c)

@[simp]

theorem SignType.meetWeak_one_left (a : SignType) : meetWeak 1 a = a

@[simp]

theorem SignType.meetWeak_zero_left (a : SignType) : meetWeak 0 a = 0

@[simp]

theorem SignType.meetWeak_zero_right (a : SignType) : a.meetWeak 0 = 0

@[simp]

theorem SignType.meetWeak_eq_zero_iff (a b : SignType) : a.meetWeak b = 0 ↔ a = 0 ∨ b = 0

The Weak Kleene conjunction is undefined iff a conjunct is.

@[simp]

theorem SignType.meetWeak_eq_one_iff (a b : SignType) : a.meetWeak b = 1 ↔ a = 1 ∧ b = 1

The Weak Kleene conjunction is true iff both conjuncts are.

@[simp]

theorem SignType.meetWeak_eq_neg_one_iff (a b : SignType) : a.meetWeak b = -1 ↔ a = -1 ∧ b ≠ 0 ∨ a ≠ 0 ∧ b = -1

The Weak Kleene conjunction is false iff a conjunct is false and the other is defined.

theorem SignType.joinWeak_eq_zero_iff (a b : SignType) : a.joinWeak b = 0 ↔ a = 0 ∨ b = 0

The Weak Kleene disjunction is undefined iff a disjunct is.

theorem SignType.joinWeak_eq_neg_one_iff (a b : SignType) : a.joinWeak b = -1 ↔ a = -1 ∧ b = -1

The Weak Kleene disjunction is false iff both disjuncts are.

theorem SignType.joinWeak_eq_one_iff (a b : SignType) : a.joinWeak b = 1 ↔ a ≠ 0 ∧ b ≠ 0 ∧ (a = 1 ∨ b = 1)

The Weak Kleene disjunction is true iff both disjuncts are defined and one is true.

theorem SignType.neg_meetWeak_of_ne_neg_one {a : SignType} (h : a ≠ -1) (b : SignType) : -a.meetWeak b = a.meetWeak (-b)

Negation passes through a Weak Kleene conjunction whose first conjunct is never false.

Assertion and presupposition

The assertion operator 𝒜 of [Boc38] sends 0 to -1, closing a value to a bivalent one, and is ofProp (a = 1). The presupposition operator ∂ of [Bea92] sends -1 to 0, keeping only truth, and is a ⊔ 0. [BK01] build presupposition projection from the two.

theorem SignType.sup_zero_eq_one_iff {a : SignType} : max a 0 = 1 ↔ a = 1

theorem SignType.sup_zero_eq_zero_iff {a : SignType} : max a 0 = 0 ↔ a ≠ 1

theorem SignType.sup_zero_ne_neg_one (a : SignType) : max a 0 ≠ -1

Middle Kleene

The Middle Kleene connectives of [Pet79] read their operands from left to right. An undefined first operand absorbs, and a defined one proceeds by Strong Kleene, the three-valued counterpart of Karttunen's filtering ([BK01]).

def SignType.meetMiddle : SignType → SignType → SignType

In Middle Kleene conjunction a left undefined operand absorbs and a defined one proceeds by Strong Kleene, so meetMiddle (-1) 0 = -1 but meetMiddle 0 (-1) = 0.

Equations

• SignType.zero.meetMiddle x✝ = 0
• x✝¹.meetMiddle x✝ = min x✝¹ x✝

def SignType.joinMiddle : SignType → SignType → SignType

In Middle Kleene disjunction a left undefined operand absorbs and a defined one proceeds by Strong Kleene, so a defined first disjunct can settle the result when the second is undefined.

Equations

• SignType.zero.joinMiddle x✝ = 0
• x✝¹.joinMiddle x✝ = max x✝¹ x✝

theorem SignType.meetMiddle_eq_meetWith (a b : SignType) : a.meetMiddle b = meetWith (a ≠ 0 ∧ (a = -1 ∨ b ≠ 0)) a b

Middle Kleene conjunction is meetWith at the asymmetric condition that the left operand is defined and either settles the value or the right operand is defined too.

theorem SignType.joinMiddle_eq_joinWith (a b : SignType) : a.joinMiddle b = joinWith (a ≠ 0 ∧ (a = 1 ∨ b ≠ 0)) a b

Middle Kleene disjunction, dually.

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

Middle Kleene conjunction is not commutative.

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

Middle Kleene disjunction is not commutative.

theorem SignType.meetMiddle_eq_inf_of_left_ne_zero (a b : SignType) (h : a ≠ 0) : a.meetMiddle b = min a b

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

theorem SignType.joinMiddle_eq_sup_of_left_ne_zero (a b : SignType) (h : a ≠ 0) : a.joinMiddle b = max a b

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

@[simp]

theorem SignType.meetMiddle_zero_left (a : SignType) : meetMiddle 0 a = 0

@[simp]

theorem SignType.joinMiddle_zero_left (a : SignType) : joinMiddle 0 a = 0

@[simp]

theorem SignType.meetMiddle_one_left (a : SignType) : meetMiddle 1 a = a

@[simp]

theorem SignType.meetMiddle_neg_one_left (a : SignType) : (-1).meetMiddle a = -1

-1 is a left zero for Middle Kleene conjunction, against Weak Kleene's meetWeak (-1) 0 = 0.

@[simp]

theorem SignType.joinMiddle_neg_one_left (a : SignType) : (-1).joinMiddle a = a

@[simp]

theorem SignType.joinMiddle_one_left (a : SignType) : joinMiddle 1 a = 1

@[simp]

theorem SignType.meetMiddle_one_right (a : SignType) : a.meetMiddle 1 = a

theorem SignType.meetMiddle_congr_right {a b b' : SignType} (h : a = 1 → b = b') : a.meetMiddle b = a.meetMiddle b'

Middle Kleene conjunction reads its right argument only when its left one is true.

theorem SignType.joinMiddle_congr_right {a b b' : SignType} (h : a = -1 → b = b') : a.joinMiddle b = a.joinMiddle b'

Middle Kleene disjunction reads its right argument only when its left one is false.

@[simp]

theorem SignType.meetMiddle_eq_one_iff {a b : SignType} : a.meetMiddle b = 1 ↔ a = 1 ∧ b = 1

@[simp]

theorem SignType.meetMiddle_eq_zero_iff {a b : SignType} : a.meetMiddle b = 0 ↔ a = 0 ∨ a = 1 ∧ b = 0

Middle Kleene conjunction is undefined iff its left operand is, or the left operand is true and the right one undefined, the first conjunct filtering the second's presupposition.

@[simp]

theorem SignType.meetMiddle_eq_neg_one_iff {a b : SignType} : a.meetMiddle b = -1 ↔ a = -1 ∨ a = 1 ∧ b = -1

@[simp]

theorem SignType.joinMiddle_eq_one_iff {a b : SignType} : a.joinMiddle b = 1 ↔ a = 1 ∨ a = -1 ∧ b = 1

@[simp]

theorem SignType.joinMiddle_eq_zero_iff {a b : SignType} : a.joinMiddle b = 0 ↔ a = 0 ∨ a = -1 ∧ b = 0

Middle Kleene disjunction is undefined iff its left operand is, or the left operand is false and the right one undefined.

@[simp]

theorem SignType.joinMiddle_eq_neg_one_iff {a b : SignType} : a.joinMiddle b = -1 ↔ a = -1 ∧ b = -1

Belnap's connectives

The connectives of [Bel70]'s conditional assertion skip undefined operands: a compound is assertive iff at least one operand is, and asserts the combination of the assertive operands only, so 0 is the identity. Strong Kleene's let 0 through unless an operand settles the value, and Weak Kleene's always do.

def SignType.meetBelnap : SignType → SignType → SignType

Belnap conjunction skips undefined operands, with 0 as identity ([Bel70], (8)).

Equations

• SignType.zero.meetBelnap x✝ = x✝
• x✝.meetBelnap SignType.zero = x✝
• x✝¹.meetBelnap x✝ = min x✝¹ x✝

def SignType.joinBelnap : SignType → SignType → SignType

Belnap disjunction skips undefined operands, with 0 as identity ([Bel70], (9)).

Equations

• SignType.zero.joinBelnap x✝ = x✝
• x✝.joinBelnap SignType.zero = x✝
• x✝¹.joinBelnap x✝ = max x✝¹ x✝

theorem SignType.meetBelnap_eq_meetWith (a b : SignType) : a.meetBelnap b = meetWith (a ≠ 0 ∨ b ≠ 0) a b

Belnap conjunction is meetWith demanding one operand defined.

theorem SignType.joinBelnap_eq_joinWith (a b : SignType) : a.joinBelnap b = joinWith (a ≠ 0 ∨ b ≠ 0) a b

Belnap disjunction, dually.

@[simp]

theorem SignType.meetBelnap_zero_left (a : SignType) : meetBelnap 0 a = a

@[simp]

theorem SignType.meetBelnap_zero_right (a : SignType) : a.meetBelnap 0 = a

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

@[simp]

theorem SignType.joinBelnap_zero_left (a : SignType) : joinBelnap 0 a = a

@[simp]

theorem SignType.joinBelnap_zero_right (a : SignType) : a.joinBelnap 0 = a

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

theorem SignType.meetBelnap_eq_inf_of_ne_zero {a b : SignType} (ha : a ≠ 0) (hb : b ≠ 0) : a.meetBelnap b = min a b

On defined operands Belnap conjunction is Strong Kleene's.

@[simp]

theorem SignType.meetBelnap_eq_zero_iff {a b : SignType} : a.meetBelnap b = 0 ↔ a = 0 ∧ b = 0

Belnap conjunction is undefined iff both conjuncts are.

@[simp]

theorem SignType.meetBelnap_eq_one_iff {a b : SignType} : a.meetBelnap b = 1 ↔ a ≠ -1 ∧ b ≠ -1 ∧ (a = 1 ∨ b = 1)

@[simp]

theorem SignType.meetBelnap_eq_neg_one_iff {a b : SignType} : a.meetBelnap b = -1 ↔ a = -1 ∨ b = -1

@[simp]

theorem SignType.joinBelnap_eq_zero_iff {a b : SignType} : a.joinBelnap b = 0 ↔ a = 0 ∧ b = 0

Belnap disjunction is undefined iff both disjuncts are.

@[simp]

theorem SignType.joinBelnap_eq_one_iff {a b : SignType} : a.joinBelnap b = 1 ↔ a = 1 ∨ b = 1

@[simp]

theorem SignType.joinBelnap_eq_neg_one_iff {a b : SignType} : a.joinBelnap b = -1 ↔ a ≠ 1 ∧ b ≠ 1 ∧ (a = -1 ∨ b = -1)

theorem SignType.joinBelnap_eq_sup_of_ne_zero {a b : SignType} (ha : a ≠ 0) (hb : b ≠ 0) : a.joinBelnap b = max a b

On defined operands Belnap disjunction is Strong Kleene's.

@[simp]

theorem SignType.zero_le_meetBelnap_iff {a b : SignType} : 0 ≤ a.meetBelnap b ↔ 0 ≤ a ∧ 0 ≤ b

Belnap conjunction is non-false exactly when both conjuncts are.

Conditional assertion

A conditional assertion asserts its consequent where its antecedent holds and is void elsewhere ([Bel70]). Over a trivalent antecedent a designation standard decides what a void antecedent does: at K3 only a true antecedent passes the consequent on, the conditional of [dF36], and at LP a void antecedent does too, the conditional of [Coo68]. At either standard the conditional commutes with negation and imports and exports a conjunction.

def SignType.condAssert (d : Trivalent.Designation) (a b : SignType) : SignType

The conditional assertion of b on a at the standard d is b where a is designated and 0 elsewhere.

Equations

• SignType.condAssert d a b = if d.threshold ≤ a then b else 0

theorem SignType.condAssert_of_le {d : Trivalent.Designation} {a : SignType} (h : d.threshold ≤ a) (b : SignType) : condAssert d a b = b

theorem SignType.condAssert_of_not_le {d : Trivalent.Designation} {a : SignType} (h : ¬d.threshold ≤ a) (b : SignType) : condAssert d a b = 0

@[simp]

theorem SignType.condAssert_one_left (d : Trivalent.Designation) (b : SignType) : condAssert d 1 b = b

@[simp]

theorem SignType.condAssert_neg_one_left (d : Trivalent.Designation) (b : SignType) : condAssert d (-1) b = 0

@[simp]

theorem SignType.condAssert_k3_zero_left (b : SignType) : condAssert Trivalent.Designation.k3 0 b = 0

De Finetti's conditional groups a void antecedent with a false one.

@[simp]

theorem SignType.condAssert_lp_zero_left (b : SignType) : condAssert Trivalent.Designation.lp 0 b = b

Cooper's conditional groups a void antecedent with a true one.

theorem SignType.condAssert_eq_one_iff {d : Trivalent.Designation} {a b : SignType} : condAssert d a b = 1 ↔ d.threshold ≤ a ∧ b = 1

theorem SignType.condAssert_eq_neg_one_iff {d : Trivalent.Designation} {a b : SignType} : condAssert d a b = -1 ↔ d.threshold ≤ a ∧ b = -1

theorem SignType.condAssert_eq_zero_iff {d : Trivalent.Designation} {a b : SignType} : condAssert d a b = 0 ↔ d.threshold ≤ a → b = 0

@[simp]

theorem SignType.condAssert_ofProp {d : Trivalent.Designation} (P : Prop) [Decidable P] (b : SignType) : condAssert d (ofProp P) b = if P then b else 0

On a two-valued antecedent the standards agree: the consequent where the antecedent holds and void elsewhere.

theorem SignType.condAssert_congr_left {d : Trivalent.Designation} {a a' : SignType} (h : d.threshold ≤ a ↔ d.threshold ≤ a') (b : SignType) : condAssert d a b = condAssert d a' b

Antecedents designated alike give the same conditional.

@[simp]

theorem SignType.neg_condAssert {d : Trivalent.Designation} {a b : SignType} : -condAssert d a b = condAssert d a (-b)

Negation commutes with the conditional.

theorem SignType.condAssert_condAssert {d : Trivalent.Designation} {a b c : SignType} : condAssert d a (condAssert d b c) = condAssert d (min a b) c

Import-Export: a conditional on a of a conditional on b is the conditional on the Strong Kleene conjunction a ⊓ b, which is designated exactly when both conjuncts are.

theorem SignType.condAssert_meetBelnap {d : Trivalent.Designation} {a b c : SignType} : condAssert d a (b.meetBelnap c) = (condAssert d a b).meetBelnap (condAssert d a c)

Conditional assertion distributes over Belnap conjunction.

theorem SignType.condAssert_joinBelnap {d : Trivalent.Designation} {a b c : SignType} : condAssert d a (b.joinBelnap c) = (condAssert d a b).joinBelnap (condAssert d a c)

Conditional assertion distributes over Belnap disjunction.

Supervaluation

The value of a predicate over a finite family of classical valuations ([vF66]). The empty family is vacuously both all-true and all-false, and supervaluation resolves it to 1.

def SignType.supervaluation {α : Type u_1} (s : Finset α) (P : α → Prop) [DecidablePred P] : SignType

The supervaluation of P over the family s is 1 when P holds at every member, -1 when it fails at every member of a nonempty s, and 0 otherwise.

Equations

• SignType.supervaluation s P = if ∀ a ∈ s, P a then 1 else if ∃ a ∈ s, P a then 0 else -1

theorem SignType.supervaluation_eq_one_iff {α : Type u_1} (s : Finset α) (P : α → Prop) [DecidablePred P] : supervaluation s P = 1 ↔ ∀ a ∈ s, P a

theorem SignType.supervaluation_eq_neg_one_iff {α : Type u_1} (s : Finset α) (P : α → Prop) [DecidablePred P] : supervaluation s P = -1 ↔ s.Nonempty ∧ ∀ a ∈ s, ¬P a

theorem SignType.supervaluation_eq_zero_iff {α : Type u_1} (s : Finset α) (P : α → Prop) [DecidablePred P] : supervaluation s P = 0 ↔ (∃ a ∈ s, P a) ∧ ∃ a ∈ s, ¬P a

@[simp]

theorem SignType.supervaluation_empty {α : Type u_1} (P : α → Prop) [DecidablePred P] : supervaluation ∅ P = 1

@[simp]

theorem SignType.supervaluation_singleton {α : Type u_1} (P : α → Prop) [DecidablePred P] (a : α) : supervaluation {a} P = ofProp (P a)

Over a single valuation the supervaluation is classical truth.

theorem SignType.supervaluation_congr {α : Type u_1} {s : Finset α} {P : α → Prop} [DecidablePred P] {Q : α → Prop} [DecidablePred Q] (h : ∀ a ∈ s, P a ↔ Q a) : supervaluation s P = supervaluation s Q

The supervaluation depends only on the predicate's values on the family.

theorem SignType.supervaluation_image {α : Type u_1} (s : Finset α) {β : Type u_2} [DecidableEq β] (f : α → β) (Q : β → Prop) [DecidablePred Q] : supervaluation (Finset.image f s) Q = supervaluation s (Q ∘ f)

Supervaluating over the image of a family is supervaluating the composite over the family.

theorem SignType.supervaluation_const {α : Type u_1} {s : Finset α} (hs : s.Nonempty) (q : Prop) [Decidable q] : (supervaluation s fun (x : α) => q) = ofProp q

Over a nonempty family a constant predicate supervaluates to its classical value.

theorem SignType.supervaluation_not {α : Type u_1} {s : Finset α} (P : α → Prop) [DecidablePred P] (hs : s.Nonempty) : (supervaluation s fun (x : α) => ¬P x) = -supervaluation s P

Over a nonempty family, negating the predicate negates the supervaluation, swapping truth and falsity and fixing the gap.

Truth-table interpretations

The trivalent logics of the literature share Kleene's negation and differ in the truth tables of their binary connectives, which Connectives collects. With a designation standard they make a logical matrix.

structure Trivalent.Connectives : Type

An interpretation of the binary connectives by trivalent truth tables; negation is always Kleene's.

• conj : SignType → SignType → SignType

  The conjunction.

• disj : SignType → SignType → SignType

  The disjunction.

• cond : SignType → SignType → SignType

  The conditional.

def Trivalent.Connectives.strongKleene : Connectives

The strong tables of [Kle52], with the material conditional ¬a ∨ b.

Equations

• Trivalent.Connectives.strongKleene = { conj := fun (x1 x2 : SignType) => min x1 x2, disj := fun (x1 x2 : SignType) => max x1 x2, cond := fun (a b : SignType) => max (-a) b }

@[simp]

theorem Trivalent.Connectives.strongKleene_disj (x1✝ x2✝ : SignType) : strongKleene.disj x1✝ x2✝ = max x1✝ x2✝

@[simp]

theorem Trivalent.Connectives.strongKleene_cond (a b : SignType) : strongKleene.cond a b = max (-a) b

@[simp]

theorem Trivalent.Connectives.strongKleene_conj (x1✝ x2✝ : SignType) : strongKleene.conj x1✝ x2✝ = min x1✝ x2✝

def Trivalent.Connectives.weakKleene : Connectives

The weak tables of [Kle52], the internal logic of [Boc38].

Equations

• Trivalent.Connectives.weakKleene = { conj := SignType.meetWeak, disj := SignType.joinWeak, cond := fun (a b : SignType) => (-a).joinWeak b }

@[simp]

theorem Trivalent.Connectives.weakKleene_disj (a✝ a✝¹ : SignType) : weakKleene.disj a✝ a✝¹ = a✝.joinWeak a✝¹

@[simp]

theorem Trivalent.Connectives.weakKleene_cond (a b : SignType) : weakKleene.cond a b = (-a).joinWeak b

@[simp]

theorem Trivalent.Connectives.weakKleene_conj (a✝ a✝¹ : SignType) : weakKleene.conj a✝ a✝¹ = a✝.meetWeak a✝¹

def Trivalent.Connectives.middleKleene : Connectives

The Middle Kleene tables of [Pet79], which read their operands from left to right.

Equations

• Trivalent.Connectives.middleKleene = { conj := SignType.meetMiddle, disj := SignType.joinMiddle, cond := fun (a b : SignType) => (-a).joinMiddle b }

@[simp]

theorem Trivalent.Connectives.middleKleene_conj (a✝ a✝¹ : SignType) : middleKleene.conj a✝ a✝¹ = a✝.meetMiddle a✝¹

@[simp]

theorem Trivalent.Connectives.middleKleene_cond (a b : SignType) : middleKleene.cond a b = (-a).joinMiddle b

@[simp]

theorem Trivalent.Connectives.middleKleene_disj (a✝ a✝¹ : SignType) : middleKleene.disj a✝ a✝¹ = a✝.joinMiddle a✝¹

def Trivalent.Connectives.cooper : Connectives

The tables of [Coo68] take Belnap's conjunction and disjunction, which skip a void operand, and the conditional that asserts its consequent on a non-false antecedent.

Equations

• Trivalent.Connectives.cooper = { conj := SignType.meetBelnap, disj := SignType.joinBelnap, cond := SignType.condAssert Trivalent.Designation.lp }

@[simp]

theorem Trivalent.Connectives.cooper_disj (a✝ a✝¹ : SignType) : cooper.disj a✝ a✝¹ = a✝.joinBelnap a✝¹

@[simp]

theorem Trivalent.Connectives.cooper_conj (a✝ a✝¹ : SignType) : cooper.conj a✝ a✝¹ = a✝.meetBelnap a✝¹

@[simp]

theorem Trivalent.Connectives.cooper_cond (a b : SignType) : cooper.cond a b = SignType.condAssert Designation.lp a b

def Trivalent.Connectives.deFinetti : Connectives

The conditional of [dF36], which asserts its consequent on a true antecedent, with the strong Kleene conjunction and disjunction.

Equations

• Trivalent.Connectives.deFinetti = { conj := fun (x1 x2 : SignType) => min x1 x2, disj := fun (x1 x2 : SignType) => max x1 x2, cond := SignType.condAssert Trivalent.Designation.k3 }

@[simp]

theorem Trivalent.Connectives.deFinetti_disj (x1✝ x2✝ : SignType) : deFinetti.disj x1✝ x2✝ = max x1✝ x2✝

@[simp]

theorem Trivalent.Connectives.deFinetti_conj (x1✝ x2✝ : SignType) : deFinetti.conj x1✝ x2✝ = min x1✝ x2✝

@[simp]

theorem Trivalent.Connectives.deFinetti_cond (a b : SignType) : deFinetti.cond a b = SignType.condAssert Designation.k3 a b