# Re: Definition of universe

```
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