Minimal axioms for Boolean algebra

{{Short description|Mathematical assumptions}}

In mathematical logic, minimal axioms for Boolean algebra are assumptions which are equivalent to the axioms of Boolean algebra (or propositional calculus), chosen to be as short as possible. For example, an axiom with six NAND operations and three variables is equivalent to Boolean algebra:{{cite journal |last1=Wolfram |first1=Stephen |title=Logic, Explainability and the Future of Understanding |url=https://writings.stephenwolfram.com/2018/11/logic-explainability-and-the-future-of-understanding/ |website=Stephen Worfram Writings|date=6 November 2018 }}

: $((a\backslash mid\; b)\backslash mid\; c)\; \backslash mid\; (a\backslash mid((a\backslash mid\; c)\backslash mid\; a))\; =\; c$

where the vertical bar represents the NAND logical operation (also known as the Sheffer stroke).

It is one of 25 candidate axioms for this property identified by Stephen Wolfram, by enumerating the Sheffer identities of length less or equal to 15 elements (excluding mirror images) that have no noncommutative models with four or fewer variables, and was first proven equivalent by William McCune, Branden Fitelson, and Larry Wos.{{cite book |last1=Wolfram |first1=Stephen |author-link=Stephen Wolfram |title=A New Kind of Science |date=2002 |publisher=Wolfram Media |isbn=978-1579550080 }}{{citation

| last1 = McCune | first1 = William |author-link1 = William McCune

| last2 = Veroff | first2 = Robert

| last3 = Fitelson | first3 = Branden |author-link3 = Branden Fitelson

| last4 = Harris | first4 = Kenneth

| last5 = Feist | first5 = Andrew

| last6 = Wos | first6 = Larry |author-link6 = Larry Wos

| doi = 10.1023/A:1020542009983

| issue = 1

| journal = Journal of Automated Reasoning

| mr = 1940227

| pages = 1–16

| title = Short single axioms for Boolean algebra

| volume = 29

| year = 2002| s2cid = 207582048 }} MathWorld, a site associated with Wolfram, has named the axiom the "Wolfram axiom".{{MathWorld|id=WolframAxiom|title=Wolfram Axiom|author=Rowland, Todd|author2=Weisstein, Eric W.}} McCune et al. also found a longer single axiom for Boolean algebra based on disjunction and negation.

In 1933, Edward Vermilye Huntington identified the axiom

:$\{\backslash neg(\{\backslash neg\; x\}\; \backslash lor\; \{y\})\}\; \backslash lor\; \{\backslash neg(\{\backslash neg\; x\}\; \backslash lor\; \{\backslash neg\; y\})\}\; =\; x$

as being equivalent to Boolean algebra, when combined with the commutativity of the OR operation, $x\; \backslash lor\; y\; =\; y\; \backslash lor\; x$, and the assumption of associativity, $(x\; \backslash lor\; y)\; \backslash lor\; z\; =\; x\; \backslash lor\; (y\; \backslash lor\; z)$.{{cite journal|last=Huntington |first=E. V. |title=New Sets of Independent Postulates for the Algebra of Logic, with Special Reference to Whitehead and Russell's Principia Mathematica |journal=Trans. Amer. Math. Soc. |volume=25 |pages=247–304 |year=1933}} Herbert Robbins conjectured that Huntington's axiom could be replaced by

:$\backslash neg(\backslash neg(x\; \backslash lor\; y)\; \backslash lor\; \backslash neg(x\; \backslash lor\; \{\backslash neg\; y\}))\; =\; x,$

which requires one fewer use of the logical negation operator $\backslash neg$. Neither Robbins nor Huntington could prove this conjecture; nor could Alfred Tarski, who took considerable interest in it later. The conjecture was eventually proved in 1996 with the aid of theorem-proving software.{{cite book |last1=Henkin |first1=Leon |author-link1=Leon Henkin |last2=Monk |first2=J. Donald |last3=Tarski |first3=Alfred |author-link3=Alfred Tarski |title=Cylindric Algebras, Part I |publisher=North-Holland |isbn=978-0-7204-2043-2 |year=1971 |oclc=1024041028 |url-access=registration |url=https://archive.org/details/cylindricalgebra0000henk }}{{cite journal|last=McCune |first=William |title=Solution of the Robbins Problem |journal=Journal of Automated Reasoning |volume=19 |year=1997 |issue=3 |pages=263–276 |doi=10.1023/A:1005843212881|s2cid=30847540 }}{{cite news|last=Kolata |first=Gina |author-link=Gina Kolata |title=Computer Math Proof Shows Reasoning Power |work=The New York Times |date=1996-12-10 |url=https://archive.nytimes.com/www.nytimes.com/library/cyber/week/1210math.html}} For errata, see {{cite web|url=http://www.mcs.anl.gov/home/mccune/nyt-corrections.html |archive-url=https://web.archive.org/web/19970605011316/http://www.mcs.anl.gov/home/mccune/nyt-corrections.html |date=1997-01-23 |archive-date=1997-06-05 |last=McCune |first=William |website=Argonne National Laboratory |title=Comments on Robbins Story}} This proof established that the Robbins axiom, together with associativity and commutativity, form a 3-basis for Boolean algebra. The existence of a 2-basis was established in 1967 by Carew Arthur Meredith:{{cite journal|last1=Meredith |first1=C. A. |author-link1=Carew Arthur Meredith |last2=Prior |first2=A. N. |author-link2=Arthur Prior |title=Equational logic |journal=Notre Dame J. Formal Logic |year=1968 |volume=9 |issue=3 |pages=212–226 |doi=10.1305/ndjfl/1093893457 |mr=0246753|doi-access=free }}

:$\backslash neg(\{\backslash neg\; x\}\; \backslash lor\; y)\; \backslash lor\; x\; =\; x,$

:$\backslash neg(\{\backslash neg\; x\}\; \backslash lor\; y)\; \backslash lor\; (z\; \backslash lor\; y)\; =\; y\; \backslash lor\; (z\; \backslash lor\; x).$

The following year, Meredith found a 2-basis in terms of the Sheffer stroke:{{cite journal|last=Meredith |first=C. A. |author-link1=Carew Arthur Meredith |title=Equational postulates for the Sheffer stroke |journal=Notre Dame J. Formal Logic |volume=10 |year=1969 |issue=3 |pages=266–270 |doi=10.1305/ndjfl/1093893713 |mr=0245423|doi-access=free }}

:$(x\backslash mid\; x)\; \backslash mid\; (y\backslash mid\; x)\; =\; x,$

:$x|(y\backslash mid(x\backslash mid\; z))\; =\; ((z\backslash mid\; y)\backslash mid\; y)\backslash mid\; x.$

In 1973, Padmanabhan and Quackenbush demonstrated a method that, in principle, would yield a 1-basis for Boolean algebra.{{cite journal |last1=Padmanabhan |first1=R. |last2=Quackenbush |first2=R. W. |title=Equational theories of algebras with distributive congruences |journal=Proc. Amer. Math. Soc. |date=1973 |volume=41 |issue=2 |pages=373–377 |doi=10.1090/S0002-9939-1973-0325498-2|doi-access=free }} Applying this method in a straightforward manner yielded "axioms of enormous length", thereby prompting the question of how shorter axioms might be found. This search yielded the 1-basis in terms of the Sheffer stroke given above, as well as the 1-basis

:$\backslash neg(\backslash neg(\backslash neg(x\; \backslash lor\; y)\; \backslash lor\; z)\; \backslash lor\; \backslash neg(x\; \backslash lor\; \backslash neg(\backslash neg\; z\; \backslash lor\; \backslash neg(z\; \backslash lor\; u))))\; =\; z,$

which is written in terms of OR and NOT.