Timeline for intuitionistic interpretation of classical logic
Current License: CC BY-SA 2.5
5 events
| when toggle format | what | by | license | comment | |
|---|---|---|---|---|---|
| Dec 15, 2014 at 23:23 | comment | added | Christoph-Simon Senjak | You can always get a $\bot$ equivalent if you set it to the conjunction of all atomic formulae in your proof. Furthermore, in the calculus of constructions, you can define $\bot$ as an inductive predicate with zero constructors, and ex falso quodlibet becomes the induction principle over $\bot$. | |
| Jun 5, 2011 at 13:03 | comment | added | Countably Infinite | What bothers me here is that Curry-Howard isomorphism, i.e. simple types, only yields minimal logic. Does the Godel-Gentzen translation also hold for minimal logic as a target? We would need to add a type constant for $\bot \rightarrow A$ to minimal logic (Ex Falso Quodlibet), to have inituitionist logic. | |
| Dec 9, 2009 at 18:56 | comment | added | Reid Barton | One should also comment that in the CPS translation, one can trivially implement callcc, whose type is Peirce's law, providing the link to classical logic. | |
| Dec 9, 2009 at 18:44 | history | edited | Dan Piponi | CC BY-SA 2.5 |
added 2233 characters in body
|
| Dec 9, 2009 at 5:34 | history | answered | Dan Piponi | CC BY-SA 2.5 |