LK の推論規則
出典: フリー百科事典『ウィキペディア（Wikipedia）』 (2019/11/21 02:32 UTC 版)
「シークエント計算」の記事における「LK の推論規則」の解説
ここでは、以下のような記法を用いる: 横線の上の論理式が与えられたとき、横線の下の論理式が推論によって導出されることを示す。 A {\displaystyle A} や B {\displaystyle B} は一階述語論理の論理式を表す（命題論理の論理式に限定する場合もある）。 Γ , Δ , Σ {\displaystyle \Gamma ,\Delta ,\Sigma } や Π {\displaystyle \Pi } は有限個（0個もありうる）の論理式の列であり、コンテキスト（文脈）と呼ぶ。 t {\displaystyle t} は任意の項を意味する。 A [ t / v ] {\displaystyle A[t/v]} は A {\displaystyle A} 内の変項 v {\displaystyle v} の全ての自由出現を項 t {\displaystyle t} で置換した論理式を表すが、 t , v , A {\displaystyle t,v,A} は「 t {\displaystyle t} 内のいかなる変項のいかなる自由出現もこの置換によって新たに束縛されない」という（代入可能）条件を満たすものとする。たとえば、 ∀ x ( p ( x , v ) ) {\displaystyle \forall x(p(x,v))} （ p {\displaystyle p} は 2 項述語、 x , v {\displaystyle x,v} は異なる変項）の v {\displaystyle v} の自由出現を x {\displaystyle x} で置換することは許されない。 x {\displaystyle x} や y {\displaystyle y} は（同じでもよい）変項を表す。 量化子 ∀ {\displaystyle \forall } や ∃ {\displaystyle \exists } で束縛されない変項を自由変項と呼ぶ。 W L {\displaystyle WL} は Weakening Left、 W R {\displaystyle WR} は Weakening Right、 C L {\displaystyle CL} と C R {\displaystyle CR} は Contraction、 P L {\displaystyle PL} と P R {\displaystyle PR} は Permutation の略である。 公理:カット: A ⊢ A ( I ) {\displaystyle {\cfrac {\qquad }{A\vdash A}}\quad (I)} Γ ⊢ Δ , A A , Σ ⊢ Π Γ , Σ ⊢ Δ , Π ( C u t ) {\displaystyle {\cfrac {\Gamma \vdash \Delta ,A\qquad A,\Sigma \vdash \Pi }{\Gamma ,\Sigma \vdash \Delta ,\Pi }}\quad ({\mathit {Cut}})} 左論理規則:右論理規則: Γ , A ⊢ Δ Γ , A ∧ B ⊢ Δ ( ∧ L 1 ) {\displaystyle {\cfrac {\Gamma ,A\vdash \Delta }{\Gamma ,A\land B\vdash \Delta }}\quad ({\land }L_{1})} Γ ⊢ A , Δ Γ ⊢ A ∨ B , Δ ( ∨ R 1 ) {\displaystyle {\cfrac {\Gamma \vdash A,\Delta }{\Gamma \vdash A\lor B,\Delta }}\quad ({\lor }R_{1})} Γ , B ⊢ Δ Γ , A ∧ B ⊢ Δ ( ∧ L 2 ) {\displaystyle {\cfrac {\Gamma ,B\vdash \Delta }{\Gamma ,A\land B\vdash \Delta }}\quad ({\land }L_{2})} Γ ⊢ B , Δ Γ ⊢ A ∨ B , Δ ( ∨ R 2 ) {\displaystyle {\cfrac {\Gamma \vdash B,\Delta }{\Gamma \vdash A\lor B,\Delta }}\quad ({\lor }R_{2})} Γ , A ⊢ Δ Σ , B ⊢ Π Γ , Σ , A ∨ B ⊢ Δ , Π ( ∨ L ) {\displaystyle {\cfrac {\Gamma ,A\vdash \Delta \qquad \Sigma ,B\vdash \Pi }{\Gamma ,\Sigma ,A\lor B\vdash \Delta ,\Pi }}\quad ({\lor }L)} Γ ⊢ A , Δ Σ ⊢ B , Π Γ , Σ ⊢ A ∧ B , Δ , Π ( ∧ R ) {\displaystyle {\cfrac {\Gamma \vdash A,\Delta \qquad \Sigma \vdash B,\Pi }{\Gamma ,\Sigma \vdash A\land B,\Delta ,\Pi }}\quad ({\land }R)} Γ ⊢ A , Δ Σ , B ⊢ Π Γ , Σ , A → B ⊢ Δ , Π ( → L ) {\displaystyle {\cfrac {\Gamma \vdash A,\Delta \qquad \Sigma ,B\vdash \Pi }{\Gamma ,\Sigma ,A\rightarrow B\vdash \Delta ,\Pi }}\quad ({\rightarrow }L)} Γ , A ⊢ B , Δ Γ ⊢ A → B , Δ ( → R ) {\displaystyle {\cfrac {\Gamma ,A\vdash B,\Delta }{\Gamma \vdash A\rightarrow B,\Delta }}\quad ({\rightarrow }R)} Γ ⊢ A , Δ Γ , ¬ A ⊢ Δ ( ¬ L ) {\displaystyle {\cfrac {\Gamma \vdash A,\Delta }{\Gamma ,\lnot A\vdash \Delta }}\quad ({\lnot }L)} Γ , A ⊢ Δ Γ ⊢ ¬ A , Δ ( ¬ R ) {\displaystyle {\cfrac {\Gamma ,A\vdash \Delta }{\Gamma \vdash \lnot A,\Delta }}\quad ({\lnot }R)} Γ , A [ t / x ] ⊢ Δ Γ , ∀ x A ⊢ Δ ( ∀ L ) {\displaystyle {\cfrac {\Gamma ,A[t/x]\vdash \Delta }{\Gamma ,\forall xA\vdash \Delta }}\quad ({\forall }L)} Γ ⊢ A [ y / x ] , Δ Γ ⊢ ∀ x A , Δ ( ∀ R ) {\displaystyle {\cfrac {\Gamma \vdash A[y/x],\Delta }{\Gamma \vdash \forall xA,\Delta }}\quad ({\forall }R)} Γ , A [ y / x ] ⊢ Δ Γ , ∃ x A ⊢ Δ ( ∃ L ) {\displaystyle {\cfrac {\Gamma ,A[y/x]\vdash \Delta }{\Gamma ,\exists xA\vdash \Delta }}\quad ({\exists }L)} Γ ⊢ A [ t / x ] , Δ Γ ⊢ ∃ x A , Δ ( ∃ R ) {\displaystyle {\cfrac {\Gamma \vdash A[t/x],\Delta }{\Gamma \vdash \exists xA,\Delta }}\quad ({\exists }R)} Γ ⊢ Δ Γ , A ⊢ Δ ( W L ) {\displaystyle {\cfrac {\Gamma \vdash \Delta }{\Gamma ,A\vdash \Delta }}\quad ({\mathit {WL}})} Γ ⊢ Δ Γ ⊢ A , Δ ( W R ) {\displaystyle {\cfrac {\Gamma \vdash \Delta }{\Gamma \vdash A,\Delta }}\quad ({\mathit {WR}})} Γ , A , A ⊢ Δ Γ , A ⊢ Δ ( C L ) {\displaystyle {\cfrac {\Gamma ,A,A\vdash \Delta }{\Gamma ,A\vdash \Delta }}\quad ({\mathit {CL}})} Γ ⊢ A , A , Δ Γ ⊢ A , Δ ( C R ) {\displaystyle {\cfrac {\Gamma \vdash A,A,\Delta }{\Gamma \vdash A,\Delta }}\quad ({\mathit {CR}})} Γ 1 , A , B , Γ 2 ⊢ Δ Γ 1 , B , A , Γ 2 ⊢ Δ ( P L ) {\displaystyle {\cfrac {\Gamma _{1},A,B,\Gamma _{2}\vdash \Delta }{\Gamma _{1},B,A,\Gamma _{2}\vdash \Delta }}\quad ({\mathit {PL}})} Γ ⊢ Δ 1 , A , B , Δ 2 Γ ⊢ Δ 1 , B , A , Δ 2 ( P R ) {\displaystyle {\cfrac {\Gamma \vdash \Delta _{1},A,B,\Delta _{2}}{\Gamma \vdash \Delta _{1},B,A,\Delta _{2}}}\quad ({\mathit {PR}})} 制約: (∃L) と (∀R) の規則において、変項 y {\displaystyle y} は Γ , ∃ x A , Δ {\displaystyle \Gamma ,\exists xA,\Delta } と Γ , ∀ x A , Δ {\displaystyle \Gamma ,\forall xA,\Delta } に自由出現をもたない。 なお、(∃L) と (∀R) の規則、および、制約は次を採用してもよい。 Γ , A ⊢ Δ Γ , ∃ x A ⊢ Δ ( ∃ L ) {\displaystyle {\cfrac {\Gamma ,A\vdash \Delta }{\Gamma ,\exists xA\vdash \Delta }}\quad ({\exists }L)} Γ ⊢ A , Δ Γ ⊢ ∀ x A , Δ ( ∀ R ) {\displaystyle {\cfrac {\Gamma \vdash A,\Delta }{\Gamma \vdash \forall xA,\Delta }}\quad ({\forall }R)} 制約: (∃L) と (∀R) の規則において、変項 x {\displaystyle x} は Γ , Δ {\displaystyle \Gamma ,\Delta } に自由出現をもたない。
※この「LK の推論規則」の解説は、「シークエント計算」の解説の一部です。
「LK の推論規則」を含む「シークエント計算」の記事については、「シークエント計算」の概要を参照ください。
- LK の推論規則のページへのリンク
