Description
@kyh155727 님이 #12 와 #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) 역사적으로 시퀀트와 전건은 겐첸이 제시했고, 가정적 판단과 맥락의 개념은 마틴뢰프가 제시한 것으로 알고 있습니다.
물론 그럼에도 불구하고 '광의의 시퀀트 계산'을 자연 연역을 포함하는 의미로 사용하는 학자가 있을지도 모르겠습니다. 만약 그렇다면 해당 자료에 대한 인용과 함께 학자에 따른 용어법의 차이가 있음을 문서에 적으면 좋을것 같습니다.