Timeline for The Curry Howard Isomorphism and models for an intuitionistic modal logic and its bimodal translation
Current License: CC BY-SA 3.0
16 events
| when toggle format | what | by | license | comment | |
|---|---|---|---|---|---|
| S Apr 6, 2018 at 14:09 | history | bounty ended | CommunityBot | ||
| S Apr 6, 2018 at 14:09 | history | notice removed | CommunityBot | ||
| S Mar 29, 2018 at 12:38 | history | bounty started | user65526 | ||
| S Mar 29, 2018 at 12:38 | history | notice added | user65526 | Draw attention | |
| Mar 28, 2018 at 18:20 | history | edited | user65526 | CC BY-SA 3.0 |
Notational changes
|
| Mar 27, 2018 at 10:05 | comment | added | user65526 | Also, are there cases in which the same type of model can be given for both sides (the 'Lambda' side and the 'logic' side)? For then this would raise the question of whether the bi-modal model which can be given for the lax logic side (or some variant of this bi-modal model) can be used as a model for a 'Montague- style' or 'Gallin-style' logic on the Lambda side. | |
| Mar 27, 2018 at 10:01 | comment | added | user65526 | I don't want to drag in classical logic, necessarily. I just want to know whether you can have a perhaps Intuitionistic version of Montague's IL (see people.umass.edu/partee/NZ_2006/Appendix%20to%20Lecture%207.pdf and p.290 of isi.edu/~hobbs/montague.pdf ) or Gallin's TY2, on the "Lambda" side, since this is the language most linguists utilise | |
| Mar 27, 2018 at 6:50 | comment | added | Andrej Bauer | This looks like a serious question. It's a pity you did not ask it under a properly registred username, so we'd know who we're talking to. In any case, why do you want to drag in classical logic? There's plenty of work on modal lambda calculi, but I think most of them do not consider classical logic on top. The formalism they use is usually type theory, and the semantics ones go for presheaf and sheaf models (Kripke models are a particularly simple kind of presheaf models.) | |
| Mar 26, 2018 at 22:10 | history | edited | user65526 | CC BY-SA 3.0 |
deleted 8 characters in body
|
| Mar 26, 2018 at 16:16 | history | edited | user65526 | CC BY-SA 3.0 |
deleted 2 characters in body
|
| Mar 26, 2018 at 16:10 | history | edited | user65526 | CC BY-SA 3.0 |
added some details
|
| Mar 26, 2018 at 14:06 | history | edited | user65526 | CC BY-SA 3.0 |
added 40 characters in body
|
| Mar 26, 2018 at 13:57 | history | edited | user65526 | CC BY-SA 3.0 |
added 6 characters in body
|
| Mar 26, 2018 at 13:47 | history | edited | user65526 | CC BY-SA 3.0 |
added 103 characters in body
|
| Mar 26, 2018 at 12:02 | review | First posts | |||
| Mar 26, 2018 at 12:06 | |||||
| Mar 26, 2018 at 12:01 | history | asked | user65526 | CC BY-SA 3.0 |