The Robbins conjecture

Herbert Robbins asked in 1933 whether the following three axioms, with ⊔ and ᶜ as in BooleanAlgebra, yield an algebra equivalent to Boolean algebra:

• ⊔ is commutative and associative
• For all a and b, ((a ⊔ b)ᶜ ⊔ (a ⊔ bᶜ)ᶜ)ᶜ = a

This conjecture was only proved in 1997 by an early automated theorem prover under the direction of William McCune by deriving Huntington's equation:

• For all a and b, (aᶜ ⊔ bᶜ)ᶜ ⊔ (aᶜ ⊔ b)ᶜ = a

With the axioms on ⊔ this had been shown by Edward Huntington to be equivalent to Boolean algebra, just before Robbins made his conjecture.

The formalisation in this file largely follows Matthew Wampler-Doty's Isabelle formalisation, which in turn follows Allen L. Mann's A Complete Proof of the Robbins Conjecture. Some differences include:

• For ease of typing and clarity around negations, algebraic notation is used for Robbins algebras: - + 0 1 instead of ᶜ ⊔ ⊥ ⊤.
• After deriving Huntington's equation we derive the BooleanAlgebra instance directly. Wampler-Doty went through an axiomatisation with 9 axioms found in a textbook.
• To make the manipulations in Mann's presentation explicit, we do not automate proofs with grind, only ac_rfl for rearranging terms and lia for numeric comparisons. Wampler-Doty relies heavily on metis, a rough Isabelle equivalent of grind.

class RobbinsAlgebra (α : Type u_1) extends Inhabited α, AddCommSemigroup α, Neg α : Type u_1

The type of Robbins algebras.

• default : α
• add : α → α → α
• add_assoc (a b c : α) : a + b + c = a + (b + c)
• add_comm (a b : α) : a + b = b + a
• neg : α → α
• robbins (a b : α) : -(-(a + b) + -(a + -b)) = a

  Robbins's axiom

@[instance_reducible]

def BooleanAlgebra.robbinsAlgebra {α : Type u_1} [BooleanAlgebra α] : RobbinsAlgebra α

Derive a Robbins algebra from a Boolean algebra.

Equations

• BooleanAlgebra.robbinsAlgebra = { default := ⊥, add := fun (x1 x2 : α) => x1 ⊔ x2, add_assoc := ⋯, add_comm := ⋯, neg := fun (x : α) => xᶜ, robbins := ⋯ }

def RobbinsAlgebra.smul {α : Type u_1} [RobbinsAlgebra α] : ℕ → α → α

Sum a number of copies of an element. Not intended to be used for 0 copies (although the ultimately correct value of -(a + -a) is included for completeness).

Equations

• RobbinsAlgebra.smul 0 x✝ = -(x✝ + -x✝)
• RobbinsAlgebra.smul 1 x✝ = x✝
• RobbinsAlgebra.smul k.succ.succ x✝ = RobbinsAlgebra.smul (k + 1) x✝ + x✝

@[instance_reducible]

instance RobbinsAlgebra.instSMulNat {α : Type u_1} [RobbinsAlgebra α] : SMul ℕ α

Equations

• RobbinsAlgebra.instSMulNat = { smul := RobbinsAlgebra.smul }

theorem RobbinsAlgebra.smul_succ {α : Type u_1} [RobbinsAlgebra α] {k : ℕ} {a : α} (hk : 1 ≤ k) : (k + 1) • a = k • a + a

theorem RobbinsAlgebra.mann_44 {α : Type u_1} [RobbinsAlgebra α] (a b : α) : -(-(-(a + b) + -a + b) + b) = -(a + b)

theorem RobbinsAlgebra.mann_45 {α : Type u_1} [RobbinsAlgebra α] (a b : α) : -(-(-(-a + b) + a + b) + b) = -(-a + b)

theorem RobbinsAlgebra.mann_46 {α : Type u_1} [RobbinsAlgebra α] (a b : α) : -(-(-(-a + b) + a + b + b) + -(-a + b)) = b

theorem RobbinsAlgebra.mann_47 {α : Type u_1} [RobbinsAlgebra α] (a b c : α) : -(-(-(-(-a + b) + a + b + b) + -(-a + b) + c) + -(b + c)) = c

theorem RobbinsAlgebra.mann_48 {α : Type u_1} [RobbinsAlgebra α] (a b c : α) : -(-(-(-(-a + b) + a + b + b) + -(-a + b) + -(b + c) + c) + c) = -(b + c)

theorem RobbinsAlgebra.mann_49 {α : Type u_1} [RobbinsAlgebra α] (a b c d : α) : -(-(-(-(-(-a + b) + a + b + b) + -(-a + b) + -(b + c) + c) + c + d) + -(-(b + c) + d)) = d

def RobbinsAlgebra.q {α : Type u_1} [RobbinsAlgebra α] (a : α) : α

A common subexpression occurring in mann_50 to winker.

Equations

• RobbinsAlgebra.q a = -(-(3 • a) + a)

theorem RobbinsAlgebra.mann_50 {α : Type u_1} [RobbinsAlgebra α] (a : α) : -(-(q a + -(3 • a)) + -(q a + 5 • a)) = q a

theorem RobbinsAlgebra.mann_51 {α : Type u_1} [RobbinsAlgebra α] (a : α) : -(q a + 5 • a) = -(3 • a)

