Timeline for Examples of anti-classical theories in iFOL
Current License: CC BY-SA 4.0
6 events
| when toggle format | what | by | license | comment | |
|---|---|---|---|---|---|
| Oct 30 at 16:02 | comment | added | Emil Jeřábek | I don't know. It sounds like a basic thing that was probably observed before, but to be honest, I'm not well read in literature on intuitionistic logic. | |
| Oct 30 at 15:34 | comment | added | Jason Carr | Also: are there other original sources for the claims in the second half of this answer? Of course they're brief enough to understand here, but I was curious how much this topic has been addressed before | |
| Oct 30 at 15:17 | vote | accept | Jason Carr | ||
| Oct 30 at 15:16 | comment | added | Jason Carr | It took me a second to see why this schema is anti-classical. Since all intuitionistically definable functions can truly be computed by a Turing machine regardless of the presence of LEM, it would seem that each instance would be fine and so the whole would be. So the interesting character is in the $\forall x, \exists y, \phi(x, y) \to ...$ portion, for specific formulae. And so rather it's a direct assertion of the non-existence of such a proof for non-computable functions $\neg \forall x, \exists y, \phi(x,y)$. The contrapositive feels more enlightening here. | |
| Oct 30 at 12:20 | history | edited | Emil Jeřábek | CC BY-SA 4.0 |
edited body
|
| Oct 30 at 12:15 | history | answered | Emil Jeřábek | CC BY-SA 4.0 |