様相論理一般 - Researchmap

様相論理一般
村上祐子
東北大学
様相論理
• 様相演算子を持つ論理
• 様相演算子：真理値表では解釈できない（こ
とがある）命題演算子
2012/11/20
CAPE上級論理学セミナー
2
様相演算子を適用したくなる例
•
•
•
•
•
•
そんなことはない。
そんなことは不可能だ。
昨日雨が降った。
次の場面では佐藤がコーヒーを飲んでいる。
先手必勝の局面だ。
宿題が終わったらおやつにしよう。
2012/11/20
CAPE上級論理学セミナー
3
先手必勝の局面だ
• 後手がどんな手を打っても、先手には適切な
応手があって、そこでも先手必勝である。
• 「先手勝ち」状態に必ず到達できる（必至）
• Cf.ゲーム意味論、記述集合論
2012/11/20
CAPE上級論理学セミナー
4
様相の文脈性
• 局面ごとに命題を評価する
• この局面では成り立っていることが、他の局
面では成立しないかもしれない
• 次の（ありうる）局面を俯瞰する必要がある
– ある事態が成立する局面に到達するにはどの手
を打ったらいいのか？
2012/11/20
CAPE上級論理学セミナー
5
クリプキ意味論
• がさつな考え方：局面間の到達可能性関係を
考える
• ところで局面って何？
2012/11/20
CAPE上級論理学セミナー
6
局面
• 二つの要素からなっている
– 前の評価点と後ろの評価点との関係からなる構
造
– その評価点での世界のあり方
• 個別の局面で文の真理値が割り当てられている
2012/11/20
CAPE上級論理学セミナー
7
様相文
• 手はじめに1項の様相演算子□を持つ言語を
考え、その解釈をみる。
• 言語：
– Prop: 命題記号
– ∧：2項命題演算子
– ￢、□：1項命題演算子
• 文
– p| p ∧q| ￢p|□p
• 省略記号：→、∨、◇
2012/11/20
CAPE上級論理学セミナー
8
クリプキフレーム
• 評価点間の構造にだけ着目
– 評価点の（空でない）集合 W
– 評価点の2項関係 R
• <W,R>
2012/11/20
CAPE上級論理学セミナー
9
フレームだけではなにもいえない
• 個別の評価点における世界の有り様の記述
– 命題記号に真理値を割り当てる
• 付値関数
– クリプキフレームF=<W,R>上の付値関数とは、関
数 Prop×W→TruthValue である。
– (TruthValueとして当面のところ2値{1,0}を考える)
2012/11/20
CAPE上級論理学セミナー
10
クリプキモデル
• F: クリプキフレーム<W,R>
• v: F上の付値関数
のとき<F,v>=<W,R,v>をF上のクリプキモデルとい
う。
2012/11/20
CAPE上級論理学セミナー
11
クリプキモデルでの様相言語解釈
•
•
•
•
w |= p iff v(p,w)=1
w |= A∧B iff w |= A かつw |= B
w |= ￢A iff w |= A でない
w |= □A iff Rwxであるすべてのxで x |= A
お絵かきタイム
2012/11/20
CAPE上級論理学セミナー
12
モデル妥当性とフレーム妥当性
• クリプキモデルM=<W,R,v>で文Ａが妥当であ
るとは、Wのすべての元wで w |= Aのときに
いう。
• クリプキフレームFで文Ａが妥当であるとは、F
上のすべてのクリプキモデルで文Ａが妥当で
あるときにいう。
2012/11/20
CAPE上級論理学セミナー
13
三重の妥当性
• 付値関数はまだローカルな文脈相当。
• 構造も文脈のうち。
• 「論理」は文脈に依存しない。
– （変換に対して不変）
– 評価点の間の構造が論理に相当する。
• フレームのあつまり（一般にクラスになる）を
考える必要がある
2012/11/20
CAPE上級論理学セミナー
14
フレームのクラスでの妥当性
• C:フレームのクラス
• Cで妥当 iff Cのすべてのフレームで妥当
• Cで妥当な文のすべてからなる集合をこれか
ら考える。
2012/11/20
CAPE上級論理学セミナー
15
論理体系
• （様相）論理体系：様相文の集合で、
– AとBが入っていたら、A∧Bが入っている（連言に
ついて閉じている）。
– 命題論理について閉じている
• 例：クリプキフレームのクラスＣで妥当な文のすべてか
らなる集合は論理体系になっている。
• 矛盾した論理体系：Aと￢Aの両方が入ってい
る体系。
2012/11/20
CAPE上級論理学セミナー
16
論理体系と公理系
• 公理系：論理式と推論規則のセット
• 論理体系が公理系を持つとは、その公理系で演
繹可能な文と論理体系が一致すること。
• 論理体系が（有限）公理化可能とは、有限個の
論理式スキームと推論規則からなる公理系を持
つこと。
• 自明な公理系（論理体系そのまんま）はつねに
存在する
• 公理系と論理体系を同一視することがある
2012/11/20
CAPE上級論理学セミナー
17
論理体系と意味論
• ある意味論で妥当な式の集合と与えられた論理
体系を比べる
• 一致していれば「完全」という
• 完全性証明でやること
1. 証明可能な式の妥当性を示す
2. 証明できない式が妥当ではないことを示す＝そ
の否定である整合的な式がモデルを持つことを
示す
2012/11/20
CAPE上級論理学セミナー
18
クリプキフレーム全体のクラスと完全
な論理体系の公理系K
• 古典命題論理の公理と推論規則（MP）
• □（A→B） → （□A→ □B）
• [必然化規則]Aが定理ならば□Aも定理であ
る。
2012/11/20
CAPE上級論理学セミナー
19
フレーム全体のクラスの部分クラスC
• 問題：C妥当な文の集合は公理化可能か。
• 言い換えると、
AがC妥当 iff AはLの定理
• となるような論理体系Lは公理化可能か。
2012/11/20
CAPE上級論理学セミナー
20
Negative answer
• フレームのクラスならどれでも公理化可能と
いうわけではないし、公理系が対応するクラ
スを持たないこともある
• Cf.
– van Benthem
– Companion of modal logic
– Handbook of modal logic
2012/11/20
CAPE上級論理学セミナー
21
General frame（一般フレーム）
• 「受容可能世界」を導入
• F=<W,R>上のモデルM=<F,v>によって生成さ
れる一般フレームとは<F,N>のことである。
• ただしN=｛|A|Ｍ:Aは様相文｝
2012/11/20
CAPE上級論理学セミナー
22
脇道：近傍意味論(Segerberg)
• 到達可能性ではなく、近傍を考える
• wの近傍:Wの部分集合
• N(w):wの近傍からなる集合
• w |=A iff |A|∈N(w)
（|A|:Aが真であるWの元の集合）
2012/11/20
CAPE上級論理学セミナー
23
近傍意味論
• クラシカルな様相論理体系の意味論を与える
– A↔Bが定理ならば□A ↔ □Bも定理
• 近傍に条件を追加することでより強い論理の
意味論を作ることができる
– レギュラーな様相論理
• A → Bが定理ならば□A →□B
– Upward closed
• これが代数意味論における単調性に相当する
2012/11/20
CAPE上級論理学セミナー
24
一般フレームの受容可能世界
• 矛盾式については∅
• 定理についてはW
• その間の構造は？
• 当然のように整合的な式Aのモデルを構築で
きる（|A|はある意味あらかじめ一般フレーム
に含まれているので必ず反例を構成できる）
2012/11/20
CAPE上級論理学セミナー
25
受容可能世界の構造→（有界）束
• 受容可能世界だけ抜き出したような感じのも
のが代数意味論
• 代数意味論のメリット：
– （ちゃんとした構造を作れれば）必ず完全：自明す
ぎて誰もやらない
• どんな構造を作るかがポイント
2012/11/20
CAPE上級論理学セミナー
26

Download Report