시퀀트 계산
시퀀트 계산 > LK 체계

아래에서는 게르하르트 겐첸에 의해 1934년 소개된 가장 일반적인 LK 체계의 추론규칙을 설명한다.
여기서는 아래와 같은 기법이 사용된다:
가로줄 위의 논리식이 주어진 것으로부터 가로줄 아래의 논리식이 도출됨을 나타낸다.
\vdash (턴스타일)은 좌측에 '가정'과 우측에 '진술'을 두어 나눈다. 추론규칙 또한 좌측에 적용되는 규칙과 우측에 적용되는 규칙이 분별된다.
A 와  B는 1차 술어 논리의 논리식들을 나타낸다. (명제논리에 한정하는 경우도 있다)
\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)로, 이는 컷 규칙을 써서 증명가능한 식은 컷 규칙을 쓰지 않고도 증명하는 방법이 반드시 존재한다는 내용의 정리이다.