Timeline for Gödel's speed-up from constructive to classical logic?
Current License: CC BY-SA 3.0
5 events
| when toggle format | what | by | license | comment | |
|---|---|---|---|---|---|
| Mar 2, 2018 at 15:57 | comment | added | Ingo Blechschmidt | Aaron: This happens in some situations, but not here; and also, it's not a phenomenon particular to constructive mathematics. For instance, Peano arithmetic can prove, for any fixed natural number $n$, that Hercules can beat any hydra with $n$ heads. But Peano arithmetic can't prove "for any $n$, Hercules can beat any hydra with $n$ heads". | |
| Mar 2, 2018 at 15:52 | comment | added | Ingo Blechschmidt | Joel is right, one can constructively prove that the first player has a winning strategy. If you interpret that proof as a program and run it, you'll get an explicit winning strategy; however, the resulting algorithm will simply apply a brute-force search to find the strategy. If you want the extracted algorithm to be more clever, then you have to supply a more insightful proof that the first player has a winning strategy (one which doesn't use a strategy-stealing argument). | |
| Mar 1, 2018 at 22:47 | comment | added | Aaron Meyerowitz | That is true. So could a constructive mathematician say “I accept that $\forall n$ there is a proof of player one has a winning strategy but not that there is a proof of $\forall n$ player one has a winning strategy.? That would speak to complexity disparity. Then there are examples like $x_n$ is $1$ or $0$ according as $2^{p_n}-1$ is or is not prime and $y_n=x_n(1-x_n)$. Then $y_n=0$ or $y_{1000000}=0$ is very different constructively than classically. Maybe $2^{2^n}$ is better. | |
| Mar 1, 2018 at 21:45 | comment | added | Joel David Hamkins | I'm not really sure, but it seems to me in light of the comments on my answer that for any particular $n$, since this is a finite game, one might constructively prove (perhaps even by a short proof) the equivalence of the first player having a winning strategy with the second player not having a winning strategy. The reason I expect this might be true is that the equivalence of these two statements is essentially a statement of de Morgan's law in an instance where all quantifiers are bounded (essentially by n), and that seemed to be what was driving the phenomenon in the other case. | |
| Mar 1, 2018 at 20:34 | history | answered | Aaron Meyerowitz | CC BY-SA 3.0 |