시퀀트 계산

시퀀트 계산(sequent calculus)은 1차 논리나 특수한 명제 논리에서 쓰이는 연역 계산법의 일종으로, 논리식으로 이루어진 특수한 열인 시퀀트를 이용한다. 유사한 수법까지 총칭하여 겐첸 체계(Gentzen system)라고도 불리며, 다른 것들과 구분하기 위해 LK라 특별히 일컫기도 한다.

자연 연역과 유사하게 이미 제시된 식들로부터 추론 규칙에 근거한 추론을 행하여 새로운 식을 이끌어내는 방식이며, 이는 공리에 근거하여 정리들을 나열하는 방식의 증명법을 가진 힐베르트 체계(Hilbert System)와는 대비된다.

시퀀트(sequent)란 논리식의 나열인데, 전건의 명제들의 논리곱을 전제로 삼고 후건의 명제들의 논리합을 귀결로 삼는 것이 특징이다. 곧, "A이고 B이고 C이고 D이고... 이면, (가)이거나 (나)이거나 (다)이거나 (라)이거나...이다."와 같은 식이다. 시퀀트 계산에서 증명은 일련의 시퀀트들의 나열로 기술되는데, 각 시퀀트는 증명과정에서 이미 출현한 시퀀트에 특정 추론규칙을 적용하는 것으로써 도출된다.

시퀀트

시퀀트(영어: sequent)란 일반적인 형태의 논리식(조건절)들의 나열로, 표명(assertion) 방식의 일종이다. 전건의 명제들의 논리곱을 전제로 삼고 후건의 명제들의 논리합을 귀결로 삼는다.

\Gamma \vdash \Sigma

와 같이 쓰이며, 풀어서 다음과 같이 쓰면:

A_{1},\,\dots ,A_{m}\,\vdash \,B_{1},\,\dots ,B_{n}.

위 시퀀트에서 m개의 논리식 A_i는 전건(antecedents), n개의 논리식 B_j은 후건(succedents) 또는 귀결(consequents)로 불린다. 이 Γ와 Σ는 논리식의 열(列)이지 집합이 아니므로, 식들의 수와 순서가 유의미하다. 기호 $\vdash$ 는 턴스타일(turnstile) 또는 표명 기호(assertion symbol) 등으로 불리는데, "생산한다", "증명한다", "수반한다" 등의 의미로 해석될 수 있다. 직관적으로, Γ를 전제로 할 때 귀결이 되는 Σ를 증명가능하다고 말할 수 있게 된다.

특징적인 것은, 시퀀트에선 전건의 명제들의 논리곱이 전제가 되고 후건의 명제들의 논리합이 귀결이 된다. 즉 전건의 모든 논리식이 참일 때, 후건의 논리식 중 적어도 1개의 논리식도 참이라고 해석할 수 있다. 그러므로 전건이 공열(空列)일 경우 그 시퀀트는 항진이며, 곧 $\vdash \Sigma$ 라는 형식은 어떤 전제도 없이 Σ 가 성립하는 항진식을 의미한다. 한편 후건이 공열일 때 그 시퀀트는 거짓이라고 해석되며, 달리 말하면 $\Gamma \vdash$ 라는 형식은 Γ 가 거짓임을 증명하고 따라서 비일관적(inconsistent)임을 나타낼 수 있다.

시퀀트 계산

시퀀트 계산(sequent calculus)은 시퀀트를 이용한 형식적 연역 논증 수법의 일종이다. 이는 이미 제시된 조건적(무조건적에 대비되는) 항진식들로부터, 정해진 추론 규칙을 통해 또다른 조건적 항진식을 도출해나가는 방식이다.

LK 체계

아래에서는 게르하르트 겐첸에 의해 1934년 소개된 가장 일반적인 LK 체계의 추론규칙을 설명한다.

여기서는 아래와 같은 기법이 사용된다:

가로줄 위의 논리식이 주어진 것으로부터 가로줄 아래의 논리식이 도출됨을 나타낸다.
$\vdash$ (턴스타일)은 좌측에 '가정'과 우측에 '진술'을 두어 나눈다. 추론규칙 또한 좌측에 적용되는 규칙과 우측에 적용되는 규칙이 분별된다.
$A$ 와 $B$ 는 1차 술어 논리의 논리식들을 나타낸다. (명제논리에 한정하는 경우도 있다)
$\Gamma ,\Delta ,\Sigma ,\Pi$ $\Gamma ,\Delta ,\Sigma ,\Pi$ 는 유한 개(0개일 수도 있음)의 논리식의 열로, '문맥'(context)이라고 불린다.
- $\vdash$ 의 좌측에 위치한 논리식들끼리는 논리곱적으로 연결되어 있다고 여겨진다.
- $\vdash$ 의 우측에 위치한 논리식들끼리는 논리합적으로 연결되어 있다고 여겨진다.
$t$ 는 어떠한 임의의 항을 나타낸다.
$x$ 와 $y$ 는 변수를 나타낸다.
양화자 $\forall$ 나 $\exists$ 에 종속되어 있지 않은 변수를 자유변수라고 부른다.
$A[t]$ 는 항 $t$ 에 주목한 논리식 $A$ 를 나타낸다.
$A[s/t]$ 는 $A[t]$ 내의 특정한 $t$ 의 출현을 항 $s$ 로 치환한 논리식을 나타낸다.
$WL$ 와 $WR$ 는 Weakening Left/Right, $CL$ 와 $CR$ 는 Contraction, $PL$ 와 $PR$ 는 Permutation의 약자이다.

