시퀀트 규칙에서의 역할에 따른 공식의 명칭을 설명하는 부분을 규칙 설명 이후로 옮기겠습니다.
저는 맥락을 명시하는 자연 연역이 이미 시퀀트 계산이라고 보았습니다. 즉, NK 또한 시퀀트가 라벨인 트리 증명을 갖는다면 시퀀트 계산이라고 봐야 한다고 봅니다. 이 경우 개념 분류 문제가 아니라 어법상의 차이에 기인한 문제가 됩니다. 예컨대, "시퀀트 계산"이라는 용어를 엄격하게 LK의 변종에만 한정하는 용법에 따른다면, NK가 시퀀트 계산이 아닌 것은 맞습니다. 하지만, NK와 LK 모두 겐첸식 시스템이라는 하위 카테고리에 묶이고, 만약 겐첸식 시스템을, 시퀀트가 라벨인 트리 증명으로 표현한다면, 제가 "시퀀트 계산"이라고 말한 것은 "겐첸식 시스템"을 의미하고, "시퀀트 계산"은 LK에 대응될 것입니다.
그것이 좋을 것 같습니다.
사실 이 부분은 Pfenning 교수의 강의자료 이상의 서술을 제가 하기 어려워서 고민하고 있습니다. 제 문서에서, 중복되는 서술이나 장황한 예시를 제거하고 충분히 문단이 응축된다면, Pfenning 교수 강의자료를 요약하는 방식으로 더 서술하고 출처를 달 생각입니다.
질문에 대한 답변
원래는 의도적으로 그런 설명을 피했습니다. 왜냐하면, 결합성이나 교환성이 부인되는 시퀀트 계산 체계에서는 고전적인 경우와 같은 식의 깔끔한 대응이 이루어지지 않기 때문입니다. (한 문장에 대응시키려면 전건의 문장을 후건으로 모두 내보내야 하는데, 결합과 교환이 부정될 정도로 약한 체계는 일반적인 연역 정리가 성립하지 않습니다. 그래서 basic deduction term같은 개념적 보조도구를 빌려야 합니다.) 그런데 지금 생각해보니, 이 문서의 내용 범위에서 굳이 그 일반적인 사례 때문에 직관적 이해를 숨길 필요가 없다고 생각합니다. 그래서 해당 방식의 시퀀트 의미 이해를 문단에 추가하겠습니다.
이 부분은 제가 잘못 서술한 것이 맞습니다. 물론 SL은 주로 논의되는 구조 규칙을 모두 제거한 체계가 맞고 그것은 substructural logic의 약자입니다(하단 출처 1). 그러나 구조 규칙이 모두 제거된 경우만을 SL로 부른다는 서술은 잘못되었습니다. SL이라는 용어법은 Handbook of Mathematical Fuzzy Logic, Vol. 1, Chp.2 subsection 2.5에 따랐습니다. 다만, 경우에 따라 GL이나 다른 용어법이 있기는 합니다.
의견 반영 및 확인
시퀀트 규칙에서의 역할에 따른 공식의 명칭을 설명하는 부분을 규칙 설명 이후로 옮기겠습니다.
저는 맥락을 명시하는 자연 연역이 이미 시퀀트 계산이라고 보았습니다. 즉, NK 또한 시퀀트가 라벨인 트리 증명을 갖는다면 시퀀트 계산이라고 봐야 한다고 봅니다. 이 경우 개념 분류 문제가 아니라 어법상의 차이에 기인한 문제가 됩니다. 예컨대, "시퀀트 계산"이라는 용어를 엄격하게 LK의 변종에만 한정하는 용법에 따른다면, NK가 시퀀트 계산이 아닌 것은 맞습니다. 하지만, NK와 LK 모두 겐첸식 시스템이라는 하위 카테고리에 묶이고, 만약 겐첸식 시스템을, 시퀀트가 라벨인 트리 증명으로 표현한다면, 제가 "시퀀트 계산"이라고 말한 것은 "겐첸식 시스템"을 의미하고, "시퀀트 계산"은 LK에 대응될 것입니다.
그것이 좋을 것 같습니다.
사실 이 부분은 Pfenning 교수의 강의자료 이상의 서술을 제가 하기 어려워서 고민하고 있습니다. 제 문서에서, 중복되는 서술이나 장황한 예시를 제거하고 충분히 문단이 응축된다면, Pfenning 교수 강의자료를 요약하는 방식으로 더 서술하고 출처를 달 생각입니다.
질문에 대한 답변
원래는 의도적으로 그런 설명을 피했습니다. 왜냐하면, 결합성이나 교환성이 부인되는 시퀀트 계산 체계에서는 고전적인 경우와 같은 식의 깔끔한 대응이 이루어지지 않기 때문입니다. (한 문장에 대응시키려면 전건의 문장을 후건으로 모두 내보내야 하는데, 결합과 교환이 부정될 정도로 약한 체계는 일반적인 연역 정리가 성립하지 않습니다. 그래서 basic deduction term같은 개념적 보조도구를 빌려야 합니다.) 그런데 지금 생각해보니, 이 문서의 내용 범위에서 굳이 그 일반적인 사례 때문에 직관적 이해를 숨길 필요가 없다고 생각합니다. 그래서 해당 방식의 시퀀트 의미 이해를 문단에 추가하겠습니다.
이 부분은 제가 잘못 서술한 것이 맞습니다. 물론 SL은 주로 논의되는 구조 규칙을 모두 제거한 체계가 맞고 그것은 substructural logic의 약자입니다(하단 출처 1). 그러나 구조 규칙이 모두 제거된 경우만을 SL로 부른다는 서술은 잘못되었습니다. SL이라는 용어법은 Handbook of Mathematical Fuzzy Logic, Vol. 1, Chp.2 subsection 2.5에 따랐습니다. 다만, 경우에 따라 GL이나 다른 용어법이 있기는 합니다.