On 17 Oct 2013, at 11:08, LizR wrote:

On 17 October 2013 21:36, Bruno Marchal <marc...@ulb.ac.be> wrote:
Arithmetical truth is not Turing emulable.

Is that anything to do with the "halting problem" ?

The halting problem gives an example of a simple problem, which is not mechanically solvable. For all theories, there will be machines x such that those theories cannot prove proposition like "machine 567 does not halt", which will, when translated into arithmetic, defined an arithmetical truth escaping the power of that machine.

But there is the more complex problem "x is the code of a total computable function". As being more complex, it is simpler to show it being non soluble, (as we did if you see what I am thinking about) and so from it, you get that there is no general theory for deciding between totality and strict partiallity of machines, which for any machines will generates deeper and more complex functions to compute, or arithmetical set to decide, and that will define more complex arithmetical propositions.

When you look at computability in term of arithmetical provability, Turing universality correspond to the sigma_1 complete set. A proposition sigma_1 as the shape EnP(n), with P(n) being completely decidable (can even be a diophantine equation).

A machine, an entity, a set, a number... is said sigma_1 complete if, each time a proposition EnP(n) is true, it can prove it. It is complete in the sense of proving all true sigma_1 sentences.

You, Liz, are sigma_1 complete, (assuming you are immortal, we are working in Plato heaven, OK?). Indeed if there is a number n such that P(n), that is if EnP(n) is true, you can, given that P is easy to verify, verify P for 0, and if O does not very P, look at s(0), etc. If EnP(n) is true, that method guaranty that you will find it.

Sigma_1 completeness is one of the many characterization of Turing universality.

The price of universality? The existence, for all universal machines, to be in front of proposition like ~EnP(n), which are true but cannot be proved by them.

Note that those propositions ~EnP(n) are equivalent with An~P(n) (to say that there is no ferocious number is the same as saying that all numbers are not-ferocious).

And if P(n) is completely verifiable, decidable, ~P(n) is too. So the type of formula An~P(n) is really the same as the type AnP(n). Those are the pi_1 sentences, typically negation of sigma_1 sentences.

Then you have the sigma_2 sentences, with the shape EnAmP(n, m), with P(n, m) easily decidable.
And their negations, the pi_2 sentences, AnEmP(n, m), and so one.

The computable = the sigma_1

But arithmetical truth contains the true sigma_1, and the true pi_1 (which might, or not, contains Riemann hypothesis), the true sigma_2, etc. It is the union of all *true* sigma_i and pi_i formula. That set is not just non computable, but it is not definable in the arithmetic language (like the first person will be to).

The computable is only a very tiny part of arithmetical truth, but (with comp) the sigma_1 complete is already clever enough to get an idea how hard it is for itself to solve pi_problems, and above. It can also understand why it is concerned by those truth.

Machines can climbs those degrees of non solvability by the use of oracles, which are nothing more that the answer to some non solvable problems. This is useful to classify the degrees of insolubility. Imagine an oracle for the halting problem, well, that would help to solve pi_1 problems, but that would not provide a solution to the sigma_2 problems.

Hope I was not too much technical, we an come back on this, soon or later.

Bruno








--
You received this message because you are subscribed to the Google Groups "Everything List" group. To unsubscribe from this group and stop receiving emails from it, send an email to everything-list+unsubscr...@googlegroups.com.
To post to this group, send email to everything-list@googlegroups.com.
Visit this group at http://groups.google.com/group/everything-list.
For more options, visit https://groups.google.com/groups/opt_out.

http://iridia.ulb.ac.be/~marchal/



--
You received this message because you are subscribed to the Google Groups 
"Everything List" group.
To unsubscribe from this group and stop receiving emails from it, send an email 
to everything-list+unsubscr...@googlegroups.com.
To post to this group, send email to everything-list@googlegroups.com.
Visit this group at http://groups.google.com/group/everything-list.
For more options, visit https://groups.google.com/groups/opt_out.

Reply via email to