토론 : 시퀀트 계산

[damhiya]

@kyh155727 님이 https://github.com/plwiki/plwiki.github.io/pull/12 와 https://github.com/plwiki/plwiki.github.io/pull/14 에서 시퀀트 계산 문서를 작성해주셨고, 두번째 커밋에서 제 질문에 대해 다음과 같은 답변을 주셨습니다.

저는 맥락을 명시하는 자연 연역이 이미 시퀀트 계산이라고 보았습니다. 즉, NK 또한 시퀀트가 라벨인 트리 증명을 갖는다면 시퀀트 계산이라고 봐야 한다고 봅니다. 이 경우 개념 분류 문제가 아니라 어법상의 차이에 기인한 문제가 됩니다. 예컨대, "시퀀트 계산"이라는 용어를 엄격하게 LK의 변종에만 한정하는 용법에 따른다면, NK가 시퀀트 계산이 아닌 것은 맞습니다. 하지만, NK와 LK 모두 겐첸식 시스템이라는 하위 카테고리에 묶이고, 만약 겐첸식 시스템을, 시퀀트가 라벨인 트리 증명으로 표현한다면, 제가 "시퀀트 계산"이라고 말한 것은 "겐첸식 시스템"을 의미하고, "시퀀트 계산"은 LK에 대응될 것입니다.

이에 대해 @kyh155727 님과 대화를 나눴으나, 기록과 추가적인 토론을 위해 이곳에 저의 의견을 정리해 남깁니다.

자연 연역과 시퀀트 계산은 많은 연관점을 가지고 있지만 여전히 둘의 용어가 다르다는 점을 언급하고 싶습니다. 자연 연역에서 도입 규칙 (introduction rule) / 소거 규칙 (elimination rule) / 가정적 판단 (hypothetical judgement) / 맥락 (context) 은 각각 시퀀트 계산의 오른쪽 규칙 (right rule) / 왼쪽 규칙 (left rule) / 시퀀트 (sequent) / 전건 (antecedent) 과 유사한 개념이지만 구분되어 사용됩니다. 이는 제가 생각하기로 다음과 같은 이유가 있습니다. (i) 자연 연역과 시퀀트 계산에서 맥락/전건을 조작하는 방법에 차이가 있습니다. 자연 연역에서는 증명 트리의 자식 트리로 갈 수록 항상 맥락에 원소가 추가 되기만 하지만, 시퀀트 계산에서 전건은 그렇지 않습니다. (ii) 이로 인하여, 자연 연역에서는 Γ |- A의 도출(derivation)을 Γ, A |- B의 도출에 치환해 넣는 것으로 Γ |- B 에 대한 도출을 얻을 수 있지만, 시퀀트 계산에선 이런 도출의 치환을 정의할 수 없습니다. 물론 시퀀트 계산에서도 cut 규칙을 사용하거나, cut의 admissibility를 이용해 비슷한 일을 할 수는 있지만 이는 단순히 도출을 치환만 하는 것과는 다릅니다. (iii) cut이 없는 시퀀트 계산 LJ, LK 등은 subformula property가 성립하지만, 자연 연역 체계에서는 성립하지 않습니다. (iv) 역사적으로 시퀀트와 전건은 겐첸이 제시했고, 가정적 판단과 맥락의 개념은 마틴뢰프가 제시한 것으로 알고 있습니다. 물론 그럼에도 불구하고 '광의의 시퀀트 계산'을 자연 연역을 포함하는 의미로 사용하는 학자가 있을지도 모르겠습니다. 만약 그렇다면 해당 자료에 대한 인용과 함께 학자에 따른 용어법의 차이가 있음을 문서에 적으면 좋을것 같습니다.

[kyh155727]

음... 일단 저도 정리를 하자면 다음과 같습니다.

1. 제가 처음 작성한 문서에서, "시퀀트 계산(sequent calculus)" 은 통상적인 의미의 "겐첸식 시스템(Gentzen system)"을 의미했습니다. 원래는 sentential/propositional calculus나 predicate calculus처럼 sequent가 조작 대상이 되면 저는 sequent calculus라고 보았는데, 지금 보니 sequent calculus가 sequent를 사용하는 논리적 계산법이라는 합성어가 아니라 그냥 두 단어를 합쳐서 별도로, subformula property가 성립하는 고유한 체계를 가리킨다고 보는 게 맞는 것 같습니다.

2. 본래 문서가 그런 방식으로 쓰인 이유는, 시퀀트라는 개념을 LK 외의 다른 체계를 다룰 때 사용하는 경우를 쉽게 찾아볼 수 있기 때문이었습니다.

   • Chiswell 과 Hodges의 Mathematical Logic 에서는 자연 연역 시스템을 다루면서, 제 3장 4절, 구체적으로는 정의 3.4.4(p. 56)에서는 자연 연역 체계에서 가정 $\Gamma$로부터 $\phi$를 도출할 수 있음을 나타내는 관계 $\vdash$를 나타내는 메타진술을 sequent라고 정의합니다. 해당 교재에서는 시퀀트 구조 규칙에 상응하는 몇 가지 성질을 증명하는 연습문제가 있지만, 명시적으로 LK식 시퀀트 계산을 논의하지는 않습니다.
   • Cintula 외 다수가 공저한 Handbook of Mathematical Fuzzy Logic (vol. 1)에서는 프레게-힐베르트 식 공리 체계를 정의하기 위해 제 2장 2.5절의 정의 2.1.4(p. 106)에서, 여러 문장 $\Gamma$와 $\phi$가 가질 수 있는 임의의 모든 관계를 나타내는 표현으로 consecution이라는 개념을 정의합니다. (교재 식 표기법대로면, $\Gamma\cup\phi\subseteq Fm_{\mathcal{L}}$이면 $(\Gamma, \phi)$는 consecution입니다) 그리고 consecution을 기존 sequent, consecutive를 대신해 사용할 수 있다고 말합니다. (정의상, 실제로 그렇게 대신해 사용할 수는 없어 보이지만.) 그리고 이 핸드북의 임의의 공리적 논리 체계는, 문장의 집합이 아니라 시퀀트의 집합 상에서 정의됩니다. (단, 각 장마다 저자가 달라서 이 내용은 2장에만 적용됩니다)

다만 sequent를 사용한다고 해서 명시적으로 sequent calculus라는 표현을 하지는 않기에, 이 부분은 수정해나가겠습니다

[damhiya]

더 자료를 찾아봐야 할것 같지만, 말씀대로 sequent가 sequent calculus로부터 독립적으로 쓰인다는게 설득력이 있는것 같네요. Jonathan Sterling의 Remark on the Hypothetical Judgement에 다음과 같은 주석이 있는데요

Hypothetical judgment is to be distinguished from the sequent judgments Γ ⊢ · · · , which are not even higher-order judgments at all.

저는 여기서 말하는 "sequent judgement Γ ⊢ · · · "가 sequent calculus의 sequent 만을 의미한다고 생각했는데, 말씀을 듣고보니 자연연역에서 쓰이는 Γ ⊢ A와 같은 judgement도 포함해 의미했다고 봐야할지도 모르겠습니다. 다만 Frank Pfenning의 A Judgmental Reconstruction of Modal Logic 에서는 hypothetical judgement를 J₁ ... Jₙ ⊢ J와 같이 표기하고 있긴 합니다.

한편, antecedent와 context는 일반적으로 구분 없이 사용하는 용어가 맞는것 같습니다 (sequent의 antecedent를 hypothetical judgement의 antecedent와 같은 개념으로 봐도 될지는 잘 모르겠지만).