Minimal Sheffer stroke axioms for Boolean algebra

The Sheffer stroke a | b is (a ⊓ b)ᶜ, i.e. the NAND gate on Bool. All functions with Bool inputs and outputs can be expressed using only this operator.

This file shows that for non-empty magmas whose operator is the Sheffer stroke, satisfying either of two axiom sets is equivalent to being a Boolean algebra. The first set, with two axioms, was proven equivalent by Robert Veroff:

1. | is commutative
2. ∀ a b c, a | b | (a | (b | c)) = a

Instead of deriving Sheffer's 1913 axioms as done in the original paper, we derive a BooleanAlgebra instance directly: aᶜ := a | a, a ≤ b := aᶜ = a | b, a ⊔ b := aᶜ | bᶜ, a ⊓ b = (a | b)ᶜ, ⊤ = a | aᶜ and ⊥ = ⊤ᶜ.

The second set consists of just the single axiom ∀ a b c, a | (b | a | a) | (b | (c | a)) = b. Its equivalence was conjectured by Stephen Wolfram and proved by William McCune et al. shortly after Veroff's result. We reduce to Veroff's axioms rather than Sheffer's 1913 axioms, following the original paper's Otter derivation of commutativity closely (with certain steps condensed), after which the other axiom becomes very easy to derive.

Both axiom sets are minimal in the sense that for any set using fewer total Sheffer strokes, non-Boolean algebra models exist.

class VeroffAlgebra (α : Type u_1) extends Inhabited α : Type u_1

Veroff's two axioms for Boolean algebra.

• default : α
• f : α → α → α

  The Sheffer stroke function

• comm (a b : α) : f a b = f b a

  The Sheffer stroke is commutative

• veroff (a b c : α) : f (f a b) (f a (f b c)) = a

  Veroff's axiom

def VeroffAlgebra.«term_|_» : Lean.TrailingParserDescr

The Sheffer stroke function

Equations

• VeroffAlgebra.«term_|_» = Lean.ParserDescr.trailingNode `VeroffAlgebra.«term_|_» 70 70 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " | ") (Lean.ParserDescr.cat `term 71))

def BooleanAlgebra.veroffAlgebra {α : Type u_1} [BooleanAlgebra α] : VeroffAlgebra α

Derive a Veroff algebra from a Boolean algebra.

Equations

• BooleanAlgebra.veroffAlgebra = { default := ⊥, f := fun (a b : α) => (a ⊓ b)ᶜ, comm := ⋯, veroff := ⋯ }

@[implicit_reducible]

instance VeroffAlgebra.instCompl {α : Type u_1} [VeroffAlgebra α] : Compl α

Equations

• VeroffAlgebra.instCompl = { compl := fun (a : α) => VeroffAlgebra.f a a }

theorem VeroffAlgebra.compl_def {α : Type u_1} [VeroffAlgebra α] (a : α) : aᶜ = f a a

theorem VeroffAlgebra.meredith {α : Type u_1} [VeroffAlgebra α] (a b : α) : f (f a b) aᶜ = a

theorem VeroffAlgebra.compl_compl {α : Type u_1} [VeroffAlgebra α] (a : α) : aᶜᶜ = a

theorem VeroffAlgebra.ababc {α : Type u_1} [VeroffAlgebra α] (a b c : α) : f a (f b (f a (f b c))) = f a (f b c)

theorem VeroffAlgebra.abba {α : Type u_1} [VeroffAlgebra α] (a b : α) : f (f (f a b) b) a = aᶜ

theorem VeroffAlgebra.aba_abb {α : Type u_1} [VeroffAlgebra α] (a b : α) : f a (f b a) = f a bᶜ

theorem VeroffAlgebra.sheffer {α : Type u_1} [VeroffAlgebra α] (a b : α) : f a (f b bᶜ) = aᶜ

@[implicit_reducible]

instance VeroffAlgebra.instPartialOrder {α : Type u_1} [VeroffAlgebra α] : PartialOrder α

Equations

• VeroffAlgebra.instPartialOrder = { le := fun (a b : α) => aᶜ = VeroffAlgebra.f a b, le_refl := ⋯, le_trans := ⋯, lt_iff_le_not_ge := ⋯, le_antisymm := ⋯ }

theorem VeroffAlgebra.le_def {α : Type u_1} [VeroffAlgebra α] (a b : α) : a ≤ b ↔ aᶜ = f a b

theorem VeroffAlgebra.le_sup_left {α : Type u_1} [VeroffAlgebra α] (a b : α) : a ≤ f aᶜ bᶜ

theorem VeroffAlgebra.inf_le_left {α : Type u_1} [VeroffAlgebra α] (a b : α) : (f a b)ᶜ ≤ a

theorem VeroffAlgebra.sup_le {α : Type u_1} [VeroffAlgebra α] (a b c : α) (h₁ : a ≤ c) (h₂ : b ≤ c) : f aᶜ bᶜ ≤ c

theorem VeroffAlgebra.compl_le_compl {α : Type u_1} [VeroffAlgebra α] (a b : α) (h : a ≤ b) : bᶜ ≤ aᶜ

