Timeline for Interpretations of modal logic where $\Box$ means "valid"
Current License: CC BY-SA 4.0
7 events
| when toggle format | what | by | license | comment | |
|---|---|---|---|---|---|
| Jun 10, 2023 at 14:31 | comment | added | PW_246 | This is impossible since a reflexive frame has the infinite sequence of related points $wRwRwR….$ for each point $w$. Provability Logic (modal logic GL) corresponds to finite, transitive, irreflexive frames. GL interprets $\Box$ as an encoding of a proof in a language that can formulate its own provability predicate. GL is characterized by $\Box (\Box P \to P) \to \Box P$, which takes reflexivity off the table immediately. | |
| Jul 31, 2020 at 18:26 | vote | accept | Andrew Bacon | ||
| Jul 31, 2020 at 9:13 | answer | added | Emil Jeřábek | timeline score: 10 | |
| Jul 31, 2020 at 8:16 | comment | added | Andrew Bacon | @AndrejBauer Sorry there was a typo in an earlier version of the question (I wrote "frame" instead of "model"). Does it make sense now: $w\Vdash B$ just means $B$ is true at $w$ in the pointed Kripke model $(W,R,w_0,[[.]])$ ? | |
| Jul 31, 2020 at 7:57 | comment | added | Andrej Bauer | What does $w \Vdash B$ stand for? I am reading your question as "Can we have a finite Kripke model $(W, R, w_0)$ such that, for all $A$, $w_0 \Vdash \Box A$ iff $w_0 \Vdash A$?" but I don't think that's what you are asking. (If it is, consider the trival model.) | |
| Jul 31, 2020 at 7:33 | history | edited | Andrew Bacon | CC BY-SA 4.0 |
I said "frame" when I meant "model"!
|
| Jul 31, 2020 at 1:33 | history | asked | Andrew Bacon | CC BY-SA 4.0 |