Drexel dragonThe Math ForumDonate to the Math Forum



Search All of the Math Forum:

Views expressed in these public forums are not endorsed by Drexel University or The Math Forum.


Math Forum » Discussions » sci.math.* » sci.math.independent

Topic: Axioms from Programs
Replies: 7   Last Post: Jul 3, 2014 1:28 PM

Advanced Search

Back to Topic List Back to Topic List Jump to Tree View Jump to Tree View   Messages: [ Previous | Next ]
Charlie-Boo

Posts: 1,585
Registered: 2/27/06
Axioms from Programs
Posted: Jul 2, 2014 6:24 PM
  Click to see the message monospaced in plain text Plain Text   Click to reply to this topic Reply

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 2-place 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?

C-B



Point your RSS reader here for a feed of the latest messages in this topic.

[Privacy Policy] [Terms of Use]

© Drexel University 1994-2014. All Rights Reserved.
The Math Forum is a research and educational enterprise of the Drexel University School of Education.