Timeline for Gödel's speed-up from constructive to classical logic?

Current License: CC BY-SA 3.0

7 events

when toggle format	what		by	license	comment
Feb 9, 2021 at 14:18	comment	added	Emil Jeřábek		My comment above should read “If the statement of Roth’s theorem were $\Pi_2$, ...”. In fact, as far as I can see, Roth’s theorem is only $\Pi_3$, now that I think about it.
Feb 9, 2021 at 10:33	comment	added	Emil Jeřábek		Since the statement of Roth’s theorem is $\Pi_2$, not only it automatically has a constructive proof once it has a classical proof, also the constructive proof is not much longer than the classical one. See en.wikipedia.org/wiki/Friedman_translation.
Mar 1, 2018 at 12:57	comment	added	Alex Gavrilov		You are right. I am convinced that the Schanuel conjecture can be proved in constructive logic, but this is just my personal opinion. Of course, such a proof ought to be pretty long. As for the Roth's theorem, I have no idea. It is conceivable that it cannot be proved in constructive second order arithmetic, for example.
Mar 1, 2018 at 12:43	comment	added	Joel David Hamkins		These are interesting examples, but the OP had requested examples where the statement is in fact provable both constructively and classically, but where the constructive proof was necessarily much longer. Do you have any reason to think that your examples are constructively provable, but do not have short constructive proofs?
Mar 1, 2018 at 12:27	history	edited	Alex Gavrilov	CC BY-SA 3.0	added 449 characters in body
Mar 1, 2018 at 11:59	comment	added	Todd Trimble		Along the same lines, we currently don't know that $e + \pi$ is transcendental, nor do we know that $e\pi$ is transcendental. But we know one of them must be, because if both were algebraic, then the roots of $x^2 - (e + \pi)x + e\pi$ would also be algebraic, contrary to what we know about $e$ and $\pi$.
Mar 1, 2018 at 11:40	history	answered	Alex Gavrilov	CC BY-SA 3.0