On 04 Feb 2010, at 15:28, Jason Resch wrote:

On Wed, Feb 3, 2010 at 1:47 PM, Bruno Marchal <marc...@ulb.ac.be> wrote:

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).


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.


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.



So then it seems the integers, addition, and multiplication (plus some logic) are the minimum axioms needed to represent and prove true any computable function, and it is through this representability that the functions are said to exist. Is this correct?

The rule of addition and the rule of multiplication, with some amount of logic provides a universal programming language. That's correct.

And at the same time this provides a tiny formal theory of arithmetic. A generator of a tiny subset of Arithmetical Truth (the set of all true arithmetical sentences, written in first order arithmetical language).

Tiny, but already equivalent with a "block- description" of a universal dovetailing.

You cannot prove true a computable function. You can only prove proposition. A theory is just a set of formula closed for inference rule. Effective theory have a recursively enumerable set of theorems.

Theories proves propositions. And those are true when the theory is sound.

Universal systems computes functions. But a priori don't prove anything.

I hope your believe that any closed formula of arithmetic is either true or false. A logician would add "in the standard model of Arithmetic", but this can lead to confusion.

I can recall you exactly what is an arithmetical formula if you desire, but be patient the next days are rather time occupied, so just be patient.

Could the connection be made between mathematically provable true statements, and functions?

Of course. mathematical logic studies mainly that. A formula F(x, y) represent a function when it verifies the functionnal condition, i.e. AxAyAz F(x,y) & F(x, z) ->. y = z.

Actually you can see functions as particular case of relations, like above. But you can see relations as a particular case of functions, by taking the characteristic function of the set of n-uples in the relation.

But you have to understand well the difference between a true arithmetical proposition, and a provable arithmetical proposition, by me or you or that formal system, or that other one. Provable is always related to a theory. And provable(p) -> p systematically for all proposition when the theory is sound (and then no rich theory can prove this, no they can prove or even directly express its own correctness, by a theorem of Tarski).

For example, the product of 4 consecutive integers is 1 less than a square, is provably true because a function exists which embiodies the relationship, and it can be proven to be true? Whereas without the existence of a function, would it be unprovable?

I am not sure what you mean by provably true. It is provable in Peano Arithmetic, I suspect. But the function or functions you can associate with such a truth exists or not independently of the fact that such or other theories proves it.

Of course, if you believe in the axioms of some theory, you may believe in the existence of a function, because you can prove it in that theory you trust, but again, the truth is independent of the theory. Now the truth about numbers can be managed in richer (not necessarily made formal) theories like naive set theory, as everyone does in practice.

It is not clear to me what Sigma1 sentences are, I could not find a good definition anywhere.

It is subtle. It is part of recursion theory. I will define the notion of sigma_1 proposition instead. (sigma_1 sentence are defined syntactically by induction. The relation between sigma_1 proposition and sigma_1 sentence is that it is the same in the eyes of God (arithmetical truth), but this can usually not been seen by the machines, which explains a part of the subtlety).

Basically a sigma_1 proposition is a proposition asserting the existence of a number verifying some decidable property.

"There exists a number x such that x is prime" = there is a prime number, is a sigma_1 proposition.

Thanks to the existence of the zero searching algorithm for the critical zero of the Riemann zeta function, it is easy to understand that the negation of the Riemann conjecture is a sigma_1 proposition.

The propositions "There exist a stopping state for the machine u starting with y and z" give you a rich set of examples of sigma_1 proposition.

When such proposition are true, they are verifiable (provable- in the tiny arithmetic described above, accessible by the universal dovetailer based on a sigma_1 complete theory).

There is a theorem (well known by logicians) that in first order logic all quantified formula can be put in prenex form which means that all the quantifier precede the atomic formula. They can all have the shape:

AxEyAzEt .... Au P(x, y, z, t, ... u)

The sigma_1 are the one having the shape ExP(x) with P decidable (sigma_0).

The pi_1 are the negation of the sigma_1 ~Ex P(x), equivalent with Ax ~P(x), and given that P is decidable ~P(x) is too, and the pi_1 are thus the formula having the shape AxP(x) with P decidable.

f is the code of a total computable function means that for all x there is a y such phi_f(x) = y. Now phi_f(x) = y is decidable, so total(f) <-> AxEyP(f, x, y), so to be total is pi_2 or in pi_2.

The insolubility ladder follows the number of alternation of quantifiers in the formulas, by a theorem of Kleene. Sigma_1 complete = turing universal (roughly speaking). This is known as the arithmetical hierarchy.

If you define sigma_1-truth by the set of true sigma_1 proposition, and p_1-truth accordingly, as sigma_2-truth (cf ExAyP(x,y)), etc. then you can define arithmetical truth as the union of sigma_1 -truth, pi_1- truth, sigma_2 truth, etc.

All the sigma(pi)_truth notion can be defined in Peano Arithmetic, but their union cannot. The set of all truth cannot be defined in arithmetic, and thus cannot be axiomatized.

You could study some book in mathematical logic and computability (recursion) theory. Like Mendelson and Rogers. It helps for auda, and tiny part of those book can help for the seventh and eight step of the ud argument.

For auda, the book by Boolos 79, 93 help a lot! But they presume a good understanding of Mendelson and Rogers, or any good textbook in mathematical logic.



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 

Reply via email to