Minimal axioms for Boolean algebra: Difference between revisions

Content deleted Content added

Inline

Revision as of 19:56, 6 November 2018

The Wolfram axiom is the result of a computer exploration undertaken by Stephen Wolfram^[1] in his A New Kind of Science looking for the shortest single axiom equivalent to the axioms of Boolean algebra (or propositional calculus). The result^[2] of his search was an axiom with six NAND operations and three variables equivalent to Boolean algebra:

((a|b)\,|\,c)\;|\;(a\,|\,((a|c)\,|\,a))=c

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

Wolfram’s 25 candidates are precisely the set of Sheffer identities of length less or equal to 15 elements (excluding mirror images) that have no noncommutative models of size less or equal to 4 (variables).^[3]

Researchers have known for some time that single equational axioms (i.e., 1-bases) exist for Boolean algebra,^[4] including representation in terms of disjunction and negation and in terms of the Sheffer stroke. Wolfram proved^[5]^[6] that his equation is a single equational axiom for Boolean algebra, and he proved^[7] that there were no smaller single equational axioms for Boolean algebra expressed only with the NAND operation.

Proof of Wolfram's Axiom for Boolean Algebra

The steps in an automated proof of the correctness of Wolfram's Axiom have been published in the Wolfram Data Repository.^[6] Each step states what is being proved and gives a list of the steps required for a proof. Each individual step in the proof is performed by inserting the specified axiom or lemma, essentially using pattern matching, but with substitutions and rearrangements for variables being made.

Notes

^ Wolfram, 2002, p. 808–811 and 1174.
^ Rudy Rucker, A review of NKS, The Mathematical Association of America, Monthly 110, 2003.
^ William Mccune, Robert Veroff, Branden Fitelson, Kenneth Harris, Andrew Feist and Larry Wos, Short Single Axioms for Boolean algebra, J. Automated Reasoning, 2002.
^ Padmanabhan, R.; Quackenbush, R. W. (1973)
^ Wolfram, 2002, p. 810–811.
^ ^a ^b "Proof of Wolfram's Axiom for Boolean Algebra".
^ Wolfram, 2002, p. 1174.

References

Padmanabhan, R.; Quackenbush, R. W. (1973). "Equational theories of algebras with distributive congruences". Proc. Amer. Math. Soc. 41: 373–377.
doi:10.1090/S0002-9939-1973-0325498-2
.

Wolfram, Stephen (2002). A New Kind of Science. Wolfram Media.
ISBN 978-1579550080
.

External links

Stephen Wolfram, 2002, "A New Kind of Science, online".
Stephen Wolfram, 2018, "Logic, Explainability and the Future of Understanding"
Weisstein, Eric W. "Wolfram Axiom". MathWorld.
http://hyperphysics.phy-astr.gsu.edu/hbase/electronic/nand.html
Weisstein, Eric W. "Boolean algebra". MathWorld.
Weisstein, Eric W. "Robbins Axiom". MathWorld.
Weisstein, Eric W. "Huntington Axiom". MathWorld.

[1] Wolfram, 2002, p. 808–811 and 1174.

[2] Rudy Rucker, A review of NKS, The Mathematical Association of America, Monthly 110, 2003.

[3] William Mccune, Robert Veroff, Branden Fitelson, Kenneth Harris, Andrew Feist and Larry Wos, Short Single Axioms for Boolean algebra, J. Automated Reasoning, 2002.

[4] Padmanabhan, R.; Quackenbush, R. W. (1973)

[5] Wolfram, 2002, p. 810–811.

[Wolfram-6] "Proof of Wolfram's Axiom for Boolean Algebra".

[7] Wolfram, 2002, p. 1174.

[1]

[2]

[3]

[4]

[5]

[6]

[7]

@@ Line 7: / Line 7: @@
 Wolfram’s 25 candidates are precisely the set of Sheffer identities of length less or equal to 15 elements (excluding mirror images) that have no noncommutative models of size less or equal to 4 (variables).<ref>William Mccune, Robert Veroff, Branden Fitelson, Kenneth Harris, Andrew Feist and Larry Wos, Short Single Axioms for Boolean algebra, J. Automated Reasoning, 2002.</ref>
-Researchers have known for some time that single equational axioms (i.e., 1-bases) exist for Boolean algebra,<ref>{{Harvcoltxt|Padmanabhan, R.; Quackenbush, R. W.|1973}}</ref> including representation in terms of disjunction and negation and in terms of the Sheffer stroke. Wolfram proved<ref>Wolfram, 2002, p. 810–811.</ref><ref>{{cite web |url=https://datarepository.wolframcloud.com/resources/Proof-of-Wolframs-Axiom-for-Boolean-Algebra |title=Proof of Wolfram's Axiom for Boolean Algebra |doi=10.24097/wolfram.65976.data}}</ref> that his equation is a single equational axiom for Boolean algebra, and he proved<ref>Wolfram, 2002, p. 1174.</ref> that there were no smaller single equational axioms for Boolean algebra expressed only with the NAND operation.
+Researchers have known for some time that single equational axioms (i.e., 1-bases) exist for Boolean algebra,<ref>{{Harvcoltxt|Padmanabhan, R.; Quackenbush, R. W.|1973}}</ref> including representation in terms of disjunction and negation and in terms of the Sheffer stroke. Wolfram proved<ref>Wolfram, 2002, p. 810–811.</ref><ref name="Wolfram">{{cite web |url=https://datarepository.wolframcloud.com/resources/Proof-of-Wolframs-Axiom-for-Boolean-Algebra |title=Proof of Wolfram's Axiom for Boolean Algebra}}</ref> that his equation is a single equational axiom for Boolean algebra, and he proved<ref>Wolfram, 2002, p. 1174.</ref> that there were no smaller single equational axioms for Boolean algebra expressed only with the NAND operation.
+==Proof of Wolfram's Axiom for Boolean Algebra==
+The steps in an automated proof of the correctness of Wolfram's Axiom have been published in the Wolfram Data Repository.<ref name="Wolfram" /> Each step states what is being proved and gives a list of the steps required for a proof. Each individual step in the proof is performed by inserting the specified axiom or [[Lemma (mathematics)|lemma]], essentially using pattern matching, but with substitutions and rearrangements for variables being made.
 ==See also==
@@ Line 28: / Line 29: @@
 ==External links==
 *[[Stephen Wolfram]], 2002, "[http://www.wolframscience.com/nksonline/page-808 A New Kind of Science], online".
+*[[Stephen Wolfram]], 2018, "[https://blog.stephenwolfram.com/2018/11/logic-explainability-and-the-future-of-understanding/ Logic, Explainability and the Future of Understanding]"
 *{{MathWorld|urlname=WolframAxiom|title=Wolfram Axiom}}
 *http://hyperphysics.phy-astr.gsu.edu/hbase/electronic/nand.html

v t e Common logical connectives
Tautology/True $\top$
Alternative denial (NAND gate) $\uparrow$ Converse implication $\leftarrow$ Implication (IMPLY gate) $\rightarrow$ Disjunction (OR gate) $\lor$
Negation (NOT gate) $\neg$ Exclusive or (XOR gate) $\not \leftrightarrow$ Biconditional (XNOR gate) $\leftrightarrow$ Statement (Digital buffer)
Joint denial (NOR gate) $\downarrow$ Nonimplication (NIMPLY gate) $\nrightarrow$ Converse nonimplication $\nleftarrow$ Conjunction (AND gate) $\land$
Contradiction/False $\bot$
Philosophy portal