Wolfram Data Repository

Immediate Computable Access to Curated Contributed Data

Proof of Wolfram's Axiom for Boolean Algebra

Steps in an automated proof of the correctness of Wolfram’s Axiom

The goal is to prove as theorems the three standard Sheffer axioms of Boolean algebra from Wolfram's single axiom.

Each step states what is being proved, then gives a list of the steps required for a proof.

The result is a proof that Wolfram's Axiom is a complete axiom for Boolean algebra. It is the simplest possible one.

The proof was first given in very small type on pages 810 and 811 of "A New Kind of Science".

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.

(2 columns, 85 rows)

Examples

Basic Examples

Retrieve the resource:

In[1]:=
ResourceObject["Proof of Wolfram's Axiom for Boolean Algebra"]
Out[1]=

Show the 20th step:

In[2]:=
ResourceData["Proof of Wolfram's Axiom for Boolean Algebra"][20]
Out[2]=

Show the corresponding proof:

In[3]:=
ResourceData[ "Proof of Wolfram's Axiom for Boolean Algebra"][20, "Proof"]
Out[3]=

Show the data associated with lemma 20:

In[4]:=
ResourceData["Proof of Wolfram's Axiom for Boolean Algebra"][ Key[{"Lemma", 20}]]
Out[4]=

Find the number of lemmas used in the proof:

In[5]:=
Count[Keys[ ResourceData[ "Proof of Wolfram's Axiom for Boolean Algebra"]], {"Lemma", _}]
Out[5]=

Pick out the statements used on the first 5 steps:

In[6]:=
Take[ResourceData["Proof of Wolfram's Axiom for Boolean Algebra"][All, "Statement"], 5]
Out[6]=

Plot the lengths of the statements used on all steps:

In[7]:=
ListLinePlot[ LeafCount /@ Values[ResourceData["Proof of Wolfram's Axiom for Boolean Algebra"][ All, "Statement"]], PlotRange -> All]
Out[7]=

Find the longest statement:

In[8]:=
Normal[Values[ MaximalBy[ ResourceData["Proof of Wolfram's Axiom for Boolean Algebra"][All, "Statement"], LeafCount]]]
Out[8]=

Show the statement as a tree:

In[9]:=
TreeForm[Normal[ Values[MaximalBy[ ResourceData["Proof of Wolfram's Axiom for Boolean Algebra"][All, "Statement"], LeafCount]]], VertexLabeling -> False]
Out[9]=
In[10]:=

Plot the lengths of the proofs used:

In[11]:=
ListLinePlot[ Length /@ Values[ResourceData["Proof of Wolfram's Axiom for Boolean Algebra"][ All, "Proof"]]]
Out[11]=

Find the chain of dependencies in the first 5 steps:

In[12]:=
Take[Normal[ KeyValueMap[#1 -> Keys[Rest[#2["Proof"]]] &, Rest[ResourceData[ "Proof of Wolfram's Axiom for Boolean Algebra"]]]], 5]
Out[12]=

Make a graph of dependencies:

In[13]:=
Graph[Flatten[ Thread[#, List, -1] & /@ Normal[KeyValueMap[#1 -> Keys[Rest[#2["Proof"]]] &, Rest[ResourceData[ "Proof of Wolfram's Axiom for Boolean Algebra"]]]]]]
Out[13]=

A layered version:

In[14]:=
Graph[Flatten[ Thread[#, List, -1] & /@ Normal[KeyValueMap[#1 -> Keys[Rest[#2["Proof"]]] &, Rest[ResourceData[ "Proof of Wolfram's Axiom for Boolean Algebra"]]]]], GraphLayout -> "LayeredDigraphEmbedding"]
Out[14]=

A linear version:

In[15]:=
Graph[Flatten[ Thread[#, List, -1] & /@ Normal[KeyValueMap[#1 -> Keys[Rest[#2["Proof"]]] &, Rest[ResourceData[ "Proof of Wolfram's Axiom for Boolean Algebra"]]]]], GraphLayout -> "LinearEmbedding"]
Out[15]=

Find the original axiom:

In[16]:=
axiom = ResourceData["Proof of Wolfram's Axiom for Boolean Algebra"][ Key[{"Axiom", 1}], "Statement"]
Out[16]=

Find the statement of Lemma 1:

In[17]:=
lemma1 = ResourceData["Proof of Wolfram's Axiom for Boolean Algebra"][ Key[{"Lemma", 1}], "Statement"]
Out[17]=

Determine that Lemma 1 can be proved from the axiom:

In[18]:=
FullSimplify[lemma1, ForAll[{a, b, c}, axiom]]
Out[18]=

Show the succession of trees used in the proof of Lemma 1:

In[19]:=
TreeForm[#, VertexLabeling -> False] & /@ Normal[Values[ ResourceData["Proof of Wolfram's Axiom for Boolean Algebra"][ Key[{"Lemma", 1}], "Proof"]]]
Out[19]=

Visual representations of the statements on the first 10 steps:

In[20]:=
Map[TreeForm[#, VertexLabeling -> False] &, Take[Normal[ Values[ResourceData[ "Proof of Wolfram's Axiom for Boolean Algebra"][All, "Statement"]]], 10], {2}]
Out[20]=
In[21]:=

Visualization

Analysis

Wolfram Research, "Proof of Wolfram's Axiom for Boolean Algebra" from the Wolfram Data Repository (2017)   https://doi.org/10.24097/wolfram.65976.data

Data Resource History

  • Date Created:

Source Metadata

Publisher Information

  • Publisher of Record: Wolfram Research