No one knows what Peano arithmetic doesn't know
post by cousin_it · 2011-12-16T21:36:56.640Z · LW · GW · Legacy · 54 commentsContents
54 comments
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.
54 comments
Comments sorted by top scores.
comment by Zetetic · 2011-12-17T02:26:57.528Z · LW(p) · GW(p)
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.
Replies from: cousin_it↑ comment by cousin_it · 2011-12-17T02:51:48.900Z · LW(p) · GW(p)
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!
Replies from: Zetetic↑ comment by Zetetic · 2011-12-17T20:34:17.199Z · LW(p) · GW(p)
Something is going on with my comment, the middle section keeps disappearing.
Replies from: Zetetic↑ comment by Zetetic · 2011-12-17T20:49:12.424Z · LW(p) · GW(p)
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.
Replies from: Zetetic↑ comment by Zetetic · 2011-12-17T20:50:37.470Z · LW(p) · GW(p)
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.
Replies from: cousin_it↑ comment by cousin_it · 2011-12-17T22:28:15.229Z · LW(p) · GW(p)
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.
Replies from: Zeteticcomment by Will_Sawin · 2011-12-18T17:01:20.575Z · LW(p) · GW(p)
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!)
Replies from: cousin_it↑ comment by cousin_it · 2011-12-18T17:06:31.459Z · LW(p) · GW(p)
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?
Replies from: Will_Sawin↑ comment by Will_Sawin · 2011-12-18T17:10:47.274Z · LW(p) · GW(p)
No. I meant to include a trivial example. I believed that it would help clarify the point.
comment by wuthefwasthat · 2011-12-16T22:26:34.894Z · LW(p) · GW(p)
Well, that argument only goes through if the other theory is recursively enumerable, so PA isnt as awesome as you make it sound.
Replies from: cousin_itcomment by JoshuaZ · 2011-12-17T04:16:42.186Z · LW(p) · GW(p)
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.
Replies from: pengvado, cousin_it↑ comment by pengvado · 2011-12-17T17:56:31.793Z · LW(p) · GW(p)
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.".
comment by wuthefwasthat · 2011-12-16T23:57:00.245Z · LW(p) · GW(p)
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.
Replies from: cousin_it↑ comment by cousin_it · 2011-12-17T00:18:19.734Z · LW(p) · GW(p)
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...
Replies from: wuthefwasthat↑ comment by wuthefwasthat · 2011-12-17T06:35:43.531Z · LW(p) · GW(p)
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.
Replies from: cousin_it↑ comment by cousin_it · 2011-12-17T10:08:41.301Z · LW(p) · GW(p)
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 :-)
Replies from: wuthefwasthat↑ comment by wuthefwasthat · 2011-12-17T12:26:56.701Z · LW(p) · GW(p)
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.
comment by Arran_Stirton · 2011-12-21T06:44:17.405Z · LW(p) · GW(p)
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.
Replies from: cousin_it↑ comment by cousin_it · 2011-12-21T09:02:24.683Z · LW(p) · GW(p)
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.
Replies from: Arran_Stirton↑ comment by Arran_Stirton · 2011-12-21T10:06:55.377Z · LW(p) · GW(p)
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.
comment by snarles · 2011-12-18T12:44:34.821Z · LW(p) · GW(p)
So is PA the weakest system capable of encapsulating Turing logic?
Replies from: Will_Sawin↑ comment by Will_Sawin · 2011-12-18T17:02:46.873Z · LW(p) · GW(p)
No. You don't need induction to do so. You can just use arithmetic to slowly, slowly evaluate the TM until you find something that halts or don't. The oracle holds all the power.
comment by ScottMessick · 2011-12-18T03:51:45.468Z · LW(p) · GW(p)
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).
Replies from: cousin_it, dbaupp↑ comment by cousin_it · 2011-12-18T12:35:13.243Z · LW(p) · GW(p)
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.
↑ comment by dbaupp · 2011-12-18T10:53:58.663Z · LW(p) · GW(p)
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.
comment by wedrifid · 2011-12-17T03:32:52.343Z · LW(p) · GW(p)
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.
comment by Douglas_Knight · 2011-12-17T01:23:48.699Z · LW(p) · GW(p)
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.
Replies from: cousin_it↑ comment by cousin_it · 2011-12-17T02:06:14.602Z · LW(p) · GW(p)
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 ?
Replies from: Douglas_Knight↑ comment by Douglas_Knight · 2011-12-17T02:17:13.685Z · LW(p) · GW(p)
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.
comment by Anatoly_Vorobey · 2011-12-16T22:35:10.097Z · LW(p) · GW(p)
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.
Replies from: wuthefwasthat, cousin_it↑ comment by wuthefwasthat · 2011-12-16T22:40:00.626Z · LW(p) · GW(p)
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... =/
Replies from: Anatoly_Vorobey↑ comment by Anatoly_Vorobey · 2011-12-16T22:59:46.137Z · LW(p) · GW(p)
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.
Replies from: cousin_it↑ comment by cousin_it · 2011-12-16T23:14:40.839Z · LW(p) · GW(p)
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).
Replies from: wuthefwasthat↑ comment by wuthefwasthat · 2011-12-16T23:23:42.098Z · LW(p) · GW(p)
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.
Replies from: cousin_it, Anatoly_Vorobey↑ comment by cousin_it · 2011-12-16T23:35:04.589Z · LW(p) · GW(p)
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.
↑ comment by Anatoly_Vorobey · 2011-12-17T09:43:05.989Z · LW(p) · GW(p)
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.
Replies from: wuthefwasthat↑ comment by wuthefwasthat · 2011-12-17T20:00:12.172Z · LW(p) · GW(p)
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.
Replies from: Anatoly_Vorobey↑ comment by Anatoly_Vorobey · 2011-12-17T22:04:54.866Z · LW(p) · GW(p)
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).
↑ comment by cousin_it · 2011-12-16T22:41:48.968Z · LW(p) · GW(p)
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:
Replies from: Anatoly_VorobeyEmil 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.
↑ comment by Anatoly_Vorobey · 2011-12-16T22:53:00.306Z · LW(p) · GW(p)
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.
Replies from: cousin_it↑ comment by cousin_it · 2011-12-16T22:57:49.355Z · LW(p) · GW(p)
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 :-)
comment by James_Miller · 2011-12-16T22:07:11.527Z · LW(p) · GW(p)
This post has nothing to do with rationality and is likely to scare away readers who haven't the slightest idea what "Peano arithmetic" refers to. And calling your conclusion "obvious" sends a rather "obvious" message to a large subset of potential readers.
Replies from: cousin_it, Dorikka, cousin_it↑ comment by cousin_it · 2011-12-16T22:30:27.017Z · LW(p) · GW(p)
(I didn't downvote your comment.)
I have written many technical posts, and the next one I've got planned will be more difficult than this one. Several of those posts got promoted and I also got some comments like this one saying my half-baked ideas were a big part of what attracted them to LW. That's probably a bit too much flattery, but still :-) To be fair, I also got some comments similar to yours. Eliezer has also written many technical posts like the cartoon guide to Löb's theorem which is more complex than most of my posts, including this one.
I'd really like to continue writing about AI-related technical stuff on LW. Would removing the word "obvious" satisfy your complaint?
Replies from: wedrifid, kbaxter, shminux, James_Miller↑ comment by Shmi (shminux) · 2011-12-16T22:42:45.632Z · LW(p) · GW(p)
When reading a technical post, it would be nice to see something like an "assumed reader's background" note before all the gory details. And maybe a non-technical summary for the rest of us.
For example, in your case you could state that the target audience is (say) a 3rd year math undergrad or higher, familiar with the concepts of <...> and <...>
Replies from: cousin_it↑ comment by James_Miller · 2011-12-16T23:00:31.930Z · LW(p) · GW(p)
Perhaps you could put something in the title or first line of the post to signal that it will be (a) only of interest to people who enjoy mathematical philosophy and (b) not indicative of the kind of writing normally seen here. The fact that similar posts of yours have attracted readers to LW is, I acknowledge, evidence against my previous comment.
Also please do omit the term obvious from future articles. It's infuriating (for me at least) to read technical articles and not understand something the author has labeled "obvious".
If possible you might want to motivate why whatever you have written provides insight into rationality. EY, I think, at least eventually always does this with his writings.
Replies from: cousin_it↑ comment by cousin_it · 2011-12-16T23:07:42.498Z · LW(p) · GW(p)
Perhaps you could put something in the title or first line of the post to signal that it will be (a) only of interest to people who enjoy mathematical philosophy and (b) not indicative of the kind of writing normally seen here.
Done, sort of.
Also please do omit the term obvious from future articles.
Okay,
It's infuriating (for me at least) to read technical articles and not understand something the author has labeled "obvious".
whuh? Your past comments indicate that you're a college professor and have written a book on game theory! I'm surprised... Okay, point taken.
If possible you might want to motivate why whatever you have written provides insight into rationality.
Most of my technical posts are about the mathematics of decision theory and AI, not human rationality. That is also a traditional LW topic that predates me. In particular, I'm very interested in AIs that try to prove theorems, and this post is the sort of theoretical result that could be relevant to those. Also it's relevant to my next post which will be about decision theory, if I don't refute that result first :-)
↑ comment by Dorikka · 2011-12-16T22:38:11.756Z · LW(p) · GW(p)
If I see a bunch of stuff that I'm not familiar with and don't immediately want to make the effort to become familiar with, I just click out of the thread. I think that if things like this composed a larger fraction of the posts here, then there might be a problem, but that there really isn't one at the moment.