On 05 Feb 2010, at 13:13, ronaldheld wrote:
is there a free version of Theoretical computer science and the
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)" :)
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)
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
For more options, visit this group at