Hatena::Groupxn--272ax3f

論理と計算のしくみ 3.4

論理と計算のしくみ 3.4

プレゼンテーション

論理と計算のしくみ 3.4 命題直観主義論理

  • 直観主義論理 (intuitionistic logic): 排中律と背理法が成り立たない論理
  • 可能世界の考えを用いて意味論を与える

直観主義論理

  • 人間の知識を表していると考えることができる
  • 論理式の成立 = その世界の知識に含まれている
  • 知識は増加する; ある世界で真な論理式はそこから到達できるすべての世界でも真

構文論

  • 記号: \neg \vee \wedge \supset
    • 古典論理といっしょ
  • \wedge\supset を省略形として定義することはできない
    • cf. 古典論理において
      • A \wedge B := \neg(\neg A \vee \neg B)
      • A \supset B := \neg A \vee B
  • \neg の定義
    • \neg A := A \supset \bot

意味論

クリプキ構造 S = <W, R, V>

  • W は世界の集合
  • R は世界の間の到達可能性関係
    • W 上の半順序でなければならない
  • V は各世界における割り当て
    • V(w, P) = T かつ w R w' なら V(w', P) = T でなければならない

※制約は世界が人間の知識であるための要請

  • 知識は減らない
  • 知識同士を比較できるとは限らない

構造の例: 図 3.5

論理式の解釈

S,w |= A … 構造 S の世界 w で論理式 A が真

  •  S,w |= A \supset B iff wRw' を満たす任意の w' \in W に対して、 S,w' |= A ならば  S,w' |= B が成り立つ
    • 世界 w から到達可能なすべての世界を参照する必要がある
  •  \neg A \supset \bot だったので
    •  S,w |= \neg A iff wRw' を満たす任意の w' \in W に対して、 S,w' |= A が成り立たない

定理 3.5

任意の論理式 A に対して、S,w |= A が成り立ち、かつ wRw' なら S,w' |= A も成り立つ

  • "ある時点で知り得た知識はなくならない"
  • A が成り立つような世界の集合 \llbracket A \rrbracket = \{ w \in W | S,w |= A \} \subseteq W を真偽値と考えることができる
    • あとで触れます (がよくわかりません)

排中律、二重否定の除去が成立しない例

  • 2つの世界 W = \{0,1\}
  • P は 0 において \bot1 において \top
  • S,0 |= P は成り立たないが将来の知識では S,1 |= \neg P なので S,0 |= \neg P ともならない (排中律)
  • S,1 |= \neg P は成り立たず S,0 |= \neg P も成り立たないので S,0 |= \neg \neg P が成り立つが S,0 |= P は成り立たない (二重否定の除去)

最後の審判

  • そこから先に到達できる世界のない世界 w_f では排中律も二重否定の除去も成立する
  • S,w_f |= A \supset B の解釈において w_f のみ考慮するだけでいいから

選言に関する性質

定理 3.6

|= A \vee B ならば |= A または |= B が成り立つ。

証明: 対偶をとる。|= A|= B も成り立たないとして、|= A \vee B が成り立たないことを示す

直観主義論理の真偽値

  • 真偽値: 真偽の度合い
    • 古典論理においては 真・偽の 2 種類

命題直観主義論理においては \llbracket A \rrbracket = \{ w \in W | S,w |= A \} \subseteq W を真偽値と考えることができる

  • \llbracket A \rrbracket は上に閉じている: 関係 R でつながる要素はすべて含まれている
  • \llbracket A \wedge B \rrbracket = \llbracket A \rrbracket \cap \llbracket B \rrbracket
  • \llbracket A  \vee  B \rrbracket = \llbracket A \rrbracket \cup \llbracket B \rrbracket
  • \llbracket \bot \rrbracket       = \emptyset

\llbracket A \supset B \rrbracket = \llbracket A \rrbracket \supset \llbracket B \rrbracket

が成立するように  X \supset Y を定義してやる:

X \supset Y = { w \in W | 任意の w' \in W に対して wRw' かつ w' \in X なら w' \in Y }

  • X \supset Y は 「W の上に閉じた部分集合 ZX \cap Z \subseteq Y を満たすもののうち最大」になっている
    • ので W の上に閉じた部分集合の全体はハイティング代数をなす
  • 世界が一つしかない構造は古典論理に対応

シーケント計算

  • \bot を用いず、\neg は独立した論理記号とする
  • \rightarrow の右側の論理式の数を 0 個か 1 個に制限する
    • 理由がわかりません…
  • 健全かつ完全であることが知られているが本書の範囲外

証明手続き

  • 古典論理とちがい推論規則を適用する順番が意味を持つ
  • 適用の仕方は有限通りしかないので、与えられた論理式が恒真かどうかを決定可能ではある