S5模態邏輯

S5是Clarence Irving Lewis和Cooper Harold Langford在其1932年出版的“象徵邏輯”一書中提出的五種模態邏輯系統之一。 它是一種普通的模態邏輯，是任何類型的最古老的模態邏輯系統之一。 是最基本的模態邏輯，是由命題演算公式和重言式構成的，以及具有替換和模態推理的推理裝置。

基本介紹

• 中文名：S5模態邏輯
• 外文名：S5 (modal logic)

克里普克的語義

就Kripke語義而言，S5的特徵在於可訪問性關係是等價關係的模型：它是自反的，傳遞的和對稱的。

確定S5公式的可滿足性是NP完全問題。硬度證明是微不足道的，因為S5包括命題邏輯。通過證明任何可滿足的公式具有Kripke模型來證明成員資格，其中世界的數量在公式的大小上最多是線性的。

套用

S5很有用，因為它避免了不同種類的限定符的多餘疊代。例如，在S5下，如果X必然，可能，必然，可能是真的，那么X可能是真的。最終“可能”之前的無限制資格賽在S5中被修剪。雖然這對於保持命題合理地縮短是有用的，但也可能看起來反直覺，因為在S5下，如果可能需要某些東西，那么這是必要的。

Alvin Plantinga認為S5的這個特徵實際上並不違反直覺。為了證明這一點，他認為如果X可能是必要的，那么至少在一個可能的世界中是必要的;因此，在所有可能的世界中都是必要的，因此在所有可能的世界中都是如此。這種推理支持了本體論論證的“模態”表述。