동일성의 공리:	자름 규칙:
${\cfrac {\qquad }{A\vdash A}}\quad (I)$	${\cfrac {\Gamma \vdash \Delta ,A\qquad A,\Sigma \vdash \Pi }{\Gamma ,\Sigma \vdash \Delta ,\Pi }}\quad ({\mathit {Cut}})$
좌변 논리규칙:	우변 논리규칙:
${\cfrac {\Gamma ,A\vdash \Delta }{\Gamma ,A\land B\vdash \Delta }}\quad ({\land }L_{1})$	${\cfrac {\Gamma \vdash A,\Delta }{\Gamma \vdash A\lor B,\Delta }}\quad ({\lor }R_{1})$
${\cfrac {\Gamma ,B\vdash \Delta }{\Gamma ,A\land B\vdash \Delta }}\quad ({\land }L_{2})$	${\cfrac {\Gamma \vdash B,\Delta }{\Gamma \vdash A\lor B,\Delta }}\quad ({\lor }R_{2})$
${\cfrac {\Gamma ,A\vdash \Delta \qquad \Sigma ,B\vdash \Pi }{\Gamma ,\Sigma ,A\lor B\vdash \Delta ,\Pi }}\quad ({\lor }L)$	${\cfrac {\Gamma \vdash A,\Delta \qquad \Sigma \vdash B,\Pi }{\Gamma ,\Sigma \vdash A\land B,\Delta ,\Pi }}\quad ({\land }R)$
${\cfrac {\Gamma \vdash A,\Delta \qquad \Sigma ,B\vdash \Pi }{\Gamma ,\Sigma ,A\rightarrow B\vdash \Delta ,\Pi }}\quad ({\rightarrow }L)$	${\cfrac {\Gamma ,A\vdash B,\Delta }{\Gamma \vdash A\rightarrow B,\Delta }}\quad ({\rightarrow }R)$
${\cfrac {\Gamma \vdash A,\Delta }{\Gamma ,\lnot A\vdash \Delta }}\quad ({\lnot }L)$	${\cfrac {\Gamma ,A\vdash \Delta }{\Gamma \vdash \lnot A,\Delta }}\quad ({\lnot }R)$
${\cfrac {\Gamma ,A[t/x]\vdash \Delta }{\Gamma ,\forall xA\vdash \Delta }}\quad ({\forall }L)$	${\cfrac {\Gamma \vdash A[y/x],\Delta }{\Gamma \vdash \forall xA,\Delta }}\quad ({\forall }R)$
${\cfrac {\Gamma ,A[y/x]\vdash \Delta }{\Gamma ,\exists xA\vdash \Delta }}\quad ({\exists }L)$	${\cfrac {\Gamma \vdash A[t/x],\Delta }{\Gamma \vdash \exists xA,\Delta }}\quad ({\exists }R)$
좌변 구조규칙:	우변 구조규칙:
${\cfrac {\Gamma \vdash \Delta }{\Gamma ,A\vdash \Delta }}\quad ({\mathit {WL}})$	${\cfrac {\Gamma \vdash \Delta }{\Gamma \vdash A,\Delta }}\quad ({\mathit {WR}})$
${\cfrac {\Gamma ,A,A\vdash \Delta }{\Gamma ,A\vdash \Delta }}\quad ({\mathit {CL}})$	${\cfrac {\Gamma \vdash A,A,\Delta }{\Gamma \vdash A,\Delta }}\quad ({\mathit {CR}})$
${\cfrac {\Gamma _{1},A,B,\Gamma _{2}\vdash \Delta }{\Gamma _{1},B,A,\Gamma _{2}\vdash \Delta }}\quad ({\mathit {PL}})$	${\cfrac {\Gamma \vdash \Delta _{1},A,B,\Delta _{2}}{\Gamma \vdash \Delta _{1},B,A,\Delta _{2}}}\quad ({\mathit {PR}})$

제약: 규칙 $({\forall }R)$ 및 $({\exists }L)$ 에서, 변항 $y$ 는 더 아래의 시퀀트(Γ, A[x/y], Δ)에서는 자유롭지 않다.

위의 규칙들은 논리규칙(logical rules)과 구조규칙(structural rules)으로 나뉘는데, 논리규칙은 귀결관계 $\vdash$ 의 우변 또는 좌변에 새로운 논리식을 도입하고, 구조규칙은 논리식의 정확한 형태는 무시하고 시퀀트의 구조를 조작한다. 다만 동일성의 공리(I)와 컷 규칙(Cut)은 예외이다.

이들 규칙들은 보통 증명의 과정에 관한 것이지만, 컷 규칙(자름 규칙)은 방향성이 조금 다르다. 이는 논리식 A가 귀결인 동시에 다른 귀결의 전제가 되기도 하는 경우 A를 빼돌린채 논리적 귀결관계를 결합하는 것이 가능함을 보이는 규칙인데, 증명을 bottom-up 방식으로 행하는 경우 A가 무엇인지 알아맞추어야 하게 되어 문제가 생긴다. 이것을 다루는 정리가 자름-제거 정리(cut-elimination theorem)로, 이는 컷 규칙을 써서 증명가능한 식은 컷 규칙을 쓰지 않고도 증명하는 방법이 반드시 존재한다는 내용의 정리이다.

같이 보기