第6章 シークェント計算

数理論理学

6.1 シークェント

定義
A1,A2,...,An ⇒ B1,B2,...,Bm
論理式の多重集合同士の関係
解釈Iに対して、I |= A1,A2,...,An ⇒ B1,B2,...,Bm (Iはシークェントを満たす）
iff
あるiが存在してI［[Ai]］=falseまたはあるjが存在してI［[Aj]］=true
iff
I |= A1,A2,...,An ⊃ B1,B2,...,Bm

  • 左辺と右辺に共通の論理式のあるシークェントは恒真である。
  • 空シークェントは充足不能である（i,jが存在しないから）

6.2 シークェント計算

シークェントが恒真であることの証明

公理シークェント

Γ∩Δ≠0であるとき、シークェントΓ⇒Δを公理シークェントという。
理由：左辺と右辺に共通の要素があればそのシークェントは恒真だから

推論規則

結合子規則8つ、限量子規則4つ
対称になっているところが結構あるので覚えやすいかもしれない。

  • 否定規則（左右）　¬
  • 連言規則（左右）　∧
  • 選言規則（左右）　∨
  • 含意規則（左右）　⊃
  • ∀規則（左右）
  • ∃規則（左右）
    • どこにアイゲンバリアブル条件が適用されるかは注意が必要

6.3 証明木

自然演繹の時とほとんど同じ
下からやると良い。どういう順番でやるかは自由っぽい。
でもアイゲンバリアブル条件には注意

導出木

証明木になってない木のこと

  1. 終了してない（まだ推論規則が適用できる可能性がある）
  2. 終了していてもすべての葉が公理シークェントになっていない
  3. 無限の導出木（証明木は有限である）

葉のない導出木は終了しているという