- ENGLISH
- JAPANESE
Interpolation properties for several logics
- \(v(A)\): the set of all propositional variables occurring in a formula \(A\).
- \(v^+(A)\): the set of all propositional variables occurring positively in a formula \(A\).
- \(v^-(A)\): the set of all propositional variables occurring negatively in a formula \(A\).
- A logic \(L\) is said to have Craig Interpolation Property (CIP) iff for any formulas \(A\) and \(B\), if \(L \vdash A \to B\), then there exists a formula \(C\) satisfying the following three conditions:
- \(v(C) \subseteq v(A) \cap v(B)\)
- \(L \vdash A \to C\)
- \(L \vdash C \to B\).
- A logic \(L\) is said to have Lyndon Interpolation Property (LIP) iff for any formulas \(A\) and \(B\), if \(L \vdash A \to B\), then there exists a formula \(C\) satisfying the following three conditions:
- \(v^+(C) \subseteq v^+(A) \cap v^+(B)\) and \(v^-(C) \subseteq v^-(A) \cap v^-(B)\)
- \(L \vdash A \to C\)
- \(L \vdash C \to B\).
- A logic \(L\) is said to have Uniform Interpolation Property (UIP) iff for any formula \(A\) and any finite set \(P\) of propositional variables, there exists a formula \(C\) satisfying the following three conditions:
- \(v(C) \subseteq v(A) \setminus P\)
- \(L \vdash A \to C\)
- \(L \vdash C \to B\) for any formula \(B\) satisfying \(L \vdash A \to B\) and \(v(B) \cap P = \emptyset\).
- A logic \(L\) is said to have Uniform Lyndon Interpolation Property (ULIP) iff for any formula \(A\) and any finite sets \(P^+\) and \(P^-\) of propositional variables, there exists a formula \(C\) satisfying the following three conditions:
- \(v^+(C) \subseteq v^+(A) \setminus P^+\) and \(v^-(C) \subseteq v^-(A) \setminus P^-\)
- \(L \vdash A \to C\)
- \(L \vdash C \to B\) for any formula \(B\) satisfying \(L \vdash A \to B\), \(v^+(B) \cap P^+ = \emptyset\), and \(v^-(B) \cap P^- = \emptyset\).
Intermediate Propositional Logics
Exactly seven intermediate propositional logics have CIP (Maksimova (1977)).
| Logics | ULIP | UIP | LIP | CIP |
|---|---|---|---|---|
| \(\mathbf{Int}\), \(\mathbf{IPC}\) | \(\checkmark\) Kurahashi (202?) New! |
\(\checkmark\) Pitts (1992) | \(\checkmark\) Maksimova (1982) | \(\checkmark\) Schütte (1962) |
| \(\mathbf{KC}\)\(\mathbf{Int} + (\neg p \lor \neg \neg p)\) | \(\checkmark\) Kurahashi (202?) New! |
\(\checkmark\) Maksimova (2014) | \(\checkmark\) Maksimova (1982) | \(\checkmark\) Gabbay (1971) |
| \(\mathbf{LP}_2\)\(\mathbf{Int} + (p \lor (p \to q \lor \neg q))\) | \(\checkmark\) local tabularity | \(\checkmark\) local tabularity | \(\checkmark\) Shimura (1992) | \(\checkmark\) Maksimova (1977) |
| \(\mathbf{LV}\)\(\mathbf{LP}_2 + (p \to q) \lor (q \to p) \lor (p \leftrightarrow \neg q)\) | \(\checkmark\) local tabularity | \(\checkmark\) local tabularity | \(\checkmark\) Kurahashi (202?) New! |
\(\checkmark\) Maksimova (1977) |
| \(\mathbf{LC}\)\(\mathbf{Int} + (p \to q) \lor (q \to p)\) | \(\checkmark\) local tabularity | \(\checkmark\) local tabularity | \(\checkmark\) Kuznets and Lellmann (2018) | \(\checkmark\) Maksimova (1977) |
| \(\mathbf{LS}, \mathbf{LC}_2\)\(\mathbf{LP}_2 + (p \to q) \lor (q \to p)\) | \(\checkmark\) local tabularity | \(\checkmark\) local tabularity | \(\checkmark\) Maksimova (1982) | \(\checkmark\) Maksimova (1977) |
| \(\mathbf{Cl}\), \(\mathbf{CPC}\)\(\mathbf{Int} + (p \lor \neg p)\) \(\mathbf{Int} + (\neg \neg p \to p)\) |
\(\checkmark\) local tabularity | \(\checkmark\) local tabularity | \(\checkmark\) Lyndon (1959) | \(\checkmark\) Craig (1957) |
Modal Propositional Logics
Survey paper (Maksimova (1991))
Intuitionistic Modal Propositional Logics
| Logics | ULIP | UIP | LIP | CIP |
|---|---|---|---|---|
| \(\mathbf{N}\mathbf{A}_{m, n}\) \((\mathbf{N} + \dfrac{\neg \Box A}{\neg \Box \Box A}) \oplus (\Box^n p \to \Box^m p) \) | \(\checkmark\) Sato (2025) New! |
\(\checkmark\) | \(\checkmark\) | \(\checkmark\) |
| \(\mathbf{N}^+\mathbf{A}_{m, n}\) \((\mathbf{N} + \dfrac{\neg \Box A}{\neg \Box \Box A}) \oplus (\Box^n p \to \Box^m p) \) | \(\checkmark\) Sato (2025) New! |
\(\checkmark\) | \(\checkmark\) | \(\checkmark\) |
| \(\mathbf{NRA}_{m, n}\) \(\mathbf{NR}\oplus (\Box^n p \to \Box^m p) \) | \(\checkmark\) Sato (2025) New! |
\(\checkmark\) | \(\checkmark\) | \(\checkmark\) |
| \(\mathbf{E}\) \(\mathbf{Cl} + \dfrac{A \leftrightarrow B}{\Box A \leftrightarrow \Box B}\) | \(\checkmark\) Akbar Tabatabai, Iemhoff, and Jalali (2021) | \(\checkmark\) Pattinson (2013) | \(\checkmark\) | \(\checkmark\) |
| \(\mathbf{EC}\) \(\mathbf{E} + (\Box p \land \Box q \to \Box (p \land q))\) | - | - | - | - Akbar Tabatabai, Iemhoff, and Jalali (2021) |
| \(\mathbf{EN}\) \(\mathbf{E} + \dfrac{A}{\Box A}\) | \(\checkmark\) Akbar Tabatabai, Iemhoff, and Jalali (2021) | \(\checkmark\) | \(\checkmark\) | \(\checkmark\) |
| \(\mathbf{ECN}\) \(\mathbf{EC} + \dfrac{A}{\Box A}\) | - | - | - | - Akbar Tabatabai, Iemhoff, and Jalali (2021) |
| \(\mathbf{M}\) \(\mathbf{Cl} + \dfrac{A \to B}{\Box A \to \Box B}\) | \(\checkmark\) Akbar Tabatabai, Iemhoff, and Jalali (2021) | \(\checkmark\) Santocanale and Venema (2010) | \(\checkmark\) | \(\checkmark\) |
| \(\mathbf{MC}\) \(\mathbf{M} + (\Box p \land \Box q \to \Box (p \land q))\) | \(\checkmark\) Akbar Tabatabai, Iemhoff, and Jalali (2021) | \(\checkmark\) | \(\checkmark\) | \(\checkmark\) |
| \(\mathbf{MN}\) \(\mathbf{M} \oplus \dfrac{A}{\Box A}\) | \(\checkmark\) Akbar Tabatabai, Iemhoff, and Jalali (2021) | \(\checkmark\) | \(\checkmark\) | \(\checkmark\) |
| \(\mathbf{MNP}\) \(\mathbf{MN} \oplus \neg \Box \bot\) | ? | ? | ? | ? |
| \(\mathbf{MND}\) \(\mathbf{MN} \oplus (\Box p \to \Diamond p)\) | ? | ? | ? | ? |
| \(\mathbf{MN4}\) \(\mathbf{MN} \oplus (\Box p \to \Box \Box p)\) | ? | ? | ? | ? |
| \(\mathbf{MNP4}\) \(\mathbf{MNP} \oplus (\Box p \to \Box \Box p)\) | ? | ? | ? | ? |
| \(\mathbf{MND4}\) \(\mathbf{MND} \oplus (\Box p \to \Box \Box p)\) | ? | ? | ? | ? |
| \(\mathbf{K}\) \(\mathbf{MCN}\) \(\mathbf{N} + (\Box(p \to q) \to (\Box p \to \Box q))\) |
\(\checkmark\) Kurahashi (2020) | \(\checkmark\) Ghilardi (1995) Visser (1996) |
\(\checkmark\) Maksimova (1982) Fitting (1983) |
\(\checkmark\) Gabbay (1972) |
| \(\mathbf{KD}\)\(\mathbf{K} \oplus \neg \Box \bot\) \(\mathbf{K} \oplus (\Box p \to \Diamond p)\) |
\(\checkmark\) Kurahashi (2020) | \(\checkmark\) Iemhoff (2019) | \(\checkmark\) | \(\checkmark\) Rautenberg (1983) |
| \(\mathbf{KT}\)\(\mathbf{K} \oplus (\Box p \to p)\) | \(\checkmark\) Kurahashi (2020) | \(\checkmark\) Bílková (2007) | \(\checkmark\) Maksimova (1982) Fitting (1983) |
\(\checkmark\) Gabbay (1972) |
| \(\mathbf{KB}\)\(\mathbf{K} \oplus (p \to \Box \Diamond p)\) | \(\checkmark\) Kurahashi (2020) | \(\checkmark\) Kurahashi (2020) | \(\checkmark\) Kuznets (2016) | \(\checkmark\) |
| \(\mathbf{KDB}\)\(\mathbf{K} \oplus (\neg \Box \bot) \oplus (p \to \Box \Diamond p)\) | \(\checkmark\) Kurahashi (2020) | \(\checkmark\) Kurahashi (2020) | \(\checkmark\) Kuznets (2016) | \(\checkmark\) |
| \(\mathbf{KTB}\)\(\mathbf{K} \oplus (\Box p \to p) \oplus (p \to \Box \Diamond p)\) | \(\checkmark\) Kurahashi (2020) | \(\checkmark\) Kurahashi (2020) | \(\checkmark\) Kuznets (2016) | \(\checkmark\) Rautenberg (1983) |
| \(\mathbf{K4}\)\(\mathbf{K} \oplus (\Box p \to \Box \Box p)\) | - | - Bílková (2007) | \(\checkmark\) Maksimova (1982) Fitting (1983) |
\(\checkmark\) Gabbay (1972) |
| \(\mathbf{K} \oplus (\Box p \to \Box^{n+1} p)\) | - | - | \(\checkmark\) Kuznets (2016) | \(\checkmark\) Gabbay (1972) |
| \(\mathbf{wK4}\)\(\mathbf{K} \oplus (p \land \Box p \to \Box \Box p)\) | - | - | - | - Karpenko and Maksimova (2010) |
| \(\mathbf{DL}\)\(\mathbf{wK4} \oplus (p \to \Box \Diamond p)\) | - | - | - | - Karpenko and Maksimova (2010) |
| \(\mathbf{K5}\)\(\mathbf{K} \oplus (\Diamond p \to \Diamond \Box p)\) | \(\checkmark\) local tabularity Kurahashi (2020) |
\(\checkmark\) local tabularity Maksimova (2014) |
\(\checkmark\) Kuznets (2016) | \(\checkmark\) |
| \(\mathbf{KD5}\)\(\mathbf{K} \oplus \neg \Box \bot \oplus (\Diamond p \to \Diamond \Box p)\) | \(\checkmark\) local tabularity Kurahashi (2020) |
\(\checkmark\) local tabularity Maksimova (2014) |
\(\checkmark\) Kuznets (2016) | \(\checkmark\) |
| \(\mathbf{K45}\)\(\mathbf{K} \oplus (\Box p \to \Box \Box p) \oplus (\Diamond p \to \Diamond \Box p)\) | \(\checkmark\) local tabularity Kurahashi (2020) |
\(\checkmark\) local tabularity Maksimova (2014) |
\(\checkmark\) Kuznets (2016) | \(\checkmark\) |
| \(\mathbf{KD45}\)\(\mathbf{K} \oplus \neg \Box \bot \oplus (\Box p \to \Box \Box p) \oplus (\Diamond p \to \Diamond \Box p)\) | \(\checkmark\) local tabularity Kurahashi (2020) |
\(\checkmark\) local tabularity Maksimova (2014) |
\(\checkmark\) Kuznets (2016) | \(\checkmark\) |
| \(\mathbf{KB5}\)\(\mathbf{K} \oplus (p \to \Box \Diamond p) \oplus (\Diamond p \to \Diamond \Box p)\) | \(\checkmark\) local tabularity Kurahashi (2020) |
\(\checkmark\) local tabularity Maksimova (2014) |
\(\checkmark\) Kuznets (2016) | \(\checkmark\) |
At most 36 consistent normal extensions of \(\mathbf{S4}\) have CIP (Maksimova (1979)).
30 of them are known to have CIP and the status of CIP for the remaining 6 is open.
It suffices to consider modal companions of intermediate logics having CIP.
Modal Companions of \(\mathbf{Int}\)
| Logics | ULIP | UIP | LIP | CIP |
|---|---|---|---|---|
| \(\mathbf{S4}\)\(\Gamma(\mathbf{Int}, \omega, \omega)\) \(\mathbf{KT4}\) \(\mathbf{K} \oplus (\Box p \to p) \oplus (\Box p \to \Box \Box p)\) |
- | - Ghilardi and Zawadowski (1995) | \(\checkmark\) Maksimova (1982) Fitting (1983) |
\(\checkmark\) Gabbay (1972) |
| \(\Gamma(\mathbf{Int}, \omega, 2)\) | ? | ? | ? | ? |
| \(\Gamma(\mathbf{Int}, \omega, 1)\)\(\mathbf{S4} \oplus (\Box(\Box (p \to \Box p) \to p) \to (\Box \Diamond \Box p \to p))\) | ? | ? | ? | \(\checkmark\) Maksimova (1987) |
| \(\Gamma(\mathbf{Int}, 2, \omega)\) | ? | ? | ? | \(\checkmark\) Maksimova (1980) |
| \(\Gamma(\mathbf{Int}, 2, 2)\) | ? | ? | ? | ? |
| \(\Gamma(\mathbf{Int}, 2, 1)\) | ? | ? | ? | \(\checkmark\) Maksimova (?) |
| \(\mathbf{S4.1}\)\(\Gamma(\mathbf{Int}, 1, \omega)\) \(\mathbf{S4} \oplus (\Box \Diamond p \to \Diamond \Box p)\) |
? | ? | \(\checkmark\) Maksimova (1982) | \(\checkmark\) Gabbay (1972) |
| \(\Gamma(\mathbf{Int}, 1, 2)\) | ? | ? | ? | ? |
| \(\mathbf{Grz}\)\(\Gamma(\mathbf{Int}, 1, 1)\) \(\mathbf{K} \oplus (\Box (\Box (p \to \Box p) \to p) \to p)\) |
\(\checkmark\) Kurahashi (2020) | \(\checkmark\) Visser (1996) | \(\checkmark\) Maksimova (2014) | \(\checkmark\) Boolos (1980) |
Modal Companions of \(\mathbf{KC}\)
| Logics | ULIP | UIP | LIP | CIP |
|---|---|---|---|---|
| \(\mathbf{S4.2}\)\(\Gamma(\mathbf{KC}, \omega, \omega)\) \(\mathbf{S4} \oplus (\Diamond \Box p \to \Box \Diamond p)\) |
? | ? | \(\checkmark\) Kuznets (2016) | \(\checkmark\) Gabbay (1972) |
| \(\Gamma(\mathbf{KC}, \omega, 2)\) | ? | ? | ? | ? |
| \(\Gamma(\mathbf{KC}, \omega, 1)\)\(\mathbf{S4.2} \oplus (\Box(\Box (p \to \Box p) \to p) \to (\Box \Diamond \Box p \to p))\) | ? | ? | ? | \(\checkmark\) Maksimova (1987) |
| \(\Gamma(\mathbf{KC}, 2, \omega)\) | ? | ? | ? | \(\checkmark\) Maksimova (1980) |
| \(\Gamma(\mathbf{KC}, 2, 2)\) | ? | ? | ? | ? |
| \(\Gamma(\mathbf{KC}, 2, 1)\) | ? | ? | ? | \(\checkmark\) Maksimova (?) |
| \(\mathbf{S4.2.1}\)\(\Gamma(\mathbf{KC}, 1, \omega)\) \(\mathbf{S4} \oplus (\Box \Diamond p \leftrightarrow \Diamond \Box p)\) |
? | ? | \(\checkmark\) Maksimova (1982) | \(\checkmark\) Gabbay (1972) |
| \(\Gamma(\mathbf{KC}, 1, 2)\) | ? | ? | ? | ? |
| \(\mathbf{Grz.2}\)\(\Gamma(\mathbf{KC}, 1, 1)\) \(\mathbf{Grz} \oplus (\Diamond \Box p \to \Box \Diamond p)\) |
\(\checkmark\) Kurahashi (202?) New! |
\(\checkmark\) Maksimova (2014) | \(\checkmark\) Maksimova (2014) | \(\checkmark\) Rautenberg (1983) |
Modal Companions of \(\mathbf{LP}_2\)
| Logics | ULIP | UIP | LIP | CIP |
|---|---|---|---|---|
| \(\Gamma(\mathbf{LP}_2, \omega, 1)\)\(\mathbf{S4.04}\) \(\mathbf{S4} \oplus (p \land \Box \Diamond \Box p \to \Box p)\) |
\(\checkmark\) local tabularity | \(\checkmark\) local tabularity | \(\checkmark\) Shimura (1992) | \(\checkmark\) Schumm (1976) |
| \(\Gamma(\mathbf{LP}_2, 2, 1)\) | \(\checkmark\) local tabularity | \(\checkmark\) local tabularity | \(\checkmark\) Kurahashi (202?) New! |
\(\checkmark\) Maksimova (1980) |
| \(\Gamma(\mathbf{LP}_2, 1, \omega)\) | - | \(\checkmark\) local tabularity | - Kurahashi (202?) New! |
\(\checkmark\) Maksimova (1980) |
| \(\Gamma(\mathbf{LP}_2, 1, 2)\) | - | \(\checkmark\) local tabularity | - Maksimova (1982) | \(\checkmark\) Maksimova (1980) |
| \(\mathbf{GW}\)\(\Gamma(\mathbf{LP}_2, 1, 1)\) \(\mathbf{Grz} \oplus (\neg p \to \Box(p \to \Box p))\) |
\(\checkmark\) local tabularity | \(\checkmark\) local tabularity | \(\checkmark\) Shimura (1992) | \(\checkmark\) Schumm (1976) |
Modal Companions of \(\mathbf{LV}\)
| Logics | ULIP | UIP | LIP | CIP |
|---|---|---|---|---|
| \(\Gamma(\mathbf{LV}, \omega, 1)\) | \(\checkmark\) local tabularity | \(\checkmark\) local tabularity | \(\checkmark\) Kurahashi (202?) New! |
\(\checkmark\) Maksimova (1980) |
| \(\Gamma(\mathbf{LV}, 2, 1)\) | \(\checkmark\) local tabularity | \(\checkmark\) local tabularity | \(\checkmark\) Kurahashi (202?) New! |
\(\checkmark\) Maksimova (1980) |
| \(\Gamma(\mathbf{LV}, 1, \omega)\) | - | \(\checkmark\) local tabularity | - Kurahashi (202?) New! |
\(\checkmark\) Maksimova (1980) |
| \(\Gamma(\mathbf{LV}, 1, 2)\) | - | \(\checkmark\) local tabularity | - Maksimova (1982) | \(\checkmark\) Maksimova (1980) |
| \(\mathbf{GV}\)\(\Gamma(\mathbf{LV}, 1, 1)\) \(\mathbf{GW} \oplus (\Diamond \Box p \land \Diamond \Box q \land \Diamond \Box r \to \Diamond \Box (p \land q) \lor \Diamond \Box (p \land r) \lor \Diamond \Box (q \land r))\) |
\(\checkmark\) local tabularity | \(\checkmark\) local tabularity Maksimova (2014) |
\(\checkmark\) Kurahashi (202?) New! |
\(\checkmark\) Maksimova (1980) |
There is no modal companions of \(\mathbf{LC}\) having CIP (Maksimova (1982))
Modal Companions of \(\mathbf{LS}\)
| Logics | ULIP | UIP | LIP | CIP |
|---|---|---|---|---|
| \(\mathbf{S4.4}\)\(\Gamma(\mathbf{LS}, \omega, 1)\) \(\mathbf{S4} \oplus (p \land \Diamond \Box p \to \Box p)\) |
\(\checkmark\) local tabularity | \(\checkmark\) local tabularity | \(\checkmark\) Shimura (1992) | \(\checkmark\) Schumm (1976) |
| \(\Gamma(\mathbf{LS}, 2, 1)\) | \(\checkmark\) local tabularity | \(\checkmark\) local tabularity | \(\checkmark\) Kurahashi (202?) New! |
\(\checkmark\) Maksimova (1980) |
| \(\Gamma(\mathbf{LS}, 1, \omega)\) | - | \(\checkmark\) local tabularity | - Kurahashi (202?) New! |
\(\checkmark\) Maksimova (1980) |
| \(\Gamma(\mathbf{LS}, 1, 2)\) | - | \(\checkmark\) local tabularity | - Maksimova (1982) | \(\checkmark\) Maksimova (1980) |
| \(\mathbf{GW.2}\)\(\Gamma(\mathbf{LS}, 1, 1)\) \(\mathbf{GW} \oplus (\Diamond \Box p \to \Box \Diamond p)\) |
\(\checkmark\) local tabularity | \(\checkmark\) local tabularity Maksimova (2014) |
\(\checkmark\) Maksimova (1982) | \(\checkmark\) Schumm (1976) |
Modal Companions of \(\mathbf{Cl}\)
| Logics | ULIP | UIP | LIP | CIP |
|---|---|---|---|---|
| \(\mathbf{S5}\)\(\Gamma(\mathbf{Cl}, \omega, 0)\) \(\mathbf{S4} \oplus (\Diamond p \to \Box \Diamond p)\) |
\(\checkmark\) local tabularity Kurahashi (2020) |
\(\checkmark\) local tabularity | \(\checkmark\) Fitting (1983) | \(\checkmark\) Schumm (1976) |
| \(\Gamma(\mathbf{Cl}, 2, 0)\) | - | \(\checkmark\) local tabularity | - Maksimova (1982) | \(\checkmark\) Maksimova (1980) |
| \(\mathbf{Triv}\)\(\Gamma(\mathbf{Cl}, 1, 0)\) \(\mathbf{K} \oplus (p \leftrightarrow \Box p)\) |
\(\checkmark\) local tabularity | \(\checkmark\) local tabularity Maksimova (2014) |
\(\checkmark\) Maksimova (1982) | \(\checkmark\) Maksimova (1980) |
Provability Logics
| Logics | ULIP | UIP | LIP | CIP |
|---|---|---|---|---|
| \(\mathbf{GL}\)\(\mathbf{K} \oplus (\Box(\Box p \to p) \to \Box p)\) | \(\checkmark\) Kurahashi (2020) | \(\checkmark\) Shavrukov (1993) Visser (1996) |
\(\checkmark\) Shamkanov (2011) | \(\checkmark\) Smoryński (1978) Boolos (1979) |
| \(\mathbf{S}\)\(\mathbf{GL} + (\Box(\Box p \to p) \to \Box p)\) | \(\checkmark\) Sierra Miranda (2025+) | \(\checkmark\) | \(\checkmark\) | \(\checkmark\) Boolos (1980) Beklemishev (1987) |
| \(\mathbf{D}\)\(\mathbf{GL} + \neg \Box \bot + (\Box(\Box p \lor \Box q) \to \Box p \lor \Box q)\) | - | - | - | - Beklemishev (1989) |
| \(\mathbf{I}\)Polymodal: \(\mathbf{GL}\) for every \([n]\) + for \(m \leq n\) \(([m] p \to [n][m] p) \oplus (\langle m \rangle p \to [n] \langle m \rangle p)\) |
? | ? | ? | ? |
| \(\mathbf{J}\)Polymodal: \(\mathbf{I} \oplus ([m]p \to [m][n]p)\) for \(m \leq n\) | - | - Shamkanov (2011) | \(\checkmark\) Shamkanov (2011) | \(\checkmark\) |
| \(\mathbf{GLP}\)Polymodal: \(\mathbf{I} \oplus ([m]p \to [n] p)\) for \(m \leq n\) | ? | \(\checkmark\) Shamkanov (2011) | ? cf. Shamkanov (2011) |
\(\checkmark\) Ignatiev (1993) Beklemishev (2010) |
| \(\mathbf{wGL}_n\)\(\mathbf{K} \oplus (\Box (\Box^n p \to p) \to \Box p)\) | ? | ? | \(\checkmark\) Iwata (2021) | \(\checkmark\) Sacchetti (2001) |
| \(\mathbf{R}\)Witness comparison \(\prec, \preccurlyeq\)： \(\mathbf{GL}\) + order axioms + \(\dfrac{\Box A}{A}\) |
- | - | - | - Sidon (1994) |
| \(\mathbf{GR}\)Bimodal：\(\mathbf{GL}(\Box) \oplus (\triangle p \to \Box p) \oplus (\Box p \to \Box \triangle p)\) \(\oplus (\Box p \to (\Box \bot \lor \triangle p)) \oplus (\Box \neg p \to \Box \neg \triangle p) + \dfrac{\Box A}{A}\) |
? cf. Kogure and Kurahashi (202?) |
\(\checkmark\) Kogure and Kurahashi (202?) New! |
\(\checkmark\) Kogure and Kurahashi (202?) New! |
\(\checkmark\) Sidon (1994) |
| \(\mathbf{CS}\)Bimodal：\(\mathbf{GL}(\Box) \oplus \mathbf{GL}(\triangle)\) \(\oplus (\Box p \to \triangle \Box p) \oplus (\triangle p \to \Box \triangle p)\) |
? | ? | ? | ? |
| \(\mathbf{CSM}\)Bimodal：\(\mathbf{CS} \oplus (\Box p \to \triangle p)\) | ? | ? | ? | ? |
| \(\mathbf{CDC}\)Bimodal：\(\mathbf{CSM} \oplus (\triangle p \to \Box (\triangle \bot \lor p))\) | ? | ? | ? | ? |
| \(\mathbf{CSM} \oplus (\triangle (\Box p \to p))\) | ? | ? | ? | ? |
| \(\mathbf{GLT}\)Bimodal：\(\mathbf{CSM} \oplus (\triangle p \leftrightarrow \triangle \Box p)\) | ? | ? | ? | ? |
| \(\mathbf{GF}\)Bimodal：\(\mathbf{GL}(\Box) \oplus \mathbf{KD}(\triangle)\) \(\oplus (\Box p \to \Box \triangle p) \oplus (\Box p \to \triangle \Box p)\) \((\Box p \leftrightarrow (\Box \bot \lor \triangle p)) \oplus (\triangle p \to \triangle ((\triangle q \to q) \lor \triangle p))\) |
? | ? | ? | ? |
| \(\mathbf{PF}\)Bimodal：\(\mathbf{GL}(\Box) \oplus \mathbf{S4.2}(\triangle)\) \(\oplus (\Box p \to \Box \triangle p) \oplus (\Box p \to \triangle \Box p) \oplus (\neg \Box p \to \triangle \neg \Box p)\) |
? | ? | ? | ? |
| \(\mathbf{IL}\) | ? | \(\checkmark\) Horvat, Sierra Miranda, and Studer (2025+) New! |
? | \(\checkmark\) Areces, Hoogland, and de Jongh (2001) |
| \(\mathbf{ILP}\) | ? | \(\checkmark\) Horvat, Sierra Miranda, and Studer (2025+) New! |
? | \(\checkmark\) Hájek (1992) Areces, Hoogland, and de Jongh (2001) |
| \(\mathbf{ILM}\) | - | - | - | - Ignatiev Visser (1997) |
| \(\mathbf{ILW}\) | - | - | - | - Areces, Hoogland, and de Jongh (2001) |
| \(\mathbf{ILW}^*\) | - | - | - | - Visser (1997) |
| \(\mathbf{ILF}\) | ? | ? | ? | ? cf. Areces, Hoogland, and de Jongh (2001) |
| \(\mathbf{il}\) | ? | ? | ? | \(\checkmark\) de Rijke (1992) |
| \(\mathbf{ilp}\) | ? | ? | ? | \(\checkmark\) de Rijke (1992) |
| \(\mathbf{ilm}\) | ? | ? | ? | \(\checkmark\) de Rijke (1992) |
| \(\mathbf{IL}^-(\mathbf{J2}_+, \mathbf{J5})\) | ? | ? | ? | \(\checkmark\) Iwata, Kurahashi, and Okawa (2024) |
| \(\mathbf{CL}\) | - | - | - | - Iwata, Kurahashi, and Okawa (2024) |
| \(\mathbf{IL}^-\) | - | - | - | - Iwata, Kurahashi, and Okawa (2024) |
| \(\mathbf{IL}^-(\mathbf{P})\) | ? | ? | ? | \(\checkmark\) Iwata, Kurahashi, and Okawa (2024) |
| Logics | ULIP | UIP | LIP | CIP |
|---|---|---|---|---|
| \(\mathbf{iM}\) intuitionistic \(\mathbf{M}\) | \(\checkmark\) Akbar Tabatabai, Iemhoff, and Jalali (2022) | \(\checkmark\) | \(\checkmark\) | \(\checkmark\) |
| \(\mathbf{iK}\) intuitionistic \(\mathbf{K}\) | ? | \(\checkmark\) Iemhoff (2019) | ? | \(\checkmark\) |
| \(\mathbf{iKD}\) intuitionistic \(\mathbf{KD}\) | ? | \(\checkmark\) Iemhoff (2019) | ? | \(\checkmark\) |
| \(\mathbf{iK4}\) intuitionistic \(\mathbf{K4}\) | - | - van der Giessen (2022) | ? | ? |
| \(\mathbf{iKT}\) intuitionistic \(\mathbf{KT}\) | ? | ? | ? | \(\checkmark\) Czermak (1975) |
| \(\mathbf{iS4}\) intuitionistic \(\mathbf{S4}\) | - | - van der Giessen (2022) | \(\checkmark\) Boričić (1991) | \(\checkmark\) Czermak (1975) |
| \(\mathbf{iGL}\) intuitionistic \(\mathbf{GL}\) | ? | \(\checkmark\) van der Giessen, Menéndez Turata, and Sierra Miranda New! |
? | \(\checkmark\) van der Giessen and Iemhoff (2021) |
| \(\mathbf{iSL}\) \(\mathbf{iGL} \oplus (p \to \Box p)\) \(\mathbf{iK} \oplus ((\Box p \to p) \to p)\) |
? | \(\checkmark\) Férée, van der Giessen, van Gool, and Shillito (2024) | ? | \(\checkmark\) van der Giessen and Iemhoff (202?) |
| \(\mathbf{KM}\) \(\mathbf{iSL} \oplus (\Box p \to ((q \to p) \lor p))\) | ? | ? | ? | \(\checkmark\) Muravitsky (2014) |
| \(\mathbf{IEL}^-\) \(\mathbf{iK} \oplus p \to \Box p\) | ? | ? | ? | \(\checkmark\) Su and Sano (2019) |
| \(\mathbf{IEL}\) \(\mathbf{IEL} \oplus \Box p \to \neg \neg p\) | ? | ? | ? | \(\checkmark\) Su and Sano (2019) |
| \(\mathbf{PLL}\) \(\mathbf{iK} \oplus (p \to \Box p) \oplus (\Box \Box p \to \Box p) \oplus (\Box p \land \Box q \to \Box (p \land q))\) | ? | \(\checkmark\) Iemhoff (2024) | ? | \(\checkmark\) |
Modal Quantified Logics
| Logics | ULIP | UIP | LIP | CIP |
|---|---|---|---|---|
| \(\mathbf{QK}\) | - | - | \(\checkmark\) Maksimova (1982) | \(\checkmark\) |
| \(\mathbf{QK4}\) | - | - | \(\checkmark\) Maksimova (1982) | \(\checkmark\) |
| \(\mathbf{QT}\) | - | - | \(\checkmark\) Maksimova (1982) | \(\checkmark\) |
| \(\mathbf{QS4}\) | - | - | \(\checkmark\) Maksimova (1982) | \(\checkmark\) |
| \(\mathbf{QS4.1}\) | - | - | ? | \(\checkmark\) |
| \(\mathbf{QS4.2}\) | - | - | ? | \(\checkmark\) |
| \(\mathbf{QS4.1.2}\) | - | - | ? | \(\checkmark\) |
| \(\mathbf{QGL}\) | - | - | ? | ? An error in Leivant (1981) cf. Avron (1984) |
| \(\mathsf{QPL}(\mathbf{PA})\) | - | - | - | - Vardanyan cf. Boolos (1993) |
| \(\mathbf{NQGL}\) \(\mathbf{QGL} + \dfrac{\Box^{n+1} \bot \to A \quad (\forall n \in \omega)}{A}\) | - | - | - | - Iwata and Kurahashi (2020) |
| \(\mathbf{QS5}\) | - | - | - | - Fine (1979) |