Zetetic comments on No one knows what Peano arithmetic doesn't know - Less Wrong

17 Post author: cousin_it 16 December 2011 09:36PM

You are viewing a comment permalink. View the original post to see all comments and the full post content.

Article Navigation

Comments (52)

Comments (52)

You are viewing a single comment's thread.

Comment author: Zetetic 17 December 2011 02:26:57AM *  9 points [-]

Is there a formal system (not talking about the standard integers, I guess) whose provability oracle is strictly weaker than the halting oracle, but still uncomputable?

I did some reading and it looks like while there are some proofs of the existence of a dense set of intermediate Turing degrees, it's a bit difficult to pin down definite problems of intermediate degree. I found one paper that postulates a couple of possibly intermediate degree problems.

This article (same author) talks about some of the surrounding issues and some the difficulties with proving the existence of an intermediate computational process.

Given those difficulties, it isn't clear to me that intermediate proof oracles for formal systems exist and if they do it seems like that might be non-trivial, but I'm definitely not the best person to ask.

Comment author: cousin_it 17 December 2011 02:51:48AM *  5 points [-]

A quote from your last link:

In a similar vein, it was shown by Feferman that derivability in a formal theory fully reflects the structure of the r.e. degrees: for every r.e. degree d there is an axiomatizable theory whose collection of theorems has degree exactly d, see [10].

And [10] resolves to:

[10] S. Feferman. Degrees of unsolvability associated with classes of formalized theories. J. Symbolic Logic, 22:161–175, 1957.

I guess that's enough information to answer my question. Thanks a lot!

Comment author: Zetetic 17 December 2011 08:34:17PM *  0 points [-]

Something is going on with my comment, the middle section keeps disappearing.

Comment author: Zetetic 17 December 2011 08:49:12PM *  0 points [-]

I found another paper with an interesting result (unfortunately behind a pay wall). It asks what range of degrees occur for subtheories of arithmetic and concludes that a degree a is associated with these theories iff it's a complete degree. What does that mean?

Definition 10 A degree of recursive unsolvability a is said to be complete if there exists a degree b such that b' = a (According to Freiberg's theorem [6, p.265] a degree a is complete iff 0'<= a).

That makes sense because b' is basically a from b, but it's bad because 0' is the degree of the halting problem. The first Turing jump from deciable theories is of degree equal to the halting problem. So it looks like any undecidable (in distinction from Presberger and other decidable theories) first order subsystems of arithmetic, which to me would be the most intuitive theories, are going to be at least as strong as the halting problem. That is, if I'm reading this right - proof theory is sort of a hobby and I'm mostly self-taught.

Comment author: Zetetic 17 December 2011 08:50:37PM 4 points [-]

A more specific statement of the result from the paper is:

Lemma 1 Suppose that the theory T is omega consistent with repsect to some formula P(y) and that T has a finitely axiomatizable subtheory S satisfying

(i) Each recursive relation is definable in S

(ii) For every m = 0, 1, ....,

Then each subtheory of T is of complete degree

Also:

Corallary 6 Let T be the theory ZF or any extension of ZF. If T is omega consistent with respect to the formula then the degrees of subtheories of T are exactly the complete degrees.

ETA: Is this what you were referring to in:

Is there a formal system (not talking about the standard integers, I guess)

I'm not sure, I don't see a related reply/comment. Either way, I'm not 100% sure I'm following all of the arguments in the papers, but it appears that the theories that are of intermediate degree are necessarily very unusual and complicated, and I'm not sure how feasible it would be to construct one explicitly.

ETA2: I found yet another interesting paper that seems to state that finding a natural example of a problem of intermediate degree is a long standing open problem.

Comment author: cousin_it 17 December 2011 10:28:15PM *  2 points [-]

Thanks again for taking the time to parse all that!

ETA: Is this what you were referring to in:

Yeah, kind of. I didn't know the results but for some reason felt that subtheories of arithmetic shouldn't lead to intermediate degrees.

Comment author: Zetetic 17 December 2011 11:30:46PM 1 point [-]

No problem! It's an interesting topic with lots of surrounding results that are somewhat surprising (at least to me).

Powered by Reddit Powered by Reddit