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.
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!
Something is going on with my comment, the middle section keeps disappearing.
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 Turing jump 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.
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.
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.
No problem! It's an interesting topic with lots of surrounding results that are somewhat surprising (at least to me).
More powerful formal systems are not more powerful because they know more stuff. They're more powerful because they have more confidence. PA proves that PA+Con(PA) proves Con(PA) (the proof, presumably, is not very long), but PA does not trust PA+Con(PA) to be accurate. ZFC is even more confident - has even fewer models - and so is even stronger. (Maybe it even has no models!)
More powerful formal systems are not more powerful because they know more stuff. They're more powerful because they have more confidence.
That's an awesome way of putting it, thanks!
PA proves that PA+Con(PA) proves Con(PA)
Duh, PA proves that PA+X proves X for any X, because X is one of the axioms of PA+X. Did you mean some less trivial example?
Zetetic gave a good response. I'd just like to note that the title is slightly inaccurate. Consider for example Goodstein's theorem. PA can't know whether Goodstein's theorem is true or not, but based on its truth in very weak, reasonably intuitive extensions of PA we should probably believe its truth. So we can know something that PA doesn't know albeit in a weak sense.
The title is a reference to No One Knows What Science Doesn't Know, from which I infer that it's supposed to be read as "There is some set {what PA knows}. No one can know exactly where the boundaries of this set are.", not "There is some set {what PA knows}. No one can know the truth value of any proposition not in this set.".
I believe the answer to your question is yes. I'm going to just interpret "formal system" as "first order theory", and then try to do the most straightforward thing.
Take a language L of intermediate degree, as constructed via the priority method. I'd like to just take the strings (or numbers) in this language to be the theory's axioms. So let the theory have some 1-ary relation, call it R, as well as +, and constants 0 and 1. Assert that everything has a successor, just to get the "natural numbers" (without having multiplication though). Then just include the axiom that says R(x) for all x in L, and not R(x) for all x not in L.
It seems pretty clear that the only things this theory proves are things that FOL proves, silly things about the successor function, and silly things about R, like "forall x, R(x) -> R(x)" and "(R(14) and R(12)) -> R(17)" where R(14) is false. So an oracle for the logical implications of this theory has the same degree as an oracle for L.
Don't feel like thinking about how to say/prove this part formally, but maybe someone can help (or correct) me. Also, for reference, Presburger arithmetic is basically arithmetic without multiplication, and is decidable.
I'm a little out of my depth here, so sorry if my comments don't make sense.
Then just include the axiom that says R(x) for all x in L, and not R(x) for all x not in L.
That's supposed to be a r.e. set of axioms, not a single axiom, right? I can easily imagine the program that successively prints the axioms R(x) for all x in L, but how do you enumerate the axioms not R(x) for all x not in L, given that L is only r.e. and not recursive? Or am I missing some easy way to have the whole thing as a single axiom without pulling in the machinery for running arbitrary programs and such?
On second thought, maybe we don't need the second part. Just having R(x) for all x in L could be enough.
It seems pretty clear that the only things this theory proves are things that FOL proves, silly things about the successor function, and silly things about R, like "forall x, R(x) -> R(x)" and "(R(14) and R(12)) -> R(17)" where R(14) is false. So an oracle for the logical implications of this theory is basically the same as an oracle for L.
I don't completely understand why there won't be an accidental smart thing among all the silly things...
I'm a little out of my depth here, so sorry if my comments don't make sense.
I'm not an expert either, so I'm probably just being unclear
That's supposed to be a r.e. set of axioms, not a single axiom, right? I can easily imagine the program that successively prints the axioms R(x) for all x in L, but how do you enumerate the axioms not R(x) for all x not in L, given that L is only r.e. and not recursive? Or am I missing some easy way to have the whole thing as a single axiom without pulling in the machinery for running arbitrary programs and such?
The axioms don't need to be r.e. If they were, the oracle would never be more helpful than a halting oracle, no?
I don't completely understand why there won't be an accidental smart thing among all the silly things...
I don't either. It's just a strong intuition which I'm not sure I can justify, and which might be wrong.
ETA: By silly, I don't necessarily mean as simple as the examples I gave. Basically if you have a formula phi(S(x), T, F), which holds for arbitrary sentences S(x), provably true T, and provably false S, then you can replace S(x) with R(x), T with R(x in L), and S with R(x not in L). Not sure if that was well explained, but yeah.
At least it looks like my answer is correct :). Also my proof should generalize, if it does work. So I would have guessed that Feferman's (stronger) result was true, and I wouldn't be surprised if the argument was along these lines, though maybe the details are harder.
If they were, the oracle would never be more helpful than a halting oracle, no?
But we want the oracle to be less helpful than the halting oracle...
Anyway, the question is settled now, thanks a lot :-)
Oops sorry! Ignore what I said there. Anyways, the axioms aren't necessarily r.e., but as far as I can tell, they don't need to be.
My knowledge of computability is far from extensive so please forgive me if this is a stupid question.
Does an oracle being able to determine if a statement is provable in Peano arithmetic necessarily be capable of proving that all of the Turing machines that halt for standard integers do in fact halt? Or to put it another way, is there a Turing machine that operates on some standard integer that cannot be proved in Peano arithmetic?
Thanks.
The post wasn't talking about Turing machines that accept standard integers as input, it was talking about Turing machines with no arguments. If such a machine halts, then PA has a proof that just enumerates all the steps the machine takes before halting.
Ah thanks, it seems I misread the whole "is there an integer N such that T takes N steps" as "is there an integer N such that T takes some number of steps then halts", sorry about that - brain malfunction I guess. Though now that I see what you mean rather than what I thought you meant, good post! Not old news to me, but them I'm relatively new to computability theory.
Imagine you have an oracle that can determine if an arbitrary statement is provable in Peano arithmetic. Then you can try using it as a halting oracle: for an arbitrary Turing machine T, ask "can PA prove that there's an integer N such that T makes N steps and then halts?". If the oracle says yes, you know that the statement is true for standard integers because they're one of the models of PA, therefore N is a standard integer, therefore T halts. And if the oracle says no, you know that there's no such standard integer N because otherwise the oracle would've found a long and boring proof involving the encoding of N as SSS...S0, therefore T doesn't halt. So your oracle can indeed serve as a halting oracle.
I don't think this works. We can't expect PA to decide whether or not any given Turing machine halts. For example, there is a machine which enumerates the theorems proven by PA and halts if it ever encounters a proof of 0=1. By incompleteness, PA will not prove that that this machine halts. (I'm assuming PA is consistent.) This argument works for any stronger consistent theory as well, such as ZFC or even much stronger ones. Note: I basically stole this argument from Scott Aaronson.
Note that this is different from the question of whether or not the halting problem is reducible to the set of theorems of PA (i.e. whether or not the oracle you've specified is enough to compute whether or not a given TM halts). It's just that this particular approach does not give such an algorithm.
ETA: I was in error, see replies. In the OP, PA doesn't need to prove that a non-halting machine doesn't halt, it only needs to fail to prove that it halts (and it certainly does, if we believe PA is sound).
The post argues that asking "does this machine halt?" is always equivalent to asking the oracle "does PA prove that this machine halts?" A counterexample should be a machine for which the answers to these two questions are different. Your machine is a "no" on both questions (it doesn't halt and PA doesn't prove that it halts), so it doesn't seem to be a counterexample.
Imagine you have an oracle that can determine if an arbitrary statement is provable in Peano arithmetic
[...] We can't expect PA to decide whether or not any given Turing machine halts
The oracle isn't working in PA, it's just deciding statements that are in PA.
I was just talking with Wei Dai and something came up that seems at once obvious and counterintuitive.
Agree on the obvious part!
In other words, if you knew all about the logical implications of PA, then you would also know all about the logical implications of ZFC and all other formal systems.
Ahh, now that is a little counterintuitive! Like it.
For you final question, I find it hard to imagine a notion of "formal system" that does not just mean "language." Then an RE formal system is the same as an RE language. If you insist on the terminology of proofs, you can take the words of the language as axioms and not have any rules of inference.
For your final question, I find it hard to imagine a notion of "formal system" that does not just mean "language."
How about http://en.wikipedia.org/wiki/First-order_logic#Syntax ?
So you agree that "provability oracle for an RE formal system" is the same as "membership oracle for an RE language" and your question is trivial?
ETA: No, first order languages does restrict the set of languages. But I object to this usage. "Formal systems" should include more general systems.
So having a provability oracle for PA, or any other formal system that has a model containing the standard integers (like ZFC), is equivalent to having a halting oracle
No, you need guarantees on the formal system's complexity, similar to the ones in Godel's incompleteness theorem(s). You also need the formal system to be sound for your argument to carry through. This is stronger than your "has a model containing the standard integers", and is equivalent to "has the standard integers as a model".
In other words, if you knew all about the logical implications of PA, then you would also know all about the logical implications of ZFC
Note that you're assuming here that PA is sound and in particular consistent.
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?
The halting oracle's uncomputability degree is the smallest possible uncomputable degree, so no.
The halting oracle's uncomputability degree is the smallest possible uncomputable degree, so no.
What? That's false. See http://en.wikipedia.org/wiki/Turing_degree#Post.27s_problem
ETA: Also, not sure what you are saying about soundness... =/
What? That's false.
Yeah, retracted above. Don't know what I was thinking.
ETA: Also, not sure what you are saying about soundness... =/
Suppose PA is inconsistent. Then a provability oracle for PA always answers "yes", and is completely useless as a halting problem oracle. Debugging cousin_it's argument with this example helps to see where he relies on PA being sound, that is, anything proved by PA being a true statement about N.
Right. Also there's always the freaky possibility that there's no such thing as the "standard integers". After all, we don't really have any formal grounds to believe that they exist, only unreliable evolved intuitions about counting apples, and these have already let us down many times (e.g. Russell's paradox).
Sure. You actually need something a bit stronger than soundness, in that you want omega-consistency, right?
I still don't agree/understand with what you two are saying about having the standard integers as a model, or interepreting PA with its own axioms, though (or anything along the lines of needing to contain PA). I think this argument holds as long as the other formal system is recursively enumerable, and if PA is omega-consistent.
Some parts of my post were just wrong, they're edited now. But other parts use the unspoken assumption that there's such a thing as "standard integers" (or, equivalently, there's such a thing as "Turing machines") and the axioms of PA are true statements about that thing. That seems to imply omega-consistency, but the whole argument is so informal that I can't tell for sure. It could be formalized somehow, I guess, but that was not the intent.
In the words of Liron Shapira, I'm talking about Turing machines as "their own meta-level thing", so statements about their halting or non-halting are to be interpreted as "facts of the matter" outside any formal system. The "standard integers" exist in the same limbo. That's where the handwavy reasoning about SSS...S0 comes from.
Yeah I know that's weird.
Are you confusing soundness with consistency? omega-consistency is much weaker than soundness.
Consistency: a syntactic claim that it's impossible to derive a contradiction. Doesn't require a notion of truth to be useful.
Omega-consistency: a syntactic claim that it's impossible to prove certain statements together. Doesn't need a notion of truth, but is motivated by the standard model of natural numbers.
Soundness: a semantic claim that given a specific notion of "true" as applies to a statement, e.g. truth in the model N of natural numbers, all the axioms of the theory are true. Automatically implies both consistency and omega-consistency. Requires a notion of the "intended model" or a "standard model" for the theory in which we consider the truth of propositions. For example, soundness is meaningless to talk about in the case of ZFC, which doesn't have an intended model.
I think this argument holds as long as the other formal system is recursively enumerable, and if PA is omega-consistent.
Look at this sentence from the argument:
"If the oracle says yes, you know that the statement is true for standard integers because they're one of the models of PA, therefore N is a standard integer, therefore T halts."
If the oracle for a formal system S says "yes" on a given statement S that encodes the proposition "a Turing machine T will halt on this input", this means that S proves this proposition. It does not mean that the proposition is true and T will in fact halt! For that to be true, you need the formal system S to be sound. S could easily be omega-consistent and not sound, in which case it'll lie to you (example, assuming you believe PA to be consistent: the formal system.
Soundness: a semantic claim that given a specific notion of "true" as applies to a statement, e.g. truth in the model N of natural numbers, all the axioms of the theory are true. Automatically implies both consistency and omega-consistency. Requires a notion of the "intended model" or a "standard model" for the theory in which we consider the truth of propositions. For example, soundness is meaningless to talk about in the case of ZFC, which doesn't have an intended model.
I looked it up, and it seems like what you're referring to as soundness is called "arithmetic soundness." The soundness I know doesn't require a notion of standard model. It simply says that anything provable syntactically is also true in every model/interpretation. This is automatically true for any theory in first order logic. (Note that my version of soundness is the correct analogue of completeness, which is also true for any FOL theory, as Godel showed, less trivially.)
"If the oracle says yes, you know that the statement is true for standard integers because they're one of the models of PA, therefore N is a standard integer, therefore T halts."
So here, the oracle says something of the form "exists x such that T halts after x steps". Omega-consistency guarantees that there is some actual standard number N so that "T halts after N steps" is provable/true. The existence of a standard model implies omega-consistency, so I might has well have gone with that, but I was just trying to be minimalist.
Sorry for the miscommunication. Are we on the same page now? I do think that saying "soundness" generally refers to the notion I said, though.
I looked it up, and it seems like what you're referring to as soundness is called "arithmetic soundness." The soundness I know doesn't require a notion of standard model. It simply says that anything provable syntactically is also true in every model/interpretation. This is automatically true for any theory in first order logic. (Note that my version of soundness is the correct analogue of completeness, which is also true for any FOL theory, as Godel showed, less trivially.)
It's just a different meaning of the word "soundness". The soundness you're talking about is really a property of a deductive system in first-order logic, as you point out. The soundness I'm talking about is a property of a theory w.r.t. a particular notion of truth defined for first-order formulas (and it's usually defined by fixing a structure and an interpretation, in that structure, of the logic's constant/function/relation symbols; in other words, a model). You're right that sometimes, when talking about the model N, it's referred to as "arithmetic soundness", but the modifier is not at all required. E.g. search for "a theory T is sound" on Google as a phrase, with quotation marks, to see usage examples. Or search for "sound" in this post: http://rjlipton.wordpress.com/2011/03/30/random-axioms-and-gdel-incompleteness/
Compare with the word "completeness", which, I'm sure you're aware, is also notoriously ambiguous: in "Godel's completeness theorem" and "Godel's incompleteness theorems" it refers to two totally different kinds of completeness. The difference between them is similar, though not identical, to the one between soundness as a property of a first-order logic and soundness as a property of a theory.
So here, the oracle says something of the form "exists x such that T halts after x steps". Omega-consistency guarantees that there is some actual standard number N so that "T halts after N steps" is provable/true.
Well, not quite. Why do you think that omega-consistency guarantees that? What is it about omega-consistency that guarantees anything to be true? It only speaks of things that are provable/nonprovable.
Let me try to be a bit more detailed. You actually need your theory S (the one you have an oracle for, be it PA or something else) to uphold two separate requirements:
When S proves a sentence of the form "Exists x such that T halts after x steps", you need that sentence to be true. This sentence is a Sigma1 sentence (let me know if I need to detail that further).
When there is a true sentence of the form "this is a run of T that ends after N steps" (which is a Sigma0 sentence), you need S to be able to prove it. This is what the original post means when it says "the oracle would have found a long and boring proof..." - you need this proof to actually exist! If S is too weak, it might not exist.
If you have both conditions, then the argument in the original post - the one that says an oracle for S can service as an oracle for the halting problem - goes through. In detail: if S proves T halts, by 1. T in fact halts. If S does not prove T halts, S cannot possibly prove "This is a run of T that ends after N steps" for any particular N, because if it could, it would also prove "T halts" by straightforward generalization. Therefore by 2. this cannot be true for any particular N, therefore T doesn't halt.
So far, omega-consistency is not even in the picture. How does it come in? The easiest way to ensure 1. and 2. is simply to require that
(i) S is Sigma1-sound, that is, every Sigma1 sentence it proves must be true. (ii) S is Sigma0-complete, that is, every true Sigma0 sentence is provable in S.
It turns out that (ii) is a fairly weak requirement, and every S that is strong enough to prove some basic statements about +, * and < satisfies it. The exact statement is that S must be stronger than Robinson's theory R. And, given (ii), (i) is in fact implied by omega-consistency. By itself, omega-consistency of S doesn't imply (i), but combined with Sigma0-completeness of S, it does. And here's why:
Let P be a Sigma1 sentence of the form "There exist x such that R(x)" provable in S, where R is Sigma0. Suppose P is actually false, and then R(N) is false for every specific N, then not-R(N) is true for every specific N, and it is provable in S for every specific N, by Sigma0-completeness. This directly contradicts the omega-consistency of S. Therefore P is true, and S is Sigma1-sound.
To sum up, it is enough to demand that S be omega-consistent if also it is strong enough to ensure that it is Sigma0-complete, and that requirement works two duties: both to translate omega-consistency into Sigma1-soundness which is what the argument really needs, and directly for the second half of the argument itself.
Phew. Hope I didn't make any stupid mistake there. Let me know if anything's unclear or disagreeable to you.
P.S. Note that the argument above depends crucially on the notion of what is "true", which is defined in the model N of natural numbers. You cannot apply it to some theory S which isn't able to speak of natural numbers at all (in fact, omega-consistency cannot be defined for such an S) or doesn't have the basic machinery of arithmetic functions and relations (because it's used to translate assertions about Turing machines into arithmetical statements). Thus my original remark that the argument depends on soundness of S. It was too broad in the sense that if you analyze the matter closely, you see that only Sigma1-soundness and not general soundness is required, as explained above, and that can be satisfied with omega-consistency and some modest strength. But the semantic requirements of having to talk about N and true statements doesn't go away (because you can't define Sigma0-completeness without that, and you do crucially need that for the argument to go through).
No, you need guarantees on the formal system's complexity, similar to the ones in Godel's incompleteness theorem(s).
Agreed. It's kind of obvious but I should've spelled that out, I guess.
This is stronger than your "has a model containing the standard integers", and is equivalent to "has the standard integers as a model".
I agree that my version is wrong, but yours doesn't sound completely right either. ZFC doesn't have the standard integers as a model, or does it? I thought it also included other objects...
Note that you're assuming here that PA is sound and in particular consistent.
Yes.
The halting oracle's uncomputability degree is the smallest possible uncomputable degree, so no.
Could you give a reference? Wikipedia seems to disagree but maybe I fail reading comprehension:
Emil Post studied the r.e. Turing degrees and asked whether there is any r.e. degree strictly between 0 and 0′. The problem of constructing such a degree (or showing that none exist) became known as Post's problem. This problem was solved independently by Friedberg and Muchnik in the 1950s, who showed that these intermediate r.e. degrees do exist.
I agree that my version is wrong, but yours doesn't sound right either. ZFC doesn't have the standard integers as a model, or does it? I thought it also included other objects...
My version is right, but perhaps too restricted. The reason your argument works for ZFC is because it interprets PA by proving its axioms as applied to particular sets in ZFC. So the general requirement would be for a system to be strong enough to prove certain true statements about the natural numbers and to disprove certain false statements.
Could you give a reference?
No, I wrote nonsense - I realized that and wanted to come back and edit it pointing out this exact link you gave, but you did that before me. I don't know enough about Post's problem or the Friedberg/Muchnik solutions to say whether they can be suitably presented as provability classes.
The reason your argument works for ZFC is because it interprets PA by proving its axioms as applied to particular sets in ZFC.
Nice! I didn't realize that. I guess the easiest way is to ask for the same guarantees that Gödel's theorems use, do you agree? For now, changed the post accordingly :-)
WARNING: this post requires some knowledge of mathematical logic and computability theory.
I was just talking with Wei Dai and something came up that seems at once obvious and counterintuitive. Though if the argument is correct, I guess it will be old news to about 50% of the people who read my posts :-)
Imagine you have an oracle that can determine if an arbitrary statement is provable in Peano arithmetic. Then you can try using it as a halting oracle: for an arbitrary Turing machine T, ask "can PA prove that there's an integer N such that T makes N steps and then halts?". If the oracle says yes, you know that the statement is true for standard integers because they're one of the models of PA, therefore N is a standard integer, therefore T halts. And if the oracle says no, you know that there's no such standard integer N because otherwise the oracle would've found a long and boring proof involving the encoding of N as SSS...S0, therefore T doesn't halt. So your oracle can indeed serve as a halting oracle.
On the other hand, if you had a halting oracle to begin with, you could use it as a provability oracle for PA: "if a program successively enumerates all proofs in PA, will it ever find a proof for such-and-such statement?"
So having a provability oracle for PA or any other consistent formal system that proves some valid arithmetic truths (like ZFC) is equivalent to having a halting oracle, and thus leads to a provability oracle for any other formal system. In other words, if you knew all about the logical implications of PA, then you would also know all about the logical implications of ZFC and all other formal systems. Hee hee.
ETA: this line leads to a nontrivial question. 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?
ETA 2: the question seems to be resolved, see Zetetic's comment and my reply.