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

## Advertising

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 GoogleGroups "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.