Category Theory
Zulip Server
Archive

You're reading the public-facing archive of the Category Theory Zulip server.
To join the server you need an invite. Anybody can get an invite by contacting Matteo Capucci at name dot surname at gmail dot com.
For all things related to this archive refer to the same person.

Stream: deprecated: logic

Topic: Kripke frames (logical vs relational algebraic view)

Ralph Sarkis (Oct 13 2022 at 20:12):

Fix a set of atomic propositions. We can define a class of Kripke frames in the two following ways:

• We give a set of formulas in modal logic (over the atomic propositions), e.g. $\{P\vee \diamond Q \rightarrow \Box \Box P, \Box P\rightarrow \diamond P\}$ , and we consider the class of Kripke frames that satisfy all these formulas.
• We give a set of inequations between relations constructed from one binary relation $R$ and the language of allegories (an other algebraic language could be used), e.g. $\{R^o;R \leq R, R;R \leq R\}$, and we consider the class of Kripke frames such that the accessibility relation satisfies all these inequations.

Is the link between these two different methods fully understood? For example, we know that if the accessibility relation satisfies $R^o;R \leq R$, then the frame satisfies the formula $\diamond P \rightarrow \Box\diamond P$. Other examples of links between formulas and inequations are given in the table here (the inequations are given in the "frame condition" column in a non-algebraic language). The example I just gave is the row named 5 in that table.

I have a feeling this should be understood, but maybe I am not googling with the right language.

Valeria de Paiva (Oct 14 2022 at 04:06):

well, the correspondence between axioms in modal logic and conditions on the accessibility relations is what traditional modal logicians call "Correspondence Theory", see e.g. http://www.fenrong.net/projects/translation/papers/BenthemCh2.ps, so in some sense this is very well understood. But modal logic tends to be considered mostly as an extension of classical logic, and I don't know how much of a constructive or intuitionistic correspondence theory people have developed.

Henry Story (Oct 14 2022 at 13:18):

Interesting question.
Btw. There is also the work on the relation to coalgebras as in the paper Modal logics are coalgebraic,...

Ralph Sarkis (Oct 14 2022 at 13:29):

@Valeria de Paiva Thanks, this is a great chapter! With this new terminology I can simplify my question to: Is there an account of point-free correspondence theory (for modal logic)?

This led me to this chapter which gives the most complete account with many examples.

Valeria de Paiva (Oct 14 2022 at 14:30):

well, "the most complete account " is a tall order, but I'm sure it's enough to get some pointers.