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.
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.
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 :-)
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”.
Note that you’re assuming here that PA is sound and in particular consistent.
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… =/
Yeah, retracted above. Don’t know what I was thinking.
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.
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.
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.)
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.
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.
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).
Agreed. It’s kind of obvious but I should’ve spelled that out, I guess.
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...
Yes.
Could you give a reference? Wikipedia seems to disagree but maybe I fail reading comprehension:
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.
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.
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 :-)