On 03 Feb 2010, at 15:49, Jason Resch wrote:

## Advertising

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 infinitenumber of successive symbols, any computable function can beconstructed?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 somehowcreate 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 theprogram of the machine (theorem prover).Thanks,You are welcome. Such questions help to see where the difficultiesremain. Keep asking if anything is unclear.Thanks again, things are becoming a little more clear for me. Mybackground is in computer science, in case that applies and helps inwriting 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.