Chapter 12: The Principle of Computational Equivalence

Section 9: Implications for Mathematics and Its Foundations

Implementation [of operators from axioms]

Given an axiom system in the form {f[a, f[a, a]] a, f[a, b] f[b, a]} one can find rule numbers for the operators f[x, y] with k values for each variable that are consistent with the axiom system by using

Module[{c, v}, c = Apply[Function, {v = Union[Level[axioms, {-1}]], Apply[And, axioms]}]; Select[Range[0, kk2 - 1], With[{u = IntegerDigits[#, k, k2]}, Block[{f}, f[x_, y_] := u-1 - k x - y; Array[c, Table[k, {Length[v]}], 0, And]]] &]]

For k = 4 this involves checking nearly 164 or 4 billion cases, though many of these can often be avoided, for example by using analogs of the so-called Davis–Putnam rules. (In searching for an axiom system for a given operator it is in practice often convenient first to test whether each candidate axiom holds for the operator one wants.)

Image Source Notebooks:

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