- 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}\) | ✔ Kurahashi (202?) New! |
✔ Pitts (1992) | ✔ Maksimova (1982) | ✔ Schütte (1962) |
| \(\mathbf{KC}\)\(\mathbf{Int} + (\neg p \lor \neg \neg p)\) | ✔ Kurahashi (202?) New! |
✔ Maksimova (2014) | ✔ Maksimova (1982) | ✔ Gabbay (1971) |
| \(\mathbf{LP}_2\)\(\mathbf{Int} + (p \lor (p \to q \lor \neg q))\) | ✔ local tabularity | ✔ local tabularity | ✔ Shimura (1992) | ✔ Maksimova (1977) |
| \(\mathbf{LV}\)\(\mathbf{LP}_2 + (p \to q) \lor (q \to p) \lor (p \leftrightarrow \neg q)\) | ✔ local tabularity | ✔ local tabularity | ✔ Kurahashi (202?) New! |
✔ Maksimova (1977) |
| \(\mathbf{LC}\)\(\mathbf{Int} + (p \to q) \lor (q \to p)\) | ✔ local tabularity | ✔ local tabularity | ✔ Kuznets and Lellmann (2018) | ✔ Maksimova (1977) |
| \(\mathbf{LS}, \mathbf{LC}_2\)\(\mathbf{LP}_2 + (p \to q) \lor (q \to p)\) | ✔ local tabularity | ✔ local tabularity | ✔ Maksimova (1982) | ✔ Maksimova (1977) |
| \(\mathbf{Cl}\), \(\mathbf{CPC}\)\(\mathbf{Int} + (p \lor \neg p)\) \(\mathbf{Int} + (\neg \neg p \to p)\) |
✔ local tabularity | ✔ local tabularity | ✔ Lyndon (1959) | ✔ 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) \) | ✔ Sato (202?) New! |
✔ | ✔ | ✔ |
| \(\mathbf{N}^+\mathbf{A}_{m, n}\) \((\mathbf{N} + \dfrac{\neg \Box A}{\neg \Box \Box A}) \oplus (\Box^n p \to \Box^m p) \) | ✔ Sato (202?) New! |
✔ | ✔ | ✔ |
| \(\mathbf{NRA}_{m, n}\) \(\mathbf{NR}\oplus (\Box^n p \to \Box^m p) \) | ✔ Sato (202?) New! |
✔ | ✔ | ✔ |
| \(\mathbf{E}\) \(\mathbf{Cl} + \dfrac{A \leftrightarrow B}{\Box A \leftrightarrow \Box B}\) | ✔ Akbar Tabatabai, Iemhoff, and Jalali (2021) | ✔ Pattinson (2013) | ✔ | ✔ |
| \(\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}\) | ✔ Akbar Tabatabai, Iemhoff, and Jalali (2021) | ✔ | ✔ | ✔ |
| \(\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}\) | ✔ Akbar Tabatabai, Iemhoff, and Jalali (2021) | ✔ Santocanale and Venema (2010) | ✔ | ✔ |
| \(\mathbf{MC}\) \(\mathbf{M} + (\Box p \land \Box q \to \Box (p \land q))\) | ✔ Akbar Tabatabai, Iemhoff, and Jalali (2021) | ✔ | ✔ | ✔ |
| \(\mathbf{MN}\) \(\mathbf{M} \oplus \dfrac{A}{\Box A}\) | ✔ Akbar Tabatabai, Iemhoff, and Jalali (2021) | ✔ | ✔ | ✔ |
| \(\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))\) |
✔ Kurahashi (2020) | ✔ Ghilardi (1995) Visser (1996) |
✔ Maksimova (1982) Fitting (1983) |
✔ Gabbay (1972) |
| \(\mathbf{KD}\)\(\mathbf{K} \oplus \neg \Box \bot\) \(\mathbf{K} \oplus (\Box p \to \Diamond p)\) |
✔ Kurahashi (2020) | ✔ Iemhoff (2019) | ✔ | ✔ Rautenberg (1983) |
| \(\mathbf{KT}\)\(\mathbf{K} \oplus (\Box p \to p)\) | ✔ Kurahashi (2020) | ✔ Bílková (2007) | ✔ Maksimova (1982) Fitting (1983) |
✔ Gabbay (1972) |
| \(\mathbf{KB}\)\(\mathbf{K} \oplus (p \to \Box \Diamond p)\) | ✔ Kurahashi (2020) | ✔ Kurahashi (2020) | ✔ Kuznets (2016) | ✔ |
| \(\mathbf{KDB}\)\(\mathbf{K} \oplus (\neg \Box \bot) \oplus (p \to \Box \Diamond p)\) | ✔ Kurahashi (2020) | ✔ Kurahashi (2020) | ✔ Kuznets (2016) | ✔ |
| \(\mathbf{KTB}\)\(\mathbf{K} \oplus (\Box p \to p) \oplus (p \to \Box \Diamond p)\) | ✔ Kurahashi (2020) | ✔ Kurahashi (2020) | ✔ Kuznets (2016) | ✔ Rautenberg (1983) |
| \(\mathbf{K4}\)\(\mathbf{K} \oplus (\Box p \to \Box \Box p)\) | × | × Bílková (2007) | ✔ Maksimova (1982) Fitting (1983) |
✔ Gabbay (1972) |
| \(\mathbf{K} \oplus (\Box p \to \Box^{n+1} p)\) | × | × | ✔ Kuznets (2016) | ✔ 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)\) | ✔ local tabularity Kurahashi (2020) |
✔ local tabularity Maksimova (2014) |
✔ Kuznets (2016) | ✔ |
| \(\mathbf{KD5}\)\(\mathbf{K} \oplus \neg \Box \bot \oplus (\Diamond p \to \Diamond \Box p)\) | ✔ local tabularity Kurahashi (2020) |
✔ local tabularity Maksimova (2014) |
✔ Kuznets (2016) | ✔ |
| \(\mathbf{K45}\)\(\mathbf{K} \oplus (\Box p \to \Box \Box p) \oplus (\Diamond p \to \Diamond \Box p)\) | ✔ local tabularity Kurahashi (2020) |
✔ local tabularity Maksimova (2014) |
✔ Kuznets (2016) | ✔ |
| \(\mathbf{KD45}\)\(\mathbf{K} \oplus \neg \Box \bot \oplus (\Box p \to \Box \Box p) \oplus (\Diamond p \to \Diamond \Box p)\) | ✔ local tabularity Kurahashi (2020) |
✔ local tabularity Maksimova (2014) |
✔ Kuznets (2016) | ✔ |
| \(\mathbf{KB5}\)\(\mathbf{K} \oplus (p \to \Box \Diamond p) \oplus (\Diamond p \to \Diamond \Box p)\) | ✔ local tabularity Kurahashi (2020) |
✔ local tabularity Maksimova (2014) |
✔ Kuznets (2016) | ✔ |
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) | ✔ Maksimova (1982) Fitting (1983) |
✔ 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))\) | ? | ? | ? | ✔ Maksimova (1987) |
| \(\Gamma(\mathbf{Int}, 2, \omega)\) | ? | ? | ? | ✔ Maksimova (1980) |
| \(\Gamma(\mathbf{Int}, 2, 2)\) | ? | ? | ? | ? |
| \(\Gamma(\mathbf{Int}, 2, 1)\) | ? | ? | ? | ✔ Maksimova (?) |
| \(\mathbf{S4.1}\)\(\Gamma(\mathbf{Int}, 1, \omega)\) \(\mathbf{S4} \oplus (\Box \Diamond p \to \Diamond \Box p)\) |
? | ? | ✔ Maksimova (1982) | ✔ 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)\) |
✔ Kurahashi (2020) | ✔ Visser (1996) | ✔ Maksimova (2014) | ✔ 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)\) |
? | ? | ✔ Kuznets (2016) | ✔ 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))\) | ? | ? | ? | ✔ Maksimova (1987) |
| \(\Gamma(\mathbf{KC}, 2, \omega)\) | ? | ? | ? | ✔ Maksimova (1980) |
| \(\Gamma(\mathbf{KC}, 2, 2)\) | ? | ? | ? | ? |
| \(\Gamma(\mathbf{KC}, 2, 1)\) | ? | ? | ? | ✔ Maksimova (?) |
| \(\mathbf{S4.2.1}\)\(\Gamma(\mathbf{KC}, 1, \omega)\) \(\mathbf{S4} \oplus (\Box \Diamond p \leftrightarrow \Diamond \Box p)\) |
? | ? | ✔ Maksimova (1982) | ✔ 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)\) |
✔ Kurahashi (202?) New! |
✔ Maksimova (2014) | ✔ Maksimova (2014) | ✔ 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)\) |
✔ local tabularity | ✔ local tabularity | ✔ Shimura (1992) | ✔ Schumm (1976) |
| \(\Gamma(\mathbf{LP}_2, 2, 1)\) | ✔ local tabularity | ✔ local tabularity | ✔ Kurahashi (202?) New! |
✔ Maksimova (1980) |
| \(\Gamma(\mathbf{LP}_2, 1, \omega)\) | × | ✔ local tabularity | × Kurahashi (202?) New! |
✔ Maksimova (1980) |
| \(\Gamma(\mathbf{LP}_2, 1, 2)\) | × | ✔ local tabularity | × Maksimova (1982) | ✔ Maksimova (1980) |
| \(\mathbf{GW}\)\(\Gamma(\mathbf{LP}_2, 1, 1)\) \(\mathbf{Grz} \oplus (\neg p \to \Box(p \to \Box p))\) |
✔ local tabularity | ✔ local tabularity | ✔ Shimura (1992) | ✔ Schumm (1976) |
Modal Companions of \(\mathbf{LV}\)
| Logics | ULIP | UIP | LIP | CIP |
|---|---|---|---|---|
| \(\Gamma(\mathbf{LV}, \omega, 1)\) | ✔ local tabularity | ✔ local tabularity | ✔ Kurahashi (202?) New! |
✔ Maksimova (1980) |
| \(\Gamma(\mathbf{LV}, 2, 1)\) | ✔ local tabularity | ✔ local tabularity | ✔ Kurahashi (202?) New! |
✔ Maksimova (1980) |
| \(\Gamma(\mathbf{LV}, 1, \omega)\) | × | ✔ local tabularity | × Kurahashi (202?) New! |
✔ Maksimova (1980) |
| \(\Gamma(\mathbf{LV}, 1, 2)\) | × | ✔ local tabularity | × Maksimova (1982) | ✔ 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))\) |
✔ local tabularity | ✔ local tabularity Maksimova (2014) |
✔ Kurahashi (202?) New! |
✔ 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)\) |
✔ local tabularity | ✔ local tabularity | ✔ Shimura (1992) | ✔ Schumm (1976) |
| \(\Gamma(\mathbf{LS}, 2, 1)\) | ✔ local tabularity | ✔ local tabularity | ✔ Kurahashi (202?) New! |
✔ Maksimova (1980) |
| \(\Gamma(\mathbf{LS}, 1, \omega)\) | × | ✔ local tabularity | × Kurahashi (202?) New! |
✔ Maksimova (1980) |
| \(\Gamma(\mathbf{LS}, 1, 2)\) | × | ✔ local tabularity | × Maksimova (1982) | ✔ Maksimova (1980) |
| \(\mathbf{GW.2}\)\(\Gamma(\mathbf{LS}, 1, 1)\) \(\mathbf{GW} \oplus (\Diamond \Box p \to \Box \Diamond p)\) |
✔ local tabularity | ✔ local tabularity Maksimova (2014) |
✔ Maksimova (1982) | ✔ 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)\) |
✔ local tabularity Kurahashi (2020) |
✔ local tabularity | ✔ Fitting (1983) | ✔ Schumm (1976) |
| \(\Gamma(\mathbf{Cl}, 2, 0)\) | × | ✔ local tabularity | × Maksimova (1982) | ✔ Maksimova (1980) |
| \(\mathbf{Triv}\)\(\Gamma(\mathbf{Cl}, 1, 0)\) \(\mathbf{K} \oplus (p \leftrightarrow \Box p)\) |
✔ local tabularity | ✔ local tabularity Maksimova (2014) |
✔ Maksimova (1982) | ✔ Maksimova (1980) |
Provability Logics
| Logics | ULIP | UIP | LIP | CIP |
|---|---|---|---|---|
| \(\mathbf{GL}\)\(\mathbf{K} \oplus (\Box(\Box p \to p) \to \Box p)\) | ✔ Kurahashi (2020) | ✔ Shavrukov (1993) Visser (1996) |
✔ Shamkanov (2011) | ✔ Smoryński (1978) Boolos (1979) |
| \(\mathbf{S}\)\(\mathbf{GL} + (\Box(\Box p \to p) \to \Box p)\) | ? | ✔ | ✔ | ✔ 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) | ✔ Shamkanov (2011) | ✔ |
| \(\mathbf{GLP}\)Polymodal: \(\mathbf{I} \oplus ([m]p \to [n] p)\) for \(m \leq n\) | ? | ✔ Shamkanov (2011) | ? cf. Shamkanov (2011) |
✔ Ignatiev (1993) Beklemishev (2010) |
| \(\mathbf{wGL}_n\)\(\mathbf{K} \oplus (\Box (\Box^n p \to p) \to \Box p)\) | ? | ? | ✔ Iwata (2021) | ✔ 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?) |
✔ Kogure and Kurahashi (202?) New! |
✔ Kogure and Kurahashi (202?) New! |
✔ 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}\) | ? | ✔ Horvat, Sierra Miranda, and Studer New! |
? | ✔ Areces, Hoogland, and de Jongh (2001) |
| \(\mathbf{ILP}\) | ? | ✔ Horvat, Sierra Miranda, and Studer New! |
? | ✔ 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}\) | ? | ? | ? | ✔ de Rijke (1992) |
| \(\mathbf{ilp}\) | ? | ? | ? | ✔ de Rijke (1992) |
| \(\mathbf{ilm}\) | ? | ? | ? | ✔ de Rijke (1992) |
| \(\mathbf{IL}^-(\mathbf{J2}_+, \mathbf{J5})\) | ? | ? | ? | ✔ Iwata, Kurahashi, and Okawa (2024) |
| \(\mathbf{CL}\) | × | × | × | × Iwata, Kurahashi, and Okawa (2024) |
| \(\mathbf{IL}^-\) | × | × | × | × Iwata, Kurahashi, and Okawa (2024) |
| \(\mathbf{IL}^-(\mathbf{P})\) | ? | ? | ? | ✔ Iwata, Kurahashi, and Okawa (2024) |
| Logics | ULIP | UIP | LIP | CIP |
|---|---|---|---|---|
| \(\mathbf{iM}\) intuitionistic \(\mathbf{M}\) | ✔ Akbar Tabatabai, Iemhoff, and Jalali (2022) | ✔ | ✔ | ✔ |
| \(\mathbf{iK}\) intuitionistic \(\mathbf{K}\) | ? | ✔ Iemhoff (2019) | ? | ✔ |
| \(\mathbf{iKD}\) intuitionistic \(\mathbf{KD}\) | ? | ✔ Iemhoff (2019) | ? | ✔ |
| \(\mathbf{iK4}\) intuitionistic \(\mathbf{K4}\) | × | × van der Giessen (2022) | ? | ? |
| \(\mathbf{iKT}\) intuitionistic \(\mathbf{KT}\) | ? | ? | ? | ✔ Czermak (1975) |
| \(\mathbf{iS4}\) intuitionistic \(\mathbf{S4}\) | × | × van der Giessen (2022) | ✔ Boričić (1991) | ✔ Czermak (1975) |
| \(\mathbf{iGL}\) intuitionistic \(\mathbf{GL}\) | ? | ✔ van der Giessen, Menéndez Turata, and Sierra Miranda New! |
? | ✔ van der Giessen and Iemhoff (2021) |
| \(\mathbf{iSL}\) \(\mathbf{iGL} \oplus (p \to \Box p)\) \(\mathbf{iK} \oplus ((\Box p \to p) \to p)\) |
? | ✔ Litak and Visser (202?) | ? | ✔ van der Giessen and Iemhoff (202?) |
| \(\mathbf{KM}\) \(\mathbf{iSL} \oplus (\Box p \to ((q \to p) \lor p))\) | ? | ? | ? | ✔ Muravitsky (2014) |
| \(\mathbf{IEL}^-\) \(\mathbf{iK} \oplus p \to \Box p\) | ? | ? | ? | ✔ Su and Sano (2019) |
| \(\mathbf{IEL}\) \(\mathbf{IEL} \oplus \Box p \to \neg \neg p\) | ? | ? | ? | ✔ 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))\) | ? | ✔ Iemhoff (2024) | ? | ✔ |
Modal Quantified Logics
| Logics | ULIP | UIP | LIP | CIP |
|---|---|---|---|---|
| \(\mathbf{QK}\) | × | × | ✔ Maksimova (1982) | ✔ |
| \(\mathbf{QK4}\) | × | × | ✔ Maksimova (1982) | ✔ |
| \(\mathbf{QT}\) | × | × | ✔ Maksimova (1982) | ✔ |
| \(\mathbf{QS4}\) | × | × | ✔ Maksimova (1982) | ✔ |
| \(\mathbf{QS4.1}\) | × | × | ? | ✔ |
| \(\mathbf{QS4.2}\) | × | × | ? | ✔ |
| \(\mathbf{QS4.1.2}\) | × | × | ? | ✔ |
| \(\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) |