feat(Foundations/Logic/Belnap): add BelnapLevel and gates with four-valued logic

[matthunz]

Adds BelnapLevel and primitive gates with four-valued logic which can be used to model information that may be inconsistent or incomplete:

def BelnapLevel := WithBotTop Bool

/-- Logical AND. -/
def and : BelnapLevel → BelnapLevel → BelnapLevel

/-- Logical OR. -/
def or : BelnapLevel → BelnapLevel → BelnapLevel

/-- Logical NOT. -/
def not : BelnapLevel → BelnapLevel

I'm currently using this in circuitlib to model digital circuits, where ⊥ represents a disconnection and ⊤ represents a short, but I've also seen this four-valued logic used to model things like values in a database and threading in programming languages.

A big part of this PR is the instance for Lattice which I'm not super confident in - a custom Preorder that doesn't define true > false is required to prove the gates are Monotone, which helps for modeling things like real-world circuit gates that can't physically gain information. I like the general Monotone proofs so I'm leaning towards it being useful but it might be better without it if the custom Preorder isn't expected by users.

[thomaskwaring]

Hi!

I haven't spent enough time trying to make it work out, but I suspect we can find a way to avoid defining that Lattice instance by hand. Using WithBotTop means that we'll potentially be able to use typeclass inference, but to do that I would define a fresh two-element inductive type, say TruthVal, so you don't class with the existing order instance on Bool. Then you get lots of stuff for free:

import Mathlib.Order.WithBotTop

/-- Truth values (synonym for `Bool`) -/
inductive TruthVal where
  | tt | ff

/-- Give `TruthVal` the discrete order -/
instance : LE TruthVal where
  le := (· = ·)

abbrev BelnapLevel := WithBotTop TruthVal

instance : OrderTop BelnapLevel := inferInstance -- eg this works

You still have to cook up the lattice operations, but it might be a bit easier this way.

A completely different approach would be to notice the lattice you've defined is exactly the powerset lattice of a two-element set. So you could define BelnapLevel := Set (Fin 2), get the Lattice etc instances from that, then define BelnapLevel.true := {0} and so forth to hide the implementation details.

EDIT: I think the latter is the right way — I'm not familiar with Belnap's work, but judging from the wikipedia article viewing BelnapLevel := Set Bool (so that the four values are "true", "false", "both" and "neither") is actually pretty close to his original presentation, and has the potential to match with Scott-style semantics of datatypes down the track.