- ENGLISH
- JAPANESE
様々な論理の補間性の状況
- 論理式 \(A\) に含まれる命題変数全体の集合を \(v(A)\) で表す．
- 論理式 \(A\) に positive に現れる命題変数全体の集合を \(v^+(A)\) で表す．
- 論理式 \(A\) に negative に現れる命題変数全体の集合を \(v^-(A)\) で表す．
- 論理 \(L\) が Craig 補間性 (CIP) を持つとは，任意の論理式 \(A, B\) について，\(L \vdash A \to B\) ならば，次の三条件を満たす論理式 \(C\) が存在することをいう：
- \(v(C) \subseteq v(A) \cap v(B)\)
- \(L \vdash A \to C\)
- \(L \vdash C \to B\).
- 論理 \(L\) が Lyndon 補間性 (LIP) を持つとは，任意の論理式 \(A, B\) について，\(L \vdash A \to B\) ならば，次の三条件を満たす論理式 \(C\) が存在することをいう：
- \(v^+(C) \subseteq v^+(A) \cap v^+(B)\) かつ \(v^-(C) \subseteq v^-(A) \cap v^-(B)\)
- \(L \vdash A \to C\)
- \(L \vdash C \to B\).
- 論理 \(L\) が 一様補間性 (UIP) を持つとは，任意の論理式 \(A\) と命題変数の有限集合 \(P\) について，次の三条件を満たす論理式 \(C\) が存在することをいう：
- \(v(C) \subseteq v(A) \setminus P\)
- \(L \vdash A \to C\)
- \(L \vdash A \to B\) かつ \(v(B) \cap P = \emptyset\) を満たす任意の論理式 \(B\) について \(L \vdash C \to B\).
- 論理 \(L\) が 一様 Lyndon 補間性 (ULIP) を持つとは，任意の論理式 \(A\) と命題変数の有限集合 \(P^+, P^-\) について，次の三条件を満たす論理式 \(C\) が存在することをいう：
- \(v^+(C) \subseteq v^+(A) \setminus P^+\) かつ \(v^-(C) \subseteq v^-(A) \setminus P^-\)
- \(L \vdash A \to C\)
- \(L \vdash A \to B\) かつ \(v^+(B) \cap P^+ = \emptyset\) かつ \(v^-(B) \cap P^- = \emptyset\) を満たす任意の論理式 \(B\) について \(L \vdash C \to B\).
中間命題論理
CIP をもつ中間命題論理は次の7個だけ（Maksimova (1977)）．
| 論理 | 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) |
様相命題論理
サーベイ論文(Maksimova (1991))
直観主義様相命題論理
| 論理 | 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{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}\) | ✔ Tabatabai, Iemhoff, and Jalali (2021) | ✔ Pattinson (2013) | ✔ | ✔ |
| \(\mathbf{EC}\) \(\mathbf{E} + (\Box p \land \Box q \to \Box (p \land q))\) | × | × | × | × Tabatabai, Iemhoff, and Jalali (2021) |
| \(\mathbf{EN}\) \(\mathbf{E} + \dfrac{A}{\Box A}\) | ✔ Tabatabai, Iemhoff, and Jalali (2021) | ✔ | ✔ | ✔ |
| \(\mathbf{ECN}\) \(\mathbf{EC} + \dfrac{A}{\Box A}\) | × | × | × | × Tabatabai, Iemhoff, and Jalali (2021) |
| \(\mathbf{M}\) \(\mathbf{Cl} + \dfrac{A \to B}{\Box A \to \Box B}\) | ✔ Tabatabai, Iemhoff, and Jalali (2021) | ✔ Santocanale and Venema (2010) | ✔ | ✔ |
| \(\mathbf{MC}\) \(\mathbf{M} + (\Box p \land \Box q \to \Box (p \land q))\) | ✔ Tabatabai, Iemhoff, and Jalali (2021) | ✔ | ✔ | ✔ |
| \(\mathbf{MN}\) \(\mathbf{M} \oplus \dfrac{A}{\Box A}\) | ✔ 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)\) | × | × \(\mathbf{K4}\) より | ✔ 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) | ✔ |
CIP をもつ \(\mathbf{S4}\) の無矛盾正規拡大は 36 個以下（Maksimova (1979)）で30個は持つが残り6個は未解決．
CIP を持つ中間命題論理の modal companion のみを考えればよい．
\(\mathbf{Int}\) の modal companion
| 論理 | 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) |
\(\mathbf{KC}\) の modal companion
| 論理 | 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) |
\(\mathbf{LP}_2\) の modal companion
| 論理 | 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) |
\(\mathbf{LV}\) の modal companion
| 論理 | 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) |
\(\mathbf{LC}\) の modal companion は CIP を持たない（Maksimova (1982)）
\(\mathbf{LS}\) の modal companion
| 論理 | 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)\)1点 \(\leq\) 2点クラスター の論理 |
✔ local tabularity | ✔ local tabularity | ✔ Kurahashi (202?) New! |
✔ Maksimova (1980) |
| \(\mathbf{K3.2}\)\(\Gamma(\mathbf{LS}, 1, \omega)\) | × | ✔ local tabularity | × Kurahashi (202?) New! |
✔ Maksimova (1980) |
| \(\Gamma(\mathbf{LS}, 1, 2)\)2点クラスター \(\leq\) 1点 の論理 |
× | ✔ 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) |
\(\mathbf{Cl}\) の modal companion
| 論理 | 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)\)2点からなるクラスターの論理 | × | ✔ 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) |
証明可能性論理
| 論理 | 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)\) | ? | ✔ \(\mathbf{GL}\) の UIP から | ✔ 未発表 | ✔ 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: 各様相演算子 \([n]\) に対する \(\mathbf{GL}\) に次を加える：\(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) | ? 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}\) と順序公理 + \(\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}\) |
? 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}\) | ? | ? | ? | ✔ Areces, Hoogland, and de Jongh (2001) |
| \(\mathbf{ILP}\) | ? | ? | ? | ✔ 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}\) | ? | ? | ? | ? 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) |
| 論理 | ULIP | UIP | LIP | CIP |
|---|---|---|---|---|
| \(\mathbf{iM}\) 直観主義 \(\mathbf{M}\) | ✔ Tabatabai, Iemhoff, and Jalali (2022) | ✔ | ✔ | ✔ |
| \(\mathbf{iK}\) 直観主義 \(\mathbf{K}\) | ? | ✔ Iemhoff (2019) | ? | ✔ |
| \(\mathbf{iKD}\) 直観主義 \(\mathbf{KD}\) | ? | ✔ Iemhoff (2019) | ? | ✔ |
| \(\mathbf{iK4}\) 直観主義 \(\mathbf{K4}\) | × | × van der Giessen (2022) | ? | ? |
| \(\mathbf{iKT}\) 直観主義 \(\mathbf{KT}\) | ? | ? | ? | ✔ Czermak (1975) |
| \(\mathbf{iS4}\) 直観主義 \(\mathbf{S4}\) | × | × van der Giessen (2022) | ✔ Boričić (1991) | ✔ Czermak (1975) |
| \(\mathbf{iGL}\) 直観主義 \(\mathbf{GL}\) | ? | ? | ? | ✔ 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) | ? | ✔ |
様相述語論理
| 論理 | 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}\) | × | × | ? | ? Leivant (1981) の証明に誤りあり Avron (1984) 参照 |
| \(\mathsf{QPL}(\mathbf{PA})\) | × | × | × | × Vardanyan 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) |