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] = h[h[a_, a_], h[a_, b_]] -> a; s[2, x_] := b_ -> h[h[b, b], h[b, x]]; s[3] = h[a_, h[a_, b_]] -> h[a, h[b, b]]; s[4] = h[a_, h[b_, b_]] -> h[a, h[a, b]]; s[5] = h[a_, h[a_, h[b_, c_]]] -> h[b, h[b, h[a, c]]];

the proof shown here can be represented by

{{s[2, b], {2}}, {s[4], {}}, {s[2, h[h[b, b], h[h[a, a], h[b, b]]]], {2, 2}}, {s[1], {2, 2, 1}}, {s[2, h[b, b]], {2, 2, 2, 2, 2, 2}}, {s[5], {2, 2, 2}}, {s[2, h[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[#, v[[1]]] &, u, {v[[2]]}]], h[a, b], proof]


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