Search All of the Math Forum:
Views expressed in these public forums are not endorsed by
Drexel University or The Math Forum.



Axioms from Programs
Posted:
Jul 2, 2014 6:24 PM


As soon as Peano published his axioms of arithmetic, others (e.g. Frege) tried to further reduce arithmetic by proving Peano's axioms.
However, we cannot reduce addition and multiplication further. They are so similar  both are 3 place relations where the 3rd place is a function of the 1st 2  that we have to show which of the 2 we are defining even after we state that we are going to define a fundamental 2place function. We have to define addition and define multiplication to show they are different. This is not the case for the naturals, where we have a single set (the universal set) and can appeal to concepts like time and set enumeration to define the single set of interest.
With the benefit of computer science, we can define these 3 relations completely formally as relations enumerated by computer programs. The naturals:
1. A = 0 2. Write A 3. A = A+1 4. Goto 2
This actually proves that the universal set (the naturals) is recursively enumerable. And we can prove Peano's 1st 5 axioms directly from the definition given for the natural numbers about which these axioms speak.
For example, axiom 1 is proven by having the rule that variable assignment leaves a variable at a value until reset, so in line 1 A is 0, and in line 2 there is an instance of A=0. Now line 2 writes A, so another rule says that the current value of A is a natural number, and we know 0 is one value for A. Therefore 0 is a natural number.
All we need to do is to devise some rules for translating a program into assertions that are then called axioms. (And also vice versa: programs from axioms.)
Likewise for the remaining axioms. We simply write computer programs to enumerate addition and multiplication, and derive the axioms from them.
What would be programs for enumerating addition and multiplication using primitives within the programs?
CB



