Belnap levels

References

• [N. D. Belnap, A Useful Four-Valued Logic][Belnap1977]
• [Ghica, Kaye, and Sprunger, A Complete Theory of Sequential Digital Circuits][Ghica2025]

def Circuit.BelnapLevel : Type

The Belnap four-valued logic lattice on Bool, with a bottom (no information) and a top (conflicting information) adjoined.

Equations

• Circuit.BelnapLevel = WithBotTop Bool

@[instance_reducible]

instance Circuit.BelnapLevel.instCoeWithBotTopBool : Coe (WithBotTop Bool) BelnapLevel

Equations

• Circuit.BelnapLevel.instCoeWithBotTopBool = { coe := fun (l : WithBotTop Bool) => l }

@[instance_reducible]

instance Circuit.BelnapLevel.instBot : Bot BelnapLevel

Equations

• Circuit.BelnapLevel.instBot = { bot := none }

@[instance_reducible]

instance Circuit.BelnapLevel.instTop : Top BelnapLevel

Equations

• Circuit.BelnapLevel.instTop = { top := ↑none }

@[inline]

def Circuit.BelnapLevel.le : BelnapLevel → BelnapLevel → Prop

The information ordering on Belnap levels: ⊥ is below everything, everything is below ⊤, and the two classical values are only related to themselves.

Equations

• Circuit.BelnapLevel.le none x✝ = (true = true)
• x✝.le (some none) = (true = true)
• Circuit.BelnapLevel.le (some (some x_2)) (some (some y)) = ((x_2 == y) = true)
• x✝¹.le x✝ = (false = true)

theorem Circuit.BelnapLevel.le_refl (a : BelnapLevel) : a.le a

theorem Circuit.BelnapLevel.le_trans (a b c : BelnapLevel) : a.le b → b.le c → a.le c

@[instance_reducible]

instance Circuit.BelnapLevel.instPreorder : Preorder BelnapLevel

Equations

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

theorem Circuit.BelnapLevel.le_antisymm (a b : BelnapLevel) : a ≤ b → b ≤ a → a = b

def Circuit.BelnapLevel.sup : BelnapLevel → BelnapLevel → BelnapLevel

The join (least upper bound) on Belnap levels in the information order.

theorem Circuit.BelnapLevel.le_sup_left (a b : BelnapLevel) : a ≤ a.sup b

theorem Circuit.BelnapLevel.le_sup_right (a b : BelnapLevel) : b ≤ a.sup b

theorem Circuit.BelnapLevel.sup_le (a b c : BelnapLevel) : a ≤ c → b ≤ c → a.sup b ≤ c

@[instance_reducible]

instance Circuit.BelnapLevel.instSemilatticeSup : SemilatticeSup BelnapLevel

Equations

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

@[inline]

def Circuit.BelnapLevel.and (a b : BelnapLevel) : BelnapLevel

Logical AND.

@[inline]

def Circuit.BelnapLevel.or (a b : BelnapLevel) : BelnapLevel

Logical OR.

@[inline]

def Circuit.BelnapLevel.not : BelnapLevel → BelnapLevel

Logical NOT.