논리학 입문을 위해 겐첸의 시퀀트 표기법과 시퀀트 계산법, 자연 연역, 단측 시퀀트, 직관주의 논리, 그리고 단순형 람다 계산과의 대응을 개관한다.
2025년 1월 13일
이 글은 논리(Logic)에 관한 연재의 첫 글이다. 여기서 다루는 생각들은 프로그래밍 언어 이론, 특히 타입 이론과 람다 계산에 관한 중요한 논문들을 이해하는 데 매우 유용하다. 우선 논리 체계로서의 시퀀트와 시퀀트 계산법(Sequent Calculus)을 설명한 뒤, 다음 글에서는 선형 논리(linear logic)를 파고들 것이다. 그리고 세 번째 글에서는 Par와 고전 논리(classical logic)의 계산적 해석을 다루며 이 삼부작을 마무리할 계획이다.
이 글에서는 어떤 논리 체계의 모든 규칙을 다 제시하지는 않을 것이다. 대신 각 체계마다 몇 가지 규칙만 예시로 들어, 규칙이 어떻게 작동하는지 설명하고, 앞으로 여러분이 이런 규칙을 읽고 직접 쓸 수 있도록 돕는 데 초점을 맞추겠다. 또 하나의 이유는, 서로 다른 참고 문헌들이 같은 체계를 약간씩 다르지만 결국은 동치인 규칙들로 제시하는 경우가 많기 때문이다.
논리는 학문 분야로서 수천 년의 역사를 가지고 있다. 그런데 1900년대 초, 수학자들이 자신들이 무엇을 하고 있는지, 그리고 그것을 왜 신뢰할 수 있는지 이해하기 위해 논리학을 본격적으로 들여다보면서, 논리는 새롭고 흥미로운 방향으로 폭발적으로 전개되었다. 이때 게르하르트 겐첸(Gerhard Gentzen)이라는 뛰어난 논리학자(안타깝게도 나치에 가담했는데, 무관심 때문이었다거나 심지어 강요에 의한 것이었다는 주장도 있다)가 1934년에 다음과 같은 추론 표기법을 개발했다. 이 글의 나머지를 이해하기 위해서는 이 표기법을 알아두는 것이 중요하다. 왜 이 글을 이해하는 데 특별한 표기법이 필요한가? 어떤 수학적 표기법은 무슨 일이 실제로 벌어지는지를 훌륭하게 드러내 주고, 뇌 속에 완벽한 직관을 심어 주는데, 겐첸의 표기법은 그중에서도 가장 뛰어난 축에 속한다.
이 표기법을 "시퀀트 표기법(sequent notation)"이라고 부르는데, 턴스타일(turnstile) 기호 ⊢를 기준으로 양옆에 있는 (비어 있을 수도 있는) 기호들의 리스트 쌍을 "시퀀트(sequent)"라고 부르기 때문이다. 여기에는 세 개의 시퀀트가 있는 식이다, 라고 말할 수 있다. 시퀀트 표기법은 꽤 까다롭게 느껴질 수 있는데, 가장 좋은 요령은 머리를 잠시 꺼두고, 이것을 멍청한 기계적 기호-재작성기(symbol rewriter)쯤으로 보는 것이다. 이제 설명해 보겠다.
수평선(가로줄)은 위쪽을 "입력", 아래쪽을 "출력"이라고 생각하면 된다. 이 덕분에 다음과 같은 식으로 여러 줄을 이어 붙일 수 있다:
(여기에는 규칙들을 이어 붙인 도식이 온다고 생각하면 된다.)
이 표기법은 두 가지 방식으로 사용된다. "추론 규칙(inference rule)"과 "도출 나무(derivation tree)"이다. 추론 규칙은 가로줄이 한 줄만 있어서, 위(입력)와 아래(출력)가 하나씩만 있다. 도출 나무는 이런 추론 규칙들을 위와 같은 식으로 체인처럼 연결한 것이다. 도출 나무를 얘기할 때 각 가로줄 하나를 "단계(step)"라고 부르며, 이 단계들은 각각 어떤 추론 규칙과 정확히 일치해야 한다. 따라서 위에서 본 체인이 하나의 도출 나무라면, 아마도 다음 두 가지 추론 규칙을 사용하고 있을 것이다:
(여기에는 두 개의 규칙 예시가 온다고 생각하면 된다.)
여기서 가운데 시퀀트가 연결 포인트 역할을 한다. 하나의 추론 규칙에서는 그 시퀀트가 아래쪽(출력)이고, 다른 추론 규칙에서는 위쪽(입력)의 일부이기 때문이다. 레고 블록을 떠올려 보자. 아래쪽 블록의 위가, 위쪽 블록의 아래와 정확히 맞아떨어지면 두 블록을 포개서 쌓을 수 있다. 마찬가지로 추론 규칙도, 아래쪽 규칙의 출력과 위쪽 규칙의 입력이 일치하면 층층이 쌓을 수 있다.
추론 규칙은 도출 나무에서 허용되는 올바른 한 단계 한 단계를 기술하는 것이므로, 규칙의 위쪽 시퀀트에는 종종 "메타변수(metavariable)"를 채워 넣는다. 메타변수는 일종의 와일드카드로, 아무 표현이나 매칭될 수 있다. 메타변수를 어떻게 표기할지는 문맥마다 다르지만, 보통 그리스 문자나 라틴 문자(영어 알파벳) 하나를 메타변수로 쓴다.
안타깝게도 여기서 "보통(typically)"이라고 했지 "항상(always)"이라고 하지는 못한다. 예외가 정말 많아서, 실제로는 문맥 단서를 활용해 시퀀트 표기법을 해독해야 할 때가 잦다.
만약 같은 메타변수가 시퀀트의 위쪽에 여러 번 등장한다면, 그 부분들은 서로 같은 것이라야 한다. 왜냐하면 하나의 메타변수는 한 번에 단 하나의 것만 가리킬 수 있기 때문이다(여러 번 등장하더라도). 메타변수는 표현식의 일부, 하나의 전체 표현식, 혹은 리스트에서 서로 인접한 여러 표현식들을 대신할 수 있다. 하지만 일반적으로 시퀀트 전체(턴스타일의 양쪽 리스트 전체)를 대신하지는 않는다. 메타변수가 정확히 무엇을 대신하는지 이해하는 것 역시 불행히도 문맥 단서에 의존한다! 하지만 이런 표기들을 충분히 많이 보고 나면, 꽤 믿을 만한 기대와 직관이 빠르게 자리 잡는다. 이 글의 예시들도 그 직관을 키우는 데 도움이 될 것이다.
마지막으로, 추론 규칙의 아래쪽(출력) 시퀀트에는 위쪽에 등장한 메타변수가 다시 나타나는 경우가 많다. 이것은 "입력에서 그 메타변수가 매칭한 것을, 출력의 이 자리에 그대로 집어넣으라"는 뜻이다. 만약 아래쪽에 어떤 메타변수가 있는데 위쪽에는 한 번도 등장하지 않았다면, 그 메타변수 자리는 그 메타변수가 매칭할 수 있는 아무 것으로나 채워도 좋다는 뜻이다. 무엇을 넣을지는 전적으로 여러분에게 달려 있다. 곧 구체적인 예시를 보게 될 것이다.
이제 겐첸의 표기법을 이용해 실제로 추론을 해 보자! 턴스타일 왼쪽에는 가정(assumptions)을, 오른쪽에는 결론(conclusions)을 두겠다. 이를 다음과 같이 해석하자:
왼쪽의 모든 명제가 참이면, 오른쪽 명제들 가운데 적어도 하나는 참이다.
다시 말해, 왼쪽은 큰 논리곱(“그리고”, conjunction)으로, 오른쪽은 큰 논리합(“또는”, disjunction)으로 볼 수 있다. 만약 왼쪽이 비어 있다면, 오른쪽의 모든 명제가 거짓이 되는 것은 불가능해야 한다(즉, 오른쪽은 항진적인 논리합이다). 반대로 오른쪽이 비어 있다면, 왼쪽의 모든 명제가 참이 되는 것은 불가능해야 한다(즉, 왼쪽은 모순적인 논리곱이다).
여기서 꼭 강조하고 싶은 점이 있다. 우리는 지금 시퀀트 표기법에 **하나의 해석(interpretation)**을 부여한 것이다. 이 해석은 표기법 자체의 본질적인 의미가 아니다. 이 의미는 우리가 선택한 추론 규칙들에서 온다. 이 규칙들을 우리는, 형식 논리를 모사하도록 신중히 설계했다. 그 기반이 되는 시스템, 즉 시퀀트 표기법 자체는 여전히 멍청한 기호 재작성기일 뿐이고, 우리가 어떤 규칙들을 선택하느냐에 따라 그 동작이 구성될 뿐이다.
이제 논리곱(conjunction)에 대해 추론하는 간단한 추론 규칙들을 보자:
(여기에는 ∧ 에 대한 좌/우 규칙 예시가 온다고 생각하면 된다.)
여기서 대문자 그리스 문자 Γ, Δ(감마, 델타)는 리스트에서 서로 인접한 0개 이상의 명제들을 나타내는 메타변수이고, 소문자 라틴 문자 A, B는 하나의 명제를 나타내는 메타변수다. 이 규칙들을 실제 증명(도출 나무)에서 사용하려면 몇 가지 규칙이 더 필요하다. 우선 증명을 시작할 방법, 즉 위가 빈(입력이 없는) 규칙이 필요하다.
이 규칙은 말한다. "위가 비어 있으니 언제나, 어떤 명제 A를 가정하면, 그 A를 결론으로 삼을 수 있다" (A ⊢ A). 이것을 흔히 공리 규칙(Axiom rule)이라고 부른다. 위쪽에서 매칭할 것이 아무것도 필요 없기 때문이다. 다음으로는 "구조 규칙(structural rules)"이 필요하다. 이 규칙들은 리스트(컨텍스트)를 다루는 방법을 제공한다. 세 가지 구조 규칙 각각은 좌측 구조 규칙(left structural rule)과 우측 구조 규칙(right structural rule) 두 가지 변형을 가진다.
이제 도출 나무를 만들어서 무언가를 증명할 수 있게 되었다. 맨 위의 모든 줄이 공리(Axiom) 규칙이고, 그 아래의 각 줄이 어떤 추론 규칙과 정확히 일치하기만 하면, 그 도출 나무 전체는 맨 아래 시퀀트의 증명이 된다!
지금까지 본 것이 바로 시퀀트 계산법(Sequent Calculus)이다. 이 체계는 아주 명시적이고 기계적이어서, 논리학 연구의 대상(object of study)로 매우 좋다. 하지만 실제로 보면 이런 단계들 가운데 상당수는 단지 행정적인 잡무에 가깝다. 그래서, 사람에게 의미 있는 단계만 남겨 둔 다음과 같은 나무를 생각해 보자:
(여기에는 구조 규칙을 생략한 도출 나무 예시가 온다고 생각하면 된다.)
이것이 바로 **시퀀트 자연 연역(Sequent Natural Deduction)**이라는 체계다. 여기서는 턴스타일 오른쪽에 단 하나의 명제만 허용된다. 두 시퀀트가 연결될 수 있는지(즉, 위와 아래를 이어 체인을 만들 수 있는지)를 확인할 때, 단순히 눈에 보이는 것만 비교하는 것이 아니라, 구조 규칙들을 마음속으로 적용해 보면서, 그런 변형을 거친 뒤에라도 서로 일치하는 경우가 있는지를 살펴본다. 그 결과, 이 체계는 연구 대상으로는 훨씬 더 복잡해지지만, 실제로 사용하기에는 훨씬 더 편리하다. 자연 연역 증명은 증명의 **정수(essence)**만을 추려내어, 사람에게 중요한 단계만 보여 준다고 말할 수도 있다.
하지만 시퀀트 자연 연역보다도 더 "자연스러운" 체계가 있으니, 그것이 바로 일반적으로 말하는 **자연 연역(Natural Deduction)**이다:
시퀀트 자연 연역에서는 항상 턴스타일 오른쪽에 정확히 하나의 명제가 있어야 한다. 이 점을 이용하면, 가정들과 턴스타일을 통째로 생략하고도 의미 있게 쓸 수 있다. 왜냐하면 실제로 어떤 명제에 중요한 가정들은 항상 그 명제 바로 위에 표시되어 있기 때문이다! 논리학의 연구 대상으로서 자연 연역은 시퀀트 자연 연역보다도 더 다루기 어렵다. 바로 이처럼 더 많은 것을 생략해 버리기 때문에, 인간의 추론처럼 보이도록 만든 대가를 치르게 되는 것이다.
(여기서 필자는 스탠퍼드 철학 백과사전(Stanford Encyclopedia of Philosophy)의 용어를 따르고 있다. 나는 이 구분이 마음에 들지만, 실제로는 시퀀트 자연 연역과 자연 연역을 구분하지 않고, 둘 다 그냥 "자연 연역"이라고 부르는 경우가 일반적이다.)
시퀀트 계산법에서는 논리곱에 대한 규칙들이, 논리곱을 턴스타일 왼쪽에 도입하거나 오른쪽에 도입하는 식으로 나뉘어 있었다. 반면 시퀀트 자연 연역(그리고 따라서 자연 연역도)은 "도입 규칙(introduction rule)"과 "제거 규칙(elimination rule)"을 사용한다. 예를 몇 가지 보자:
(여기에는 ∧-Intro, ∧-Elim 규칙들의 자연 연역/시퀀트 자연 연역 버전이 온다고 생각하면 된다.)
모든 규칙이, 턴스타일의 각각 한쪽에서 동작하도록 일종의 "쌍"을 이루고 있다는 것을 볼 수 있다. 다만 자연 연역에는 오른쪽 수축(right contraction)과 오른쪽 약화(right weakening) 같은 규칙은 없다. 그런 규칙들은 턴스타일 오른쪽에 여러 개의 명제를 두어야 필요해지거나, 그런 여러 명제를 새로 도입해 버리는 규칙이기 때문이다. 또 한 가지 알아 둘 점은, 턴스타일 왼쪽에서의 논리곱은 쉼표와 동치라는 것이다(그래서 왼쪽 논리곱 제거 규칙 모양이 좀 괴상하다). 따라서 왼쪽 논리곱 도입 규칙은 사실상 왼쪽 약화 규칙과 거의 다르지 않다.
지금까지 규칙이 너무 많아 보인다는 느낌이 들 것이다. 턴스타일 오른쪽 규칙 하나마다 왼쪽 규칙이 하나씩 짝을 이루고 있으니, 모든 규칙이 두 배로 늘어난 셈이다. 이를 피하는 방법이 바로 **단측 시퀀트 계산법(one-sided sequent calculus)**이다. 여기서는 모든 것을 턴스타일 오른쪽에서만 한다.
이 방식을 쓰려면 우선, 부정(negation, "not", ¬)에 대한 도입/제거 규칙부터 시작하자. 이제는 왼쪽-도입/오른쪽-도입 같은 말을 할 수 없으므로, 단순히 도입 규칙과 제거 규칙만 있게 된다. 왜냐하면 이제는 시퀀트에 단 한쪽만 존재하기 때문이다!
(여기에는 ¬-Intro, ¬-Elim에 해당하는 단측 시퀀트 규칙이 온다고 생각하면 된다.)
이 규칙들은 꽤 낯설게 느껴지기 시작한다. 여기서 기억해야 도움이 되는 사실은, 단측 시퀀트 계산법에서는 턴스타일 오른쪽의 쉼표가 **논리합(disjunction)**을 나타낸다는 점이다. 즉, 단측 시퀀트 ⊢ A, B, C는 "이 명제들 가운데 하나는 참이다"라는 뜻이다.
이제 논리합과 부정만 있으면, 고전 논리(classical logic)에서 다른 논리 기호들을 모두 정의할 수 있다. 예를 들어, 함의(implication) A → B는 ¬A ∨ B와 동치다. 함의를 가지게 되면, 가정(assumption)을 시뮬레이션할 수 있다(가정은 원래 턴스타일 왼쪽에 있던 것들이다). 따라서 앞서 소개한 시퀀트 계산법의 논리곱 규칙들을, 이 단측 시퀀트 시스템으로 쉽게 옮길 수 있다!
우선, 논리곱에 대해서는 자연 연역 규칙이 이미 단측 형태(턴스타일 오른쪽에만 있는 형식)였으므로, 그것부터 다시 적어 보고, 이어서 턴스타일 왼쪽에서의 논리곱에 해당하는 규칙들을 단측 시퀀트 시스템에서 도출해 보자:
(여기에는 ∧에 대한 단측 자연 연역 규칙과, 그로부터 도출된 왼쪽 규칙에 해당하는 단측 시퀀트 규칙이 온다고 생각하면 된다.)
만약 이 논리곱 도입/제거 규칙들이 여러분이 알고 있는 논리곱의 의미와 잘 매치되지 않는다면, 이렇게 생각해 보면 도움이 된다. 단측 시퀀트 계산법에서 쉼표는 논리합이므로, 오른쪽에 있는 명제들 가운데 적어도 하나는 참이다.
∧-제거 규칙 두 개를 보자. 만약 논리곱 A ∧ B가 참이라면, 그 각 항 A, B도 참이므로, 논리곱을 항 중 하나로 바꾸어도 타당하다. 반대로 A ∧ B가 거짓이라면, 리스트 안 어딘가에 있는 다른 명제가 참이어야 하므로, 논리곱 자리를 무엇으로든(참이든 거짓이든) 바꾸어도 여전히 전체 논리합은 참이다.
이제 ∧-도입 규칙을 보자. 만약 A와 B가 둘 다 참이라면, 리스트 Γ에 있는 모든 명제가 거짓일 수도 있지만, 그래도 A ∨ B는 참이다. 왜냐하면 A가 참이기 때문이다. 반대로 A나 B 가운데 하나라도 거짓이라면, 그 대신 Γ 안 어딘가에 있는 어떤 명제가 참이어야 한다. 그러면 A가 거짓이더라도 A ∨ B는 여전히 참이 된다. 요약하자면, 여기서 우리가 취해야 할 태도는 "만약 Γ 안의 모든 것이 거짓이라면, 우리는 그것들을 무시해도 된다. 그렇지 않다면, 우리가 지금 하는 조작은 상관없다"는 것이다. 이것은 논리의 ∨, ¬ 규칙들에서 비롯된다.
이렇게 하면, 우리의 규칙들이 턴스타일 오른쪽에 한 개의 명제만 두는 자연 연역 같은 계산법들에 조금 더 가깝게 보인다.
단측 시퀀트 계산법에서 눈여겨볼 점은, 어떤 명제를 마치 턴스타일 왼쪽에 있는 것처럼 다루고 싶다면, 그냥 그 명제를 부정해 버리면 된다는 것이다. 논리학에서는 이것을 아주 심오한 아름다움으로 여긴다. 가정(assumptions)의 구조가 잠재적 결론들의 구조에 단지 부정을 취한 것과 같다는 사실 때문이다. 앞으로의 글들에서 이 아름다움을 더 깊이 파고들 예정이다. 바로 이 사실, 즉 한쪽을 다른 쪽의 부정으로 시뮬레이션할 수 있다는 점 덕분에, 단측 시퀀트 계산법은 왼쪽 규칙들을 전혀 두지 않고도(중복 규칙 없이) 모든 것을 처리할 수 있고, 그래서 전체 규칙 수가 훨씬 적어진다.
단측 시퀀트 계산법은 매우 우아하지만, 실제 논리학 분야에서는 그다지 널리 쓰이지는 않는다. 그 이유는 이 체계가 본질적으로 **고전 논리적(classical)**이기 때문이다. 앞서 보았듯, 우리의 공리(Axiom) 규칙이 바로 배중률(law of excluded middle) 규칙으로 바뀌어 버렸다는 점을 떠올려 보자!
직관주의 논리(intuitionistic logic)는 턴스타일 왼쪽이 꼭 필요하다. 왜냐하면 이 논리에서는 함의(→)가 더 이상 "부정된 전건과 후건의 논리합"(¬A ∨ B)과 동치가 아니고, 왼쪽 규칙과 오른쪽 규칙이 서로 부정 관계에 있지도 않기 때문이다. 또, 턴스타일 오른쪽의 쉼표에 대한 전형적인 규칙들은, 직관주의 논리에서의 논리합이 작동하는 아주 특이한 방식과 잘 맞지 않는다.
그래서 직관주의 논리는 항상 (시퀀트) 자연 연역 방식으로 다루며, 턴스타일 오른쪽에는 단 하나의 명제만 허용한다. 그 명제는 직관주의적 논리합(직관주의적 disjunction)일 수도 있다.
이론적으로는, 턴스타일 오른쪽의 쉼표를 직관주의적 논리합으로 새로 정의할 수도 있다. 지금까지 직관주의 논리에서는 오른쪽 쉼표의 의미가 아예 정의되지 않았기 때문이다. 하지만 그렇게 할 실질적인 이점은 없다. 직관주의적 논리합은 완전히 다른 규칙들을 가지며, 왼쪽 쉼표와 쌍을 이루는 이중(dual) 관계도 아니고, 비교 가능한 것도 아니다. 따라서 오른쪽에는 굳이 쉼표의 특수 규칙을 새로 도입하는 대신, 기존의 논리합 기호 ∨를 쓰는 것으로 충분하다. 아래는 직관주의 논리에서의 논리합(∨)에 대한 추론 규칙들이다:
(여기에는 직관주의 논리의 ∨-Intro, ∨-Elim 규칙이 온다고 생각하면 된다.)
자연 연역과 직관주의 논리 사이의 연결은 상당히 강하다. (어쩌면 "자연스럽다"고까지 말할 수 있을 것이다!) 고전 자연 연역도 가능하지만, 전통적으로는 다소 실망스럽고 만족스럽지 못한 것으로 여겨진다. 고전 자연 연역을 구현하는 한 가지 방법은, 우리가 앞서 살펴본 (고전적인) 단측 시퀀트 계산법의 공리 규칙, 즉 배중률에 해당하는 두 번째 공리 규칙을 자연 연역에 그대로 도입하는 것이다:
⊢ A, ¬A에 해당하는 규칙을 자연 연역에 공리로 추가하는 식이다.
그러나 직관주의 논리의 진짜 장점은, 여기에 계산적인 **증명 항(proof term)**을 부여할 수 있다는 데 있다. 증명 항은 어떤 형이 지정된 람다 계산(typed lambda calculus) 안의 표현식으로, 그 타입이 직관주의 논리의 참인 명제에 해당할 때에만, 그 표현식이 정규형(normal form)을 가진다(계산 도중 무한 루프에 빠지지 않는다). 그래서 이를 "증명 항"이라고 부른다. 어떤 타입을 가진 완전히 계산된 표현식(정규형)이 하나 존재한다는 사실이, 그에 대응하는 명제가 참이라는 증명이 되는 것이다.
일반적으로 고전 논리를 연구할 때는 이런 증명 항을 쓰지 않는다. 다만 이후 글들에서 고전 논리에 대해서도 증명 항을 부여하는 여러 가지 방법을 살펴볼 예정이다. 하지만 지금은 논의를 단순하게 유지하기 위해, 직관주의 논리의 간단한 경우에만 집중하겠다.
단순화를 위해, 직관주의 논리를 함의(→)와 ⊥만으로 제한하자. 이 둘만으로도 논리곱, 논리합, 부정을 모두 표현할 수 있다. 이때 타입과 명제 사이의 대응은 다음과 같다.
⊥는 아무 값도 가지지 않는 타입에 대응한다.이렇게 하면, 단순형 람다 계산(simply-typed lambda calculus)이 명제 논리의 직관주의 논리 중에서도 "함의 부분(fragment)"에 해당하는 체계에 증명 항을 제공하게 된다. 여기서는 약간 새로운 표기를 쓰겠다:
(여기에는 Γ ⊢ e : A 형태의 규칙들, 예를 들면 Axiom, →-Intro, →-Elim, ⊥-Elim 등이 온다고 생각하면 된다.)
이제 시퀀트 곳곳에 콜론이 붙어 있는 것을 볼 수 있다. Γ ⊢ e : A는 "e는 A의 증명이다", 또는 동등하게 "e는 타입 A를 갖는 단순형 람다 계산식이다"라는 뜻이다.
메타변수에 대해 한 가지 언급하자면, x, y, z 같은 기호는 람다 계산의 변수를 나타내고, e는 임의의 람다 계산식 전체를 나타낸다. 따라서 컨텍스트(가정) 안에 들어가는 증명 항들은 항상 변수만 된다. 예를 들어, Γ, x : A와 같은 식이다. 이 중 x : A는 Axiom 규칙을 쓸 때, Γ 안에 새롭게 추가해 줄 수 있다.
타입들이 명제를 "의미한다"는 점을 강조하기 위해, 여기서는 타입 표기에 전통적인 프로그래밍 언어 표기(예: A -> B) 대신 논리 표기(예: A → B)를 쓰고 있다. 이 체계는 단순형 람다 계산이므로, 이 추론 규칙들로 만들어지는 표현식들은 계산 도중 영원히 루프에 빠지는 일이 없다. 따라서 턴스타일 오른쪽에 등장하는 모든 표현식은 자신의 타입/명제에 대한 올바른 증명이다.
여기서 메타변수 사용이 조금 복잡해졌으므로, 이들을 기술하는 정식 표기법을 소개하겠다. 일반적으로 메타변수의 동작은 **형식 문법(formal grammar)**으로 지정하는데, 이를 기술적으로는 **BNF 문법(Backus–Naur Form)**이라고 부르며, 다음처럼 쓴다:
bnfe ::= x | λx.e | e e Γ ::= · | Γ, x : A A ::= ⊥ | A → A
여기서 ::= 왼쪽에는 메타변수가, 오른쪽에는 그 메타변수가 대체될 수 있는 것들이 온다. | 기호는 "또는(or)"를 뜻한다. 따라서 위의 문법은 다음을 말한다.
e는 변수(x), 람다 추상 λx.e, 또는 응용 e e 가운데 하나일 수 있다.Γ는 빈 컨텍스트 ·, 또는 어떤 컨텍스트 뒤에 x : A를 붙인 형태일 수 있다.A는 ⊥이거나, 두 명제 사이의 함의 A → A일 수 있다(더 완전한 문법에서는 서로 다른 타입 메타변수를 쓰지만, 여기서는 개략만 표현하고 있다).이 정의들은 서로 재귀적으로 되어 있다는 점을 주목하자.
컨텍스트 정의에 등장한 기호 ·도 언급할 만하다. 이것은 빈 컨텍스트를 뜻한다. 기술적으로는 x : A, y : B 같은 컨텍스트를 ((·, x : A), y : B)의 줄임말로 볼 수 있다. 하지만 지금까지 글 내내 그랬듯이, 실제로는 모두가 이렇게 빈 컨텍스트까지 풀어 쓰지 않고 x : A, y : B 같은 간단한 줄임 표기를 쓴다. 실제 논문이나 책에서도 · 기호는 거의 전적으로 이런 형식 문법 안에서만 등장하고, 추론 규칙이나 도출 나무에는 잘 나타나지 않는다. 여기서도 그 전통을 따른 것이다.
이 모든 내용을 염두에 두고, 우리의 직관주의 논리 증명 체계의 **판단 형식(judgement form)**을 다음처럼 쓸 수 있다:
textΓ ⊢ e : A
이것은 어떤 시퀀트가(이 맥락에서는 종종 "판단(judgement)"이라고 부른다) 유효하다는 것을 형식적으로 기술한 것이다. 이것을 자연어 문법으로 비유하면, "유효한 문장은 명사구 다음에 동사구가 온 것"이라는 진술과 비슷하다. 여기서는 "유효한 시퀀트는 컨텍스트 Γ가 왼쪽에, 그다음에 턴스타일 ⊢, 그다음에 표현식 e, 그다음에 콜론 :, 마지막으로 명제 A가 오는 것"이라는 말과 같다.
앞서의 다른 추론 규칙들에도 이런 식의 형식 문법과 판단 형식을 줄 수 있었지만, 거기서는 메타변수 사용이 충분히 단순했기 때문에 생략했다.
이것으로 시퀀트 표기법과 시퀀트 계산법에 대한 속성 강좌를 마친다! 이 시스템을 우아하고도 강력하게 사용하는 선형 논리에 대한 후속 글이 준비 중이다.
© 2025 Ryan Brewer.