Timeline for Lowest Turing degree that allows a Turing machine to tell whether $\operatorname{Con}(PA)$?
Current License: CC BY-SA 3.0
28 events
| when toggle format | what | by | license | comment | |
|---|---|---|---|---|---|
| Apr 26, 2018 at 21:04 | review | Close votes | |||
| Apr 29, 2018 at 10:21 | |||||
| Apr 26, 2018 at 19:57 | comment | added | Christopher King | @CarlMummert yeah, I think I didn't think the question though enough | |
| Apr 26, 2018 at 19:56 | history | edited | Christopher King | CC BY-SA 3.0 |
deleted 206 characters in body
|
| Apr 26, 2018 at 19:52 | comment | added | Carl Mummert | That's why the issue of encoding $\alpha$ into the formula matters. We can't actually write all the bits of an oracle in the formula, instead we have to write a definition of the oracle in the language of Peano arithmetic. But then that definition is likely to find a different set of natural numbers depending on which model of Peano arithmetic we look at. | |
| Apr 26, 2018 at 19:43 | comment | added | Carl Mummert | @PyRulez: the example that you gave about $0'$ has the same issue - PA neither proves nor disproves that the $n$ in that example is in the halting set $K$. | |
| Apr 26, 2018 at 19:42 | comment | added | Carl Mummert | @PyRulez: So you are really saying something more like PA + Con(PA) $\vdash$ "$T^\alpha$ accepts". But then how do we specify the quoted phrase as a sentence of PA? | |
| Apr 26, 2018 at 19:42 | comment | added | Christopher King | @AlexMennen oh, that's true. | |
| Apr 26, 2018 at 19:41 | comment | added | Alex Mennen | @PyRulez all oracles of the form you describe are computable, since they can be computed by brute force searching for proofs in PA. Since this provides an explicit computation of them, any Turing machine with oracle access to them may as well have no oracle. | |
| Apr 26, 2018 at 19:41 | comment | added | Christopher King | @CarlMummert that oracle is not allowed thanks to the edit. | |
| Apr 26, 2018 at 19:40 | comment | added | Christopher King | @CarlMummert when I talk about oracle machine, I mean an ordered pair of a turing machine and an oracle. | |
| Apr 26, 2018 at 19:40 | comment | added | Carl Mummert | Separately, what if we consider the oracle $\alpha$ so that $\alpha(0) = 1$ if and only if $\text{Con}(PA)$ and $\alpha(n+1) = 0$ for all $n$. This has Turing degree 0, but it answers the question "Does Con(PA) hold?", in the same way that $K$ answers that question. | |
| Apr 26, 2018 at 19:39 | comment | added | Carl Mummert | @PyRulez: the machine itself can take any oracle as input, while still being the same machine, so I am not sure what you mean by a machine existing for one oracle but not another - the oracle is not part of the machine, it is a separate object that is used when the machine is executed. | |
| Apr 26, 2018 at 19:37 | comment | added | Christopher King | @CarlMummert well, for $0$, such a machine likely does not exist. | |
| Apr 26, 2018 at 19:36 | comment | added | Carl Mummert | @PyRulez: the definition of "decides Con(PA)" does not appear to depend on an oracle, as it is currently written | |
| Apr 26, 2018 at 19:34 | comment | added | Christopher King | @CarlMummert i.e. there has to exist a specific oracle machine with degree $d$ such that the oracle machine decides $Con(PA)$ | |
| Apr 26, 2018 at 19:33 | comment | added | Carl Mummert | Let me ignore that machine for a moment and ask the question I was really interested in: what does it mean for a degree to "allow a Turing machine to exist"? | |
| Apr 26, 2018 at 19:32 | comment | added | Christopher King | @CarlMummert What axioms is $T$ starting from to look for $Con(PA)$ and $\lnot Con(PA)$? | |
| Apr 26, 2018 at 19:30 | comment | added | Christopher King | @CarlMummert Starting from what set of axioms? If you start from $PA$, you'll never find either. (In particular, $T$ does not know what automatically whether it is in the $PA+Con(PA)$ or $PA+ \lnot Con(PA)$ universe. | |
| Apr 26, 2018 at 19:27 | comment | added | Christopher King | @AlexMennen Okay, I edited the question. Does that plug the leak (so to speak)? | |
| Apr 26, 2018 at 19:27 | history | edited | Christopher King | CC BY-SA 3.0 |
added 205 characters in body
|
| Apr 26, 2018 at 19:19 | comment | added | Alex Mennen | Consider the formula $\varphi(x):\iff Con(PA)$. The set $X:=\{x\mid\varphi(x)\}$ is computable. Let T be the Turing machine with oracle access to $X$, which accepts iff $0\in X$. Then PA+Con(PA) proves that T accepts and PA+ not Con(PA) proves that T rejects. So in some sense, the answer is the Turing degree 0. I don't think this is what you meant, so you'll have to clarify your question to explain why this solution doesn't count. | |
| Apr 26, 2018 at 19:14 | history | edited | Christopher King | CC BY-SA 3.0 |
added 15 characters in body; edited title
|
| Apr 26, 2018 at 18:40 | comment | added | Christopher King | @JohannesHahn yep, sure thing. Sorry if it was unclear. | |
| Apr 26, 2018 at 18:38 | comment | added | Johannes Hahn | Oh, so we're talking about "$PA+Con(PA) \vdash$ The machine with code $n$ halts" etc? Thanks, that clears it up. | |
| Apr 26, 2018 at 18:28 | history | edited | Christopher King | CC BY-SA 3.0 |
added 6 characters in body; added 1 character in body
|
| Apr 26, 2018 at 18:28 | comment | added | Christopher King | @JohannesHahn $T$ has to be a specific turing machine. You can describe turing machines in the language of arithmetic. | |
| Apr 26, 2018 at 18:21 | comment | added | Johannes Hahn | I'm not quite sure what you mean by "$PA + Con(PA) \vdash T\text{ accepts}$" ? As long as $T$ does not refer to an explicitly constructed Turing machine, this does not seem to be an assertion in the language of arithmetic. (Maybe I am missing something obvious here) A similar sounding question might be the one you wanted to ask: Let $B$ be the set of all $PA$-provable statement in the language of arithmetic. What is the Turing degree of $B$? It is clearly $\leq 0'$, because a halting oracle can be used to check if a proof-enumerating machine halts on any given arithmetic statement as input. | |
| Apr 26, 2018 at 18:01 | history | asked | Christopher King | CC BY-SA 3.0 |