Timeline for Is there a semantics for intuitionistic logic that is meta-theoretically "self-hosting"?
Current License: CC BY-SA 4.0
5 events
| when toggle format | what | by | license | comment | |
|---|---|---|---|---|---|
| Jun 29, 2021 at 14:09 | comment | added | მამუკა ჯიბლაძე | If one understands completeness of the self-hosting semantics for IPC as the claim that every Heyting algebra is the algebra of all truth values in some elementary topos, then this has been proven by Pataraia but still unpublished (for which, I must admit, I am responsible). | |
| Feb 24, 2021 at 1:30 | vote | accept | ttbo | ||
| Feb 23, 2021 at 15:09 | comment | added | Mike Shulman | Yes, you got it right, except that as Andrej says, the set of intuitionistic truth values is not just $\{0,1\}$. | |
| Feb 23, 2021 at 7:51 | comment | added | ttbo | I tried to semi-formalize the first part of your answer, as far as I understood it, and updated my question with the results. Can you let me know if I said anything wrong, or if I didn't get your meaning properly? Thanks. | |
| Feb 19, 2021 at 17:36 | history | answered | Mike Shulman | CC BY-SA 4.0 |