시퀀트 계산 문서 원본 보기

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

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

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

== 시퀀트 ==
'''시퀀트'''({{llang|en|sequent}})란 일반적인 형태의 논리식(조건절)들의 나열로, 표명(assertion) 방식의 일종이다. 전건의 명제들의 [[논리곱]]을 전제로 삼고 후건의 명제들의 [[논리합]]을 [[논리적 귀결|귀결]]로 삼는다.

:<math>\Gamma\vdash\Sigma</math>

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

: <math>A_1,\,\dots,A_m \,\vdash\, B_1,\,\dots,B_n.</math>

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

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

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

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

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

{| border="0" cellpadding="20" style="text-align:center"
|-
| 동일성의 공리:
| 자름 규칙:
|-
| style="background:#fafafa; border:1px #ccc solid;" | 
<math> \cfrac{\qquad }{ A \vdash A} \quad (I) </math>
| style="background:#fafafa; border:1px #ccc solid;" | 
<math>
   \cfrac{\Gamma \vdash \Delta, A \qquad A, \Sigma \vdash \Pi} {\Gamma, \Sigma \vdash \Delta, \Pi} \quad (\mathit{Cut})
 </math>
|-
| 좌변 논리규칙:
| 우변 논리규칙:
|-
| style="background:#fafafa; border:1px #ccc solid;" | 
<math> \cfrac{\Gamma, A \vdash \Delta} {\Gamma, A \land B \vdash \Delta} \quad ({\land}L_1)
 </math>
| style="background:#fafafa; border:1px #ccc solid;" | 
<math> \cfrac{\Gamma \vdash A, \Delta}{\Gamma \vdash A \lor B, \Delta} \quad  ({\lor}R_1)
 </math>
|-
| style="background:#fafafa; border:1px #ccc solid;" | 
<math> \cfrac{\Gamma, B \vdash \Delta}{\Gamma, A \land B \vdash \Delta}  \quad ({\land}L_2)
 </math>
| style="background:#fafafa; border:1px #ccc solid;" | 
<math> \cfrac{\Gamma \vdash B, \Delta}{\Gamma \vdash A \lor B, \Delta} \quad ({\lor}R_2)
 </math>
|-
| style="background:#fafafa; border:1px #ccc solid;" | 
<math> \cfrac{\Gamma, A \vdash \Delta \qquad \Sigma, B \vdash \Pi}{\Gamma, \Sigma, A \lor B \vdash \Delta, \Pi} \quad ({\lor}L)
 </math>
| style="background:#fafafa; border:1px #ccc solid;" | 
<math> \cfrac{\Gamma \vdash A, \Delta \qquad \Sigma \vdash B, \Pi}{\Gamma, \Sigma \vdash A \land B, \Delta, \Pi} \quad ({\land}R)
 </math>
|-
| style="background:#fafafa; border:1px #ccc solid;" | 
<math>
  \cfrac{\Gamma \vdash A, \Delta \qquad \Sigma, B \vdash \Pi}{\Gamma, \Sigma, A\rightarrow B \vdash \Delta, \Pi} \quad  ({\rightarrow }L)
 </math>
| style="background:#fafafa; border:1px #ccc solid;" | 
<math>
   \cfrac{\Gamma, A \vdash B, \Delta}{\Gamma \vdash A \rightarrow B, \Delta} \quad ({\rightarrow}R)
 </math>
|-
| style="background:#fafafa; border:1px #ccc solid;" | 
<math>
  \cfrac{\Gamma \vdash A, \Delta}{\Gamma, \lnot A \vdash \Delta} \quad  ({\lnot}L)
 </math>
| style="background:#fafafa; border:1px #ccc solid;" | 
<math>
  \cfrac{\Gamma, A \vdash \Delta}{\Gamma \vdash \lnot A, \Delta} \quad ({\lnot}R)
 </math>
|-
| style="background:#fafafa; border:1px #ccc solid;" | 
<math>
  \cfrac{\Gamma, A[t/x] \vdash \Delta}{\Gamma, \forall x A \vdash \Delta} \quad  ({\forall}L)
 </math>
| style="background:#fafafa; border:1px #ccc solid;" | 
<math>
  \cfrac{\Gamma \vdash A[y/x], \Delta}{\Gamma \vdash \forall x A, \Delta} \quad  ({\forall}R)
 </math>
|-
| style="background:#fafafa; border:1px #ccc solid;" | 
<math>
  \cfrac{\Gamma, A[y/x] \vdash \Delta}{\Gamma, \exists x A \vdash \Delta} \quad  ({\exists}L)
 </math>
| style="background:#fafafa; border:1px #ccc solid;" | 
<math>
  \cfrac{\Gamma \vdash A[t/x], \Delta}{\Gamma \vdash \exists x A, \Delta} \quad  ({\exists}R)
 </math>
|-
| 좌변 구조규칙:
| 우변 구조규칙:
|-
| style="background:#fafafa; border:1px #ccc solid;" | 
<math>
  \cfrac{\Gamma \vdash \Delta}{\Gamma, A \vdash \Delta} \quad (\mathit{WL})
 </math>
| style="background:#fafafa; border:1px #ccc solid;" | 
<math>
  \cfrac{\Gamma \vdash \Delta}{\Gamma \vdash A, \Delta} \quad (\mathit{WR})
 </math>
|-
| style="background:#fafafa; border:1px #ccc solid;" | 
<math>
  \cfrac{\Gamma, A, A \vdash \Delta}{\Gamma, A \vdash \Delta} \quad (\mathit{CL})
 </math>
| style="background:#fafafa; border:1px #ccc solid;" | 
<math>
  \cfrac{\Gamma \vdash A, A, \Delta}{\Gamma \vdash A, \Delta} \quad (\mathit{CR})
 </math>
|-
| style="background:#fafafa; border:1px #ccc solid;" | 
<math>
  \cfrac{\Gamma_1, A, B, \Gamma_2 \vdash \Delta}{\Gamma_1, B, A, \Gamma_2 \vdash \Delta} \quad (\mathit{PL})
 </math>
| style="background:#fafafa; border:1px #ccc solid;" | 
<math>
  \cfrac{\Gamma \vdash \Delta_1, A, B, \Delta_2}{\Gamma \vdash \Delta_1, B, A, \Delta_2} \quad (\mathit{PR})
 </math>
|}

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

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

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

== 같이 보기 ==
* [[자연 연역]]
* [[자름-제거 정리]]
* [[게르하르트 겐첸]]
* [[증명 이론]]

[[분류:증명 이론]]