Timeline for Gödel's speed-up from constructive to classical logic?
Current License: CC BY-SA 3.0
9 events
| when toggle format | what | by | license | comment | |
|---|---|---|---|---|---|
| Mar 1, 2018 at 21:17 | comment | added | Simon Henry | It is indeed an existence statement as asked, But that does not qualifies as something where the proof would become so long that it is not 'human readable' (It only takes 2 pages in the end) | |
| Mar 1, 2018 at 21:16 | comment | added | Simon Henry | I did encounter some example of things that where true constructively but whose proof was considerably harder than the classical one. One of them was the the following: let G be a compact localic group acting on a decidable set X. Then $X$ can be covered by finite subset stable under the action of $G$. Classically one easily show that the orbit of any point is a finite $G$ stable subset. but constructively it fails if we do not assume $G$ to be locally positive (Overt). I gave a completely different constructive proof of it in arxiv.org/abs/1505.04987. (prop 4.3 and lemma 4.2 and 4.1). | |
| Mar 1, 2018 at 20:34 | answer | added | Aaron Meyerowitz | timeline score: 2 | |
| Mar 1, 2018 at 19:14 | answer | added | Corey Bacal Switzer | timeline score: 1 | |
| Mar 1, 2018 at 13:15 | comment | added | Ingo Blechschmidt | Very interesting question. In my personal experience in algebra, a classically provable and interesting statement is either also constructively provable, with a proof of similar length, or there's an obvious reason for why there is no hope that a constructive proof exists. I'm speaking about informal proofs here, not proofs in some formal system. I'm looking forward to making a new experience and adapting my intuition! | |
| Mar 1, 2018 at 11:40 | answer | added | Alex Gavrilov | timeline score: 6 | |
| Mar 1, 2018 at 0:20 | history | edited | Ganon | CC BY-SA 3.0 |
added 788 characters in body
|
| Feb 28, 2018 at 20:43 | answer | added | Joel David Hamkins | timeline score: 12 | |
| Feb 28, 2018 at 18:00 | history | asked | Ganon | CC BY-SA 3.0 |