(※ この記事は、DIGGLE社でランチ勉強会に使った内容をそのままアップしています)

注意1: 普段の業務にそのまま活かせるものではありません
注意2: 自分は型理論を専攻していたので、出てくる記号列を理解するのに苦しみませんでしたが、初めて見る方はかなり咀嚼が必要な可能性が高いです

シークエント計算とは?

命題論理や述語論理に対して使われる演繹手法の一つの形式化

命題論理や述語論理とは?

命題論理や述語論理は 命題の形式化

= 命題(命題式)を表す言語 x 意味

(今回は命題論理のみについて話します)

命題論理の命題式の定義

次の文法で生成できる文を命題式と定義する
(以下に現れる $\phi, \psi$ はそれぞれ命題式を表す)

式	対応する直感的な意味合い
A,B,C,...	任意の記号
$\phi \wedge \psi$	$\phi$ かつ $\psi$
$\phi \vee \psi$	$\phi$ または $\psi$
$\phi \rightarrow \psi$	$\phi$ ならば $\psi$
$\lnot \phi$	$\phi$ でない

※ 結合性や()に関する議論は関心外なので省略
※ 述語論理はここに∀と∃を追加して得られる

命題論理の"意味"

命題式だけだと、ただの文=記号列

「命題が満たされている(正しい,充足している)」とは何か？ = 意味

命題式には自由変数のように記号が現れる。
そこで、記号→{T,F}の関数(真理値割当という)が所与として与えられた時の意味を定義する必要がある。

**「命題が真理値割当Aのもとで"満たされている"」**とは次のように定義する

1. A(X)=T ならば X は満たされている
2. φとψが満たされている ならば φ∧ψ は満たされている
3. φとψの少なくとも一方が満たされている ならば φ∨ψ は満たされている
4. ¬φとψの少なくとも一方が満たされている ならば φ→ψ は満たされている (※ 後述)
5. φが満たされていない ならば ¬φ は満たされている

さらに、任意の真理値割当Aのもとで命題Pが満たされているとき、 「命題Pは恒真である」 と定義する。

命題の具体例

$A \rightarrow A$

AならばA (トートロジー)

$A \wedge (A \rightarrow B) \rightarrow B$

三段論法 (modus-ponens)

これらは、どんな真理値割当のもとでも満たされている恒真命題であることが愚直に場合分けすればわかる。

注意 A→B は消せる

$A \rightarrow B$ は $\lnot A \vee B$ と同じと見做される

「あなたが持っているものがりんごならば、それは赤い」
は、相手がみかんを持っていたとしても間違ったことは言っていないので**"正しい"(??)**

A→B	B=True	B=False
A=True	True	False
A=False	True	True

今一旦納得するための考え方:

AならばB
= (AであってかつBでない) ことは絶対ない
= ¬(A∧¬B)
= ¬A∨¬¬B
= ¬A∨B

まだ気になる人は含意、論理包含の解釈、古典論理などについて調べると、より沼にハマれる！

シークエント計算とは?

remind: 命題論理の演繹手法

シークエント という文
0個以上のシークエントから1つのシークエントへの置き換えのルール(推論規則)

から成る。

シークエントの定義

$\phi_1, \cdots, \phi_m, \psi_1, \cdots, \psi_n$ を命題とするとき

シークエントは

$\phi_1, \cdots, \phi_m \Rightarrow \psi_1, \cdots, \psi_n$

という文のことをいう。
= 命題の配列2個からなると思えばOK

シークエントの意味

シークエントもこのままではただの文なので、意味が必要

シークエント

$\phi_1, \cdots, \phi_m \Rightarrow \psi_1, \cdots, \psi_n$

が満たされるのは、命題

$\phi_1 \wedge \cdots \wedge \phi_m \rightarrow \psi_1 \vee \cdots \vee \psi_n$

が満たされる時、と定義する。
(左が全部満たされる時、右のいずれかが正しい)

注意1: 左が0個の場合は真、右が0個の場合は偽
注意2: ∧と∨が逆の非対称性に違和感があるが、対偶を取ると実はこれで対称なのがわかる

推論規則

推論規則 = 0個以上のシークエント(前提) x 1つのシークエント(帰結)

このサイトから定義を拝借

(φ,ψはシークエント、　Γ、Δ、Π、Σはシークエントの列)

シークエント計算による演繹

初期シークエント $\phi \Rightarrow \phi$ から、推論規則を使って演繹(ゴールのシークエントを構成)する。
推論規則適用を1ステップの演繹と考える。これを繰り返して前提なしのシークエントを構成できるとき、その命題は満たされていることが示せる

例(二重否定) φ -> ¬¬φ
1: φ => φ     (初期シークエント)
2: ¬φ, φ =>   (1: ¬左)
3: φ => ¬¬φ   (2: ¬右)
4: => φ → ¬¬φ (3: →右)

例(三段論法) φ ∧ (φ → ψ) → ψ
1: φ => φ              （初期シークエント）
2: ψ => ψ              （初期シークエント）
3: φ, φ → ψ => ψ       （１，２→左）
4: φ ∧ (φ → ψ), φ => ψ （3∧左）
5: φ, φ ∧ (φ → ψ) => ψ （4交換左）
6: φ ∧ (φ → ψ), φ ∧ (φ → ψ) => ψ    （5∧左）
7: φ ∧ (φ → ψ) => ψ    （6希釈左）
8: => φ ∧ (φ → ψ) → ψ  （7→右）

シークエント計算の理論の帰結

命題論理のシークエント計算では、ゴールの命題を構成できるか否かを決定(できる場合は作り方も含め)する有限の手続きが存在する (決定可能性)
- つまり、与えられた命題が満たされるか否かを決定するプログラムを書ける
述語論理(∀や∃がある論理)ではそのような手続きは作れない
- 作ることを試みても、正しい場合に停止して、正しくない場合に停止しないようなプログラムになる (半決定性)

どんなプログラム？

Rubyで実装してみた例

補足: 理論が包含していることのうち、省略したこと

推論規則自体が"正しい"規則なのかどうかの確認
プログラムの作り方の確認
プログラムの停止性の確認
プログラムの出力が"正しいこと"の確認
直観主義論理(排中律のない論理)の取り扱い方