# 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]:=
 Out[1]=

#### Show the 20th step:

 In[2]:=
 Out[2]=

#### Show the corresponding proof:

 In[3]:=
 Out[3]=

#### Show the data associated with lemma 20:

 In[4]:=
 Out[4]=

#### Find the number of lemmas used in the proof:

 In[5]:=
 Out[5]=

#### Pick out the statements used on the first 5 steps:

 In[6]:=
 Out[6]=

#### Plot the lengths of the statements used on all steps:

 In[7]:=
 Out[7]=

#### Find the longest statement:

 In[8]:=
 Out[8]=

#### Show the statement as a tree:

 In[9]:=
 Out[9]=
 In[10]:=

#### Plot the lengths of the proofs used:

 In[11]:=
 Out[11]=

#### Find the chain of dependencies in the first 5 steps:

 In[12]:=
 Out[12]=

#### Make a graph of dependencies:

 In[13]:=
 Out[13]=

#### A layered version:

 In[14]:=
 Out[14]=

#### A linear version:

 In[15]:=
 Out[15]=

#### Find the original axiom:

 In[16]:=
 Out[16]=

#### Find the statement of Lemma 1:

 In[17]:=
 Out[17]=

#### Determine that Lemma 1 can be proved from the axiom:

 In[18]:=
 Out[18]=

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

 In[19]:=
 Out[19]=

#### Visual representations of the statements on the first 10 steps:

 In[20]:=
 Out[20]=
 In[21]:=

### Analysis

Wolfram Research, "Proof of Wolfram's Axiom for Boolean Algebra" from the Wolfram Data Repository (2017)