theorem VeroffAlgebra.compl_le_compl_iff_le {α : Type u_1} [VeroffAlgebra α] (a b : α) : aᶜ ≤ bᶜ ↔ b ≤ a

@[implicit_reducible]

instance VeroffAlgebra.instLattice {α : Type u_1} [VeroffAlgebra α] : Lattice α

Equations

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

theorem VeroffAlgebra.sup_def {α : Type u_1} [VeroffAlgebra α] (a b : α) : a ⊔ b = f aᶜ bᶜ

theorem VeroffAlgebra.inf_def {α : Type u_1} [VeroffAlgebra α] (a b : α) : a ⊓ b = (f a b)ᶜ

def VeroffAlgebra.top {α : Type u_1} [VeroffAlgebra α] : α

The top element, equal to a | aᶜ for any a.

Equations

• VeroffAlgebra.top = VeroffAlgebra.f default defaultᶜ

theorem VeroffAlgebra.f_compl_const {α : Type u_1} [VeroffAlgebra α] (a b : α) : f a aᶜ = f b bᶜ

theorem VeroffAlgebra.sup_compl_eq_top {α : Type u_1} [VeroffAlgebra α] (a : α) : a ⊔ aᶜ = top

theorem VeroffAlgebra.compl_inf {α : Type u_1} [VeroffAlgebra α] (a b : α) : (a ⊓ b)ᶜ = aᶜ ⊔ bᶜ

theorem VeroffAlgebra.le_iff_compl_sup {α : Type u_1} [VeroffAlgebra α] (a b : α) : a ≤ b ↔ aᶜ ⊔ b = top

@[implicit_reducible]

instance VeroffAlgebra.instBooleanAlgebra {α : Type u_1} [VeroffAlgebra α] : BooleanAlgebra α

Derive a Boolean algebra from a Veroff algebra.

Equations

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

class SingleShefferAlgebra (α : Type u_2) extends Inhabited α : Type u_2

The single-axiom algebra shown to be equivalent to Boolean algebra by McCune et al.

• default : α
• f : α → α → α

  The Sheffer stroke function

• rule (a b c : α) : f (f a (f (f b a) a)) (f b (f c a)) = b

  The single axiom of this algebra

def SingleShefferAlgebra.«term_|_» : Lean.TrailingParserDescr

The Sheffer stroke function

Equations

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

def BooleanAlgebra.singleShefferAlgebra {α : Type u_2} [BooleanAlgebra α] : SingleShefferAlgebra α

Derive a SingleShefferAlgebra from a Boolean algebra.

Equations

• BooleanAlgebra.singleShefferAlgebra = { default := ⊥, f := fun (a b : α) => (a ⊓ b)ᶜ, rule := ⋯ }

theorem SingleShefferAlgebra.eq74 {α : Type u_2} [SingleShefferAlgebra α] (a : α) : f a (f (f a a) a) = f a a

theorem SingleShefferAlgebra.eq75 {α : Type u_2} [SingleShefferAlgebra α] (a : α) : f (f a (f (f a a) a)) (f a a) = a

theorem SingleShefferAlgebra.eq76 {α : Type u_2} [SingleShefferAlgebra α] (a b : α) : f (f a a) (f a (f b a)) = a

theorem SingleShefferAlgebra.eq77 {α : Type u_2} [SingleShefferAlgebra α] (a b : α) : f (f a (f (f (f b b) a) a)) b = f b b

theorem SingleShefferAlgebra.eq79 {α : Type u_2} [SingleShefferAlgebra α] (a b : α) : f a (f (f (f (f b a) (f b a)) a) a) = f b a

theorem SingleShefferAlgebra.eq80 {α : Type u_2} [SingleShefferAlgebra α] (a b : α) : f (f a a) (f b a) = a

theorem SingleShefferAlgebra.eq84 {α : Type u_2} [SingleShefferAlgebra α] (a b : α) : f (f (f a b) (f a b)) b = f a b

theorem SingleShefferAlgebra.eq85 {α : Type u_2} [SingleShefferAlgebra α] (a b : α) : f a (f (f b a) a) = f b a

theorem SingleShefferAlgebra.eq89 {α : Type u_2} [SingleShefferAlgebra α] (a b c : α) : f a (f (f a b) (f c b)) = f a b

theorem SingleShefferAlgebra.eq91 {α : Type u_2} [SingleShefferAlgebra α] (a b : α) : f a (f (f b a) a) = f a b

theorem SingleShefferAlgebra.comm {α : Type u_2} [SingleShefferAlgebra α] (a b : α) : f a b = f b a

@[implicit_reducible]

instance SingleShefferAlgebra.instVeroffAlgebra {α : Type u_2} [SingleShefferAlgebra α] : VeroffAlgebra α

Derive a Veroff (and hence Boolean) algebra from a SingleShefferAlgebra.

Equations

• SingleShefferAlgebra.instVeroffAlgebra = { toInhabited := inst✝.toInhabited, f := SingleShefferAlgebra.f, comm := ⋯, veroff := ⋯ }