Timeline for What sets are "decidable from competing provers"?
Current License: CC BY-SA 3.0
11 events
| when toggle format | what | by | license | comment | |
|---|---|---|---|---|---|
| Jul 31, 2011 at 4:44 | vote | accept | CommunityBot | ||
| Jul 29, 2011 at 11:19 | comment | added | Carl Mummert | It's also theorem V.1.4 in Simpson's "Subsystems of Second-Order Arithmetic", and the proof there is very clear. | |
| Jul 29, 2011 at 7:24 | comment | added | Andreas Blass |
I'm away from home, so I can't easily look up a reference, but I would expect that the normal form for $\Sigma^1_1$ sets can be found in texts like Shoenfield's "Mathematical Logic", Hinman's "Fundamentals of Mathematical Logic", and Rogers's "Theory of Recursive Functions and Effective Computability." (It might be stated in a dual version, for $\Pi^1_1$ sets.)
|
|
| Jul 29, 2011 at 5:57 | comment | added | user5810 | Yes, now I see that the first implication does work for the main version. Do you have a reference for that normal form? (Also, it can be simplified to having the predicate use only bounded quantifiers.) Since the third implication is trivial, this would apparently answer my first two questions. | |
| Jul 29, 2011 at 5:18 | comment | added | Andreas Blass | Concerning Ricky Demer's second comment: You're right; the rules of such games can always be adjusted so that the winner can ignore the loser's moves. So my first comment wasn't worth making. | |
| Jul 29, 2011 at 5:16 | comment | added | Andreas Blass | Concerning the second half of Ricky Demer's first comment: The normal form begins with an existential quantifier over functions from natural numbers to natural numbers. That's followed by a universal quantifier over natural numbers, and then a recursive predicate (of the input and a finite initial segment of the quantified function). There is another normal form that begins with a quantifier over sets of natural numbers, but then you need two number quantifiers (a universal one followed by an existential one). | |
| Jul 29, 2011 at 5:16 | comment | added | Andreas Blass | Concerning the first half of Ricky Demer's first comment: I think the first implication works even if $M$ sometimes fails to halt when $Y$ and $N$ play badly. If $n\in S$ then $Y$ can make $M$ say yes (and then halt), so nothing $N$ does against that strategy can make $M$ say no. Conversely, if $n\notin S$ then $N$ has a winning strategy $w$, so for every strategy $s$ of $Y$, there will be a finite sequence of $N$ moves (an initial segment of what $w$ does against $s$) that causes $M$ to say no. | |
| Jul 29, 2011 at 3:58 | comment | added | user5810 | Also, you don't need a complexity analysis to show that a TM can be chosen so that strategies can be chosen to be non-interactive. Just have the player give a sequence coding what their inputs would be to the interactive version after any finite sequence of inputs from the other player. This translates the main question into one about computably open subsets of $\omega \times (\omega^{\omega})^2$, although I don't see that that helps. | |
| Jul 29, 2011 at 3:35 | comment | added | user5810 | Your first implication seems to only work for the always-halts version. Is the normal form of a $\Sigma_1^1$ definition supposed to be prenex disjunctive normal form with the set quantifier first? | |
| Jul 29, 2011 at 3:31 | comment | added | Andreas Blass | The second part of this proof shows that, for a suitable Turing machine $M$, the game between $Y$ and $N$ is not as interactive as one might think. The winning player doesn't need to pay any attention to what the other player is doing. If $n\in S$ then $Y$ can simply play a fixed witness $f$, ignoring $N$'s moves, and symmetrically if $n\notin S$ then $N$ can play a fixed witness $g$, ignoring $Y$'s moves. | |
| Jul 29, 2011 at 3:27 | history | answered | Andreas Blass | CC BY-SA 3.0 |