# Re: Definition of universe

On 05 Feb 2010, at 13:13, ronaldheld wrote:

Bruno:
is there a free version of Theoretical computer science and the
natural
sciences?

I have still many preprints. People interested can send me their addresses out of line.

Oops! I just see the axiom "3)" below is not correct. Please replace "x + 0 = 0" (which says that if you add nothing in your bank account, you make it empty!), by "x + 0 = x" (which says that if you add nothing to your bank account then it remains the same).

I hope everyone agree with this major change in the axiom "3)" :)

Bruno

I guess you ask: how is the existence of a computable function
proved to exist in a theory T. Usually logicians use the notion of
representability. The one variable function f(x)  is said to be
representable in the theory T, if there is a formula F(x, y) such
that when f(n) = m,  the theory T proves F(n, m), and usually
(although not needed) that T proves
Ax (F(n,x) -> x = m).

Here you will represent the function f(x) = x*2 by the formula F(x,
y) : y = x*2. Depending on your theory the proof of the true formula
F(n, m) will be tedious or not.  For example F(2, 1) is s(s(0)) =
s(0) * s(s(0), and you need a theory having at least logic +
equality rules, and the axioms

1) x * 0 = 0
2) x* s(y) = x * y   + x

3) x + 0 = 0
4) x + s(y) = s(x + y)

I let you prove that  s(s(0)) = s(0) * s(s(0) from those axioms
(using the usual axiom for egality).

s(0) * s(s(0)) = s(0) *s(0)   + s(0)        By axiom 2 with x = s(0)
and y = s(0)
s(0) *s(0)   + s(0) = s(s(0) + 0)            By axiom 4 with x =
s(0) *s(0) and y = 0
s(s(0) + 0)  = s(s(0))                             By substitution
of identical (logic + equality rules)
s(0) * s(s(0)) = s(s(0))                          Transitivity of
equality (logic + equality rules)
s(s(0)) = s(0) * s(s(0))                           equality rule (x
= y -> y = x)

http://iridia.ulb.ac.be/~marchal/

--
You received this message because you are subscribed to the Google Groups
"Everything List" group.
To post to this group, send email to everything-l...@googlegroups.com.
To unsubscribe from this group, send email to