Timeline for Contrasting theorems in classical logic and constructivism
Current License: CC BY-SA 4.0
24 events
| when toggle format | what | by | license | comment | |
|---|---|---|---|---|---|
| Sep 11, 2021 at 19:27 | history | made wiki | Post Made Community Wiki by Stefan Kohl♦ | ||
| Apr 3, 2020 at 5:17 | comment | added | VS. | @FrankaWaaldijk If a statement is provable then is it necessarily in Sigma1? I think that will resolve my confusion. Thank you. | |
| Mar 30, 2020 at 10:14 | comment | added | VS. | @FrankaWaaldijk Ok. | |
| Mar 30, 2020 at 10:11 | comment | added | Franka Waaldijk | No, this is not possible. PA is conservative over Heyting Arithmetic HA (which is PA without excluded middle) with respect to $\Pi_0^2$ statements. PA proving P$\neq$NP implies that already HA proves P$\neq$NP. | |
| Mar 30, 2020 at 7:21 | comment | added | VS. | @FrankaWaaldijk FYI P\neq NP is \Pi^0_2 statement while P=NP is \Sigma^0_2 statement. So I still dont follow if P=NP is possible in Classical while P\neq NP is possible without LEM or LLPO? Also note P\neq NP in Classical implies P\neq NP without LEM or LLPO since P\neq NP is a \Pi^0_2 statement. | |
| Mar 30, 2020 at 6:52 | comment | added | Franka Waaldijk | @RobinSaunders : see above... (couldn't add your tag because to do so exceeded the text limit) | |
| Mar 30, 2020 at 6:47 | comment | added | Franka Waaldijk | This is partly a common situation in axiomatics... when we drop Euclid's fifth postulate, we get a weakening of Euclidean geometry. This weakening then allows us to add a non-parallelity axiom to obtain a non-Euclidean geometry which is contradictory to what we started with. Similarly intuitionistic first-order logic allows us to add non-classical axioms to obtain either full-blown INT or RUSS, which are contradictory to CLASS. Not adding these axioms gives us BISH, say. Historically Brouwer was by far the first (INT), which is why the terms intuitionistic and constructive get mixed. | |
| Mar 30, 2020 at 1:18 | comment | added | Robin Saunders | The terminology seems quite confusing! If I've understood right: when discussing mathematics, 'intuitionistic' contradicts 'classical' while 'constructive' is a weakening of both; but for logics, 'intuitionistic' is a weakening of 'classical'? | |
| Mar 29, 2020 at 22:55 | vote | accept | VS. | ||
| Mar 29, 2020 at 18:24 | comment | added | Franka Waaldijk | @VS. Your remark concerns Peano Arithmetic PA only...outside of PA there are many $\forall\exists$ statements which are true in CLASS but not in INT and/or RUSS, or vice versa. It so happens that P=NP is equivalent to a $\Pi_0^2$ statement so in that particular case INT and CLASS will agree. | |
| Mar 29, 2020 at 18:09 | comment | added | VS. | @FrankaWaaldijk For Pi_2^0 statements such contradiction cannot occur (that is true in classical and false in constructive) by cs.nyu.edu/pipermail/fom/2006-March/010113.html. How about for Sigma_2^0 statements which can be shown to be true in classical nevertheless false in constructive? Perhaps it is possible to prove P=NP in classical and P\neq NP in constructive. | |
| Mar 29, 2020 at 14:45 | comment | added | Franka Waaldijk | @VS. After your explanation I added some remarks on question 2. to my answer. The remarks are a bit generic, because specific examples would take too much detail (thus obscuring clarity for non-insiders). Hope you still can get the gist, if not I could try to specify a bit more. | |
| Mar 29, 2020 at 14:29 | history | edited | Franka Waaldijk | CC BY-SA 4.0 |
expanded after elucidation of the OP
|
| Mar 29, 2020 at 11:49 | comment | added | VS. | @FrankaWaaldijk For 2 I meant even if you do not get total contradiction like true and false perhaps we can get something that does not imply other under reasonable considerations or even perhaps contradicts other under reasonable considerations. | |
| Mar 29, 2020 at 8:31 | comment | added | Franka Waaldijk | @IngoBlechschmidt thanks Ingo! It will take me some time to read ( 27 pages...:-) ) but I will do my best and get back to you. Cheers Franka | |
| Mar 28, 2020 at 22:04 | comment | added | Ingo Blechschmidt | @Franka Thank you for providing motivation! I just added the proof to a paper draft of mine, please have a look at Footnote 9 in Section 2.2 and share any difficulties in following the argument so that I can improve it, for the benefit of all who are interested in this curious injection. :-) Section 2 of this paper aims to give a leisurely introduction to the internal language of the effective topos and is hopefully readable even without extensive knowledge of toposes. | |
| Mar 28, 2020 at 13:25 | comment | added | Franka Waaldijk | @IngoBlechschmidt on principle i would of course like to try it myself... but wisdom or (rather more likely) experience tells me i'd be very happy if you would spell it out for me :-) . do you have my email address? | |
| Mar 28, 2020 at 12:36 | comment | added | Ingo Blechschmidt | @Franka I meant $\mathbb{R}$, but indeed now that you say it I recall that Andrej proved it for $\mathbb{N}^\mathbb{N}$. Slides illustrating Andrej's proof are here (see slide 24/25). The argument easily adapts to $\mathbb{R}$, this is a fun exercise; if you want me to spell out the details, I'll gladly do so! | |
| Mar 28, 2020 at 12:20 | comment | added | Franka Waaldijk | @IngoBlechschmidt yes that is a nice addition. Am I correct in thinking that you mean an injection from Baire space $\mathbb{N}^{\mathbb{N}}$ into $\mathbb{N}$? Perhaps this also leads to an injection from $\mathbb{R}$ into $\mathbb{N}$ but I don't see this immediately, being poorly knowledged on toposes. | |
| Mar 28, 2020 at 11:06 | comment | added | Philippe Gaucher | (a) comes from the fact that the equality of two real numbers is not decidable. (a) just means that there are less well-defined total functions in INT and RUSS than in CLASS. | |
| Mar 28, 2020 at 10:50 | comment | added | Ingo Blechschmidt | This answer is spot on! I'd like to contribute the realizability topos given by infinite-time Turing machines as a further intriguing environment. Any topos has an "internal logic", but the one of this one is particularly challenges many mathematical intuitions shaped by classical logic. In this topos, there is no surjection $\mathbb{N} \to \mathbb{R}$ (as you would expect from CLASS), but there is an injection $\mathbb{R} \to \mathbb{N}$. This observation is due to Andrej Bauer. | |
| Mar 28, 2020 at 10:25 | history | edited | Franka Waaldijk | CC BY-SA 4.0 |
phrasing
|
| Mar 28, 2020 at 10:19 | history | edited | Franka Waaldijk | CC BY-SA 4.0 |
expanded slightly
|
| Mar 28, 2020 at 10:06 | history | answered | Franka Waaldijk | CC BY-SA 4.0 |