様相論理に関するトピックをまとめたノートを掲載しています。 様相論理を勉強するみなさんの一助となれば幸いです。 ファイルは公開順に並んでいますが、ある程度内容が充実したら並び順を変更しようと考えています。
様相論理では、Kripke フレームの性質と公理との対応関係が知られています （たとえば、反射性と公理 T など）。 しかしながら、様相論理の論理式では特徴づけられない二項関係の性質も存在します。 この稿では、フレームの非反射性をとりあげ、非反射的フレームのクラスを定義する 様相論理の論理式が存在しないことを示しています。
pdf ファイルはこちら 最終更新: 2024-11-12
様相論理のラベルつきタブロー計算を紹介し、その健全性と完全性を証明しています。 また、「タブロー計算の手続きが有限時間で停止する」（これを停止性と呼びます）という性質を証明しています。 これらの結果の系として、様相論理 \( \mathbf{K} \) が決定可能になることが示せます。
pdf ファイルはこちら 最終更新: 2024-11-21
Negri (2005) によって導入された様相論理のラベルつきシークエント計算を紹介します。 その後、健全性と完全性、ならびにカット許容定理を証明します。
この体系にいくつかの規則を付け加えることで、 \( \mathbf{S4}, \mathbf{S5} \) に対応するシークエント計算をつくることができ、 さらにそれらのカット除去を一気に証明することができます。 それについては追って続編を書こうと考えています。
pdf ファイルはこちら 最終更新: 2024-11-21
誤植や議論の間違いなどがありましたら、お手数ですが Home の「連絡先」からお伝えいただければと思います。