On 03 Feb 2010, at 15:49, Jason Resch wrote:
On Wed, Feb 3, 2010 at 3:14 AM, Bruno Marchal <marc...@ulb.ac.be>
wrote:
On 03 Feb 2010, at 03:00, Jason Resch wrote:
Is your point that with addition, multiplication, and an infinite
number of successive symbols, any computable function can be
constructed?
You can say so.
You could also have said that with addition + multiplication axioms
+ logic, any computable function can be proved to exist.
So I suppose that is what I was wondering, given at minimum, those,
how is the existence of a computable function proved to exist?
Could you provide an example of how a simple function, like f(x) =
x*2 exists, or is it a very tedious proof?
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)
And this is F(2, 1), together with its proof. Not very tedious, but
F(2010, 1005) would be much more tedious! Note that from this we can
also deduce the existential sentence ExF(x, 1), a typical sigma_1
sentence.
Or do the relations imposed by addition and multiplication somehow
create functions/machines?
You can say so but you need logic. Not just in the (meta)
background, but made explicit in the axiom of the theory, or the
program of the machine (theorem prover).
Thanks,
You are welcome. Such questions help to see where the difficulties
remain. Keep asking if anything is unclear.
Thanks again, things are becoming a little more clear for me. My
background is in computer science, in case that applies and helps in
writing an explanation for my question above.
The nice thing is that a function is partial recursive (programmable)
if an only if it is representable in a Sigma_1 complete theory.
A sigma_1 complete theory is a theory capable of proving all the true
sentences equivalent with ExP(x) with P decidable.
In particular the theory above (with some more axioms like s(x) = s(y)
-> x = y, ..) is Sigma_1 complete, and thus Turing universal. All
computable functions can be represented in that theory, and all
computations can be represented as a proof of a Sigma_1 sentence like
above.
To show that such a weak theory is Sigma_1 complete is actually long
and not so easy. But then, to prove that the game of life is turing
universal is rather long also. For weak system, such proof asks for
some "machine language programming", and the meticulous verification
that everything works well. Always tedious, and there are some subtle
points. It is well done in the book by Epstein and Carnielli, or
Boolos, Burgess and Jeffrey.
Here is another very short Turing universal theory (a purely
equational logic-free theory!) :
((K x) y) = x
(((S x) y) z) = ((x z)(y z))
(x = x)
(x = y) ==> (y = x)
(x = y) ; (y = z) ===> (x = z)
(x = y) ===> ((x z) = (y z))
(x = y) ===> ((z x) = (z y)) "===>" is informal deduction, and
";" is the informal "and".
You may look at my paper "Theoretical computer science and the natural
sciences" for more on this theory, and its probable importance in
deriving the shape of physics from numbers.
http://www.sciencedirect.com/science?_ob=ArticleURL&_udi=B75DC-4GX6J45-1&_user=532047&_coverDate=12%2F31%2F2005&_rdoc=1&_fmt=&_orig=search&_sort=d&view=c&_acct=C000026678&_version=1&_urlVersion=0&_userid=532047&md5=e087a268f1a31acd7cd9ef629e6dc543
Hmm... It is 32 $ ... You may look at my older posts on the
combinators (Smullyan's birds!). It is not important, I wanted just to
show you another example.
Bruno
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
everything-list+unsubscr...@googlegroups.com.
For more options, visit this group at
http://groups.google.com/group/everything-list?hl=en.
