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

@[implicit_reducible]

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

Equations

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

@[implicit_reducible]

instance Circuit.BelnapLevel.instBot : Bot BelnapLevel

Equations

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

@[implicit_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

@[implicit_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.

Equations

• Circuit.BelnapLevel.sup none x✝ = x✝
• x✝.sup none = x✝
• Circuit.BelnapLevel.sup (some none) x✝ = ↑none
• x✝.sup (some none) = ↑none
• Circuit.BelnapLevel.sup (some (some x_2)) (some (some y)) = if (x_2 == y) = true then ↑↑x_2 else ↑none

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

@[implicit_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.

Equations

• Circuit.BelnapLevel.and (some (some false)) b = WithBotTop.coe false
• a.and (some (some false)) = WithBotTop.coe false
• Circuit.BelnapLevel.and (some (some true)) b = b
• a.and (some (some true)) = a
• Circuit.BelnapLevel.and none none = ⊥
• Circuit.BelnapLevel.and (some none) (some none) = ⊤
• a.and b = WithBotTop.coe false

@[inline]

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

Logical OR.

Equations

• Circuit.BelnapLevel.or (some (some true)) b = WithBotTop.coe true
• a.or (some (some true)) = WithBotTop.coe true
• Circuit.BelnapLevel.or (some (some false)) b = b
• a.or (some (some false)) = a
• Circuit.BelnapLevel.or none none = ⊥
• Circuit.BelnapLevel.or (some none) (some none) = ⊤
• a.or b = WithBotTop.coe true

@[inline]

def Circuit.BelnapLevel.not : BelnapLevel → BelnapLevel

Logical NOT.

Equations

• Circuit.BelnapLevel.not (some (some b)) = WithBotTop.coe !b
• x✝.not = x✝