直観主義様相論理K4の有限モデル性の証明

この論文をやさしく読む

ひとことで言うと

直観主義様相論理の一種 K4 に、有限のモデルで反例を調べられるという性質があることを証明した。

何に役立つ？

対象の論理体系のモデル理論や決定手続きの研究の基礎となる。要旨は数学的な証明の結果を述べる。

この研究の面白いところ

既存の Fine の選択法を直観主義様相論理へ広げ、それを有限モデル性の証明に使う。

どこまで分かった？

要旨で対象とされるのは Fischer Servi 型の直観主義 K4 であり、ほかの様相論理までの拡張は記載されていない。

v1のアブストラクトに基づくAI解説。日本語訳とは別に、用途の解釈を含みます。

アブストラクトの日本語訳

Fine の選択法を直観主義様相論理の設定へ拡張し、それを用いて、Fischer Servi 型の直観主義 K4 が有限モデル性を持つことを、モデル理論に基づいて証明する。

v1の要旨から自動生成。本文の精読・人による確認は未実施。