theorem RobbinsAlgebra.mann_52 {α : Type u_1} [RobbinsAlgebra α] (a : α) : -(-(q a + -(3 • a) + 2 • a) + -(3 • a)) = q a + 2 • a

theorem RobbinsAlgebra.mann_53 {α : Type u_1} [RobbinsAlgebra α] (a : α) : -(q a + -(3 • a)) = a

theorem RobbinsAlgebra.mann_54 {α : Type u_1} [RobbinsAlgebra α] (a b : α) : -(-(q a + -(3 • a) + b) + -(a + b)) = b

theorem RobbinsAlgebra.winker {α : Type u_1} [RobbinsAlgebra α] : ∃ (x : α), ∃ (y : α), x + y = y

Winker's first condition, proved in 1997 by the automated theorem prover EQP to be derivable in Robbins algebras.

theorem RobbinsAlgebra.mann_33 {α : Type u_1} [RobbinsAlgebra α] {a b c : α} (h : -(a + -(b + c)) = -(a + b + -c)) : a + b = a

theorem RobbinsAlgebra.mann_34 {α : Type u_1} [RobbinsAlgebra α] {a b c : α} (h : -(a + -(b + c)) = -(b + -(a + c))) : a = b

theorem RobbinsAlgebra.mann_35 {α : Type u_1} [RobbinsAlgebra α] {a b c : α} (h : -(a + -b) = c) : -(-(a + b) + c) = a

theorem RobbinsAlgebra.mann_36 {α : Type u_1} [RobbinsAlgebra α] {a b c : α} {k : ℕ} (hk : 1 ≤ k) (h : -(a + -b) = c) : -(a + -(b + k • (a + c))) = c

theorem RobbinsAlgebra.mann_37 {α : Type u_1} [RobbinsAlgebra α] {a b : α} {k : ℕ} (hk : 1 ≤ k) (h : -(-(a + -b) + -b) = a) : -(b + k • (a + -(a + -b))) = -b

theorem RobbinsAlgebra.mann_38 {α : Type u_1} [RobbinsAlgebra α] {a b : α} {k : ℕ} (hk : 1 ≤ k) (h : -(a + b) = -b) : -(b + k • (a + -(a + -b))) = -b

theorem RobbinsAlgebra.mann_39 {α : Type u_1} [RobbinsAlgebra α] {a b : α} (h₂ : -(2 • a + b) = -b) (h₃ : -(3 • a + b) = -b) : 2 • a + b = 3 • a + b

theorem RobbinsAlgebra.mann_40 {α : Type u_1} [RobbinsAlgebra α] {a b : α} (h : -(a + b) = -b ∨ -(-(a + -b) + -b) = a) : b + 2 • (a + -(a + -b)) = b + 3 • (a + -(a + -b))

theorem RobbinsAlgebra.exists_idempotent {α : Type u_1} [RobbinsAlgebra α] : ∃ (x : α), x + x = x

theorem RobbinsAlgebra.exists_zero {α : Type u_1} [RobbinsAlgebra α] : ∃ (z : α), ∀ (a : α), a + z = a

theorem RobbinsAlgebra.neg_neg {α : Type u_1} [RobbinsAlgebra α] (a : α) : - -a = a

theorem RobbinsAlgebra.huntington {α : Type u_1} [RobbinsAlgebra α] (a b : α) : -(-a + -b) + -(-a + b) = a

@[instance_reducible]

instance RobbinsAlgebra.instZero {α : Type u_1} [RobbinsAlgebra α] : Zero α

Equations

• RobbinsAlgebra.instZero = { zero := -(default + -default) }

@[instance_reducible]

instance RobbinsAlgebra.instOne {α : Type u_1} [RobbinsAlgebra α] : One α

Equations

• RobbinsAlgebra.instOne = { one := default + -default }

theorem RobbinsAlgebra.add_neg_self_const {α : Type u_1} [RobbinsAlgebra α] (a b : α) : a + -a = b + -b

theorem RobbinsAlgebra.neg_zero {α : Type u_1} [RobbinsAlgebra α] : -0 = 1

theorem RobbinsAlgebra.neg_one {α : Type u_1} [RobbinsAlgebra α] : -1 = 0

theorem RobbinsAlgebra.add_neg_self {α : Type u_1} [RobbinsAlgebra α] (a : α) : a + -a = 1

theorem RobbinsAlgebra.add_zero {α : Type u_1} [RobbinsAlgebra α] (a : α) : a + 0 = a

theorem RobbinsAlgebra.add_self {α : Type u_1} [RobbinsAlgebra α] (a : α) : a + a = a

theorem RobbinsAlgebra.min_add_left {α : Type u_1} [RobbinsAlgebra α] (a b : α) : -(-a + -b) + a = a

theorem RobbinsAlgebra.min_add_distrib {α : Type u_1} [RobbinsAlgebra α] (a b c : α) : -(-a + -(b + c)) = -(-a + -b) + -(-a + -c)

theorem RobbinsAlgebra.add_min_distrib {α : Type u_1} [RobbinsAlgebra α] (a b c : α) : a + -(-b + -c) = -(-(a + b) + -(a + c))

@[instance_reducible]

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

Equations

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

@[instance_reducible]

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

Derive a Boolean algebra from a Robbins algebra.

Equations

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