Notes

Chapter 12: The Principle of Computational Equivalence

Section 9: Implications for Mathematics and Its Foundations


Implementation [of proof example]

Given the axioms in the form

s[1] = (a_ a_) (a_ b_) a;
s[2, x_] := b_ (b b) (b x); s[3] = a_ (a_ b_) a (b b); s[4] = a_ (b_ b_) a (a b);
s[5] = a_ (a_ (b_ c_)) b (b (a c));

the proof shown here can be represented by

{{s[2, b], {2}}, {s[4], {}}, {s[2, (b b) ((a a) (b b))], {2, 2}}, {s[1], {2, 2, 1}}, {s[2, b b], {2, 2, 2, 2, 2, 2}], {s[5], {2, 2, 2}}, {s[2, b b], {2, 2, 2, 2, 2, 1}}, {s[1], {2, 2, 2, 2, 2}}, {s[3], {2, 2, 2}}, {s[1], {2, 2, 2, 2}}, {s[4], {2, 2, 2}}, {s[5], {}}, {s[2, a], {2, 2, 1}}, {s[1], {2, 2}}, {s[3], {}}, {s[1], {2}}}

and applied using

FoldList[Function[{u, v}, MapAt[Replace[#, v1] &, u, {v2}]], a b, proof]



Image Source Notebooks:

From Stephen Wolfram: A New Kind of Science [citation]