シーケント計算

シーケント計算(sequent calculus)

ゲンツェンが形式化したもの

古典論理のシーケント計算と、直観主義論理のシーケントというものがある

古典論理のシーケント計算は「LK」 (エルカー)

直観主義論理のシーケント計算は「LJ」(エルヨット)

命題論理式$ A_i, B_i (または一階述語論理式)があったとき、

$ A_1, ..., A_m \vdash B_1,...,B_n の形について

この形式の記号列をシーケントと呼ぶ

読み方: $ A_1, ..., A_m から $ B_1,...,B_n が導出できる

⊢自体はターンスタイル

$ \vdash の左側を前件(antecedent)

$ \vdash の右側を後件(antecedent)

論理式の集合$ \Gamma = \omega_1,\omega_2,...,\omega_n 、論理式$ \varphi があったとき

$ \Gamma \vdash \varphi

読み方: $ \Gamma (ラージガンマ)から$ \varphi (ファイ)が導出できる

$ \frac{ A,A,Γ \vdash \Delta }{A, Γ \vdash \Delta}(\text{CL})

上が前提(premise)

右の$ (\text{CL}) 部分が推論規則

下が結論(conclusion)

縮約(Contraction)の推論規則

確認用

Q. シーケント計算

参考