Skip to content

ProofTheory Takeuti

Contents

수학은 증명의 모임이다. 수학에 대하여 어떤 스탠스를 취하든1 이 사실은 변함 없다. 그러므로 수학을 조사할 때 효과적인 방법은 수학의 증명을 형식화하고, 증명의 구조를 조사하는 것이다. 이것이 증명 이론이 하는 일이다.

증명 이론은 수학의 무모순성을 증명하려는 힐베르트의 시도에 의하여 시작되었다. 그의 시도는 이후 겐첸에 의하여 발전되었고, 여기에서는 겐첸에 의하여 발전한 증명 이론을 살펴본다.

First Order Predicate Calculus✔

겐첸은 증명 이론 연구에 적합한 1차 논리 술어 계산 \(\mathsf{LK}\) 를 형식화했다. 또한, 직관주의 논리를 위한 \(\mathsf{LJ}\) 도 살펴본다. 각 \(\mathsf{LK}\) 와 \(\mathsf{LJ}\) 에서의 절단 제거 정리(cul-elimination theroem)를 살펴보자.

Formalization of statements✔

논리의 형식화의 첫단계는 형식 언어와 형식적 표현, 식을 만드는 것이다.

정의 1.1 1차 논리 형식 언어(first order formal language)

1차 논리 (형식) 언어는 다음의 기호로 구성된다.

  1. 상수

    1. 개별 상수: \(k_0, k_1, \dots, k_j,\dots\)
    2. \(i (= 1,2,\dots)\) 개의 인자를 갖는 함수 기호 \(f _{0}^{i}, f _{1}^{i},\dots , f _{j}^{i},\dots\)
    3. \(i (= 1,2,\dots)\) 개의 인자를 갖는 술어 기호 \(R _{0}^{i}, R _{1}^{i},\dots , R _{j}^{i},\dots\)

  2. 변수

    1. 자유 변수: \(a_0, a_1, \dots ,a_j,\dots\)
    2. 종속 변수: \(x_0, x_1, \dots ,x_j,\dots\)

  3. 논리적 기호: \(\lnot\), \(\land\), \(\lor\), \(\supset \text{ (implies)}\), \(\forall\), \(\exists\)

  4. 보조 기호: \((\), \()\), \(, \text{ (comma)}\)

모든 상수가 주어졌을 때 1차 논리 언어 \(L\) 이 주어졌다고 말한다.

모든 논의에서 언어 \(L\) 은 고정된다고 가정하므로 "언어 \(L\) 의" 라는 말을 생략한다.

  • 기호의 기수를 \(\aleph _0\) 로 제한할 이유는 없다. 그러나 기초 논리의 표준적인 접근은 순서형 \(\omega\) 의 순서를 갖는 가산 기호들로 시작하는 것이다. 그러므로 특별한 언급이 없는 한 가산 언어를 가정하자.

    그러나 어떤 경우에서든 본질적으로, 변수의 집합은 무한이고 술어 기호는 최소한 하나 이상 존재한다. 다른 상수 집합은 임의이 기수, 심지어 \(0\) 을 가질 수도 있다.

  • 함수 기호와 술어 기호의 \(f _{j}^{i}, R _{j}^{i}\) 의 윗첨자는 자주 생략된다. 또한, 상수와 변수 기호는 관례적으로 더욱 편한 기호로 사용된다. 가령, 함수 상수에는 \(g, h,\dots\) 가, 자유변수에는 \(a,b,c,\dots\) 가, 종속변수에는 \(x,y,z,\dots\) 가 사용된다.

정의 1.2 표현식(expression), 항(term)

언어 \(L\) 의 기호의 임의의 유한열을 \(L\) 의 표현식이라고 한다.

항은 귀납적으로 다음과 같이 정의된다.

  1. 모든 개별 상수는 항이다.
  2. 모든 자유 변수는 항이다.
  3. 함수 상수 \(f ^{i}\) 와 항 \(t_1, \dots, t_i\) 에 대하여 \(f ^{i}(t_1, \dots, t_i)\) 은 항이다.
  4. 오직 1)-3) 에 의하여 얻어진 표현식만 항이다.

  • 항은 자주 \(t,s,t_1,\dots\) 로 표기된다.

  • 귀납적 정의에서 나타나는 조항 4) 는 앞으로는 편의상 생략한다.

정의 1.3 원자식(atomic formula), 식(formula), 닫힌 식(closed formula, 문장, sentence)

\(R ^{i}\) 가 술어 상수이고 \(t_1, \dots, t_i\) 가 항이면 \(R ^{i}(t_1, \dots, t_i)\) 를 원자식이라고 한다.

식과 가장 바깥쪽 기호를 다음과 같이 귀납적으로 정의된다. 식을 위한 메타변수로는 \(A,B,C, \dots\) 가 사용된다.

  1. 원자식은 식이다. 원자식은 가장 바깥쪽 기호를 갖지 않는다.
  2. \(A\) 와 \(B\) 가 식이면 \((\lnot A), (A \land B), (A \lor B), (A \supset B)\) 는 식이다. 이들은 각각 \(\lnot ,\land ,\lor ,\supset\) 의 가장 바깥쪽 기호를 갖는다.
  3. \(A\) 가 식이고, \(a\) 가 자유 변수이고 \(x\) 가 \(A\) 에 나타나지 않는 종속 변수이면 \(\forall x A'\) 와 \(\exists x A'\) 는 식이다. 이때, \(A'\) 은 \(A\) 에서 나타나는 \(a\) 를 \(x\) 로 바꾼 표현식이다. 이들의 가장 바깥쪽 기호는 각각 \(\forall\) 과 \(\exists\) 이다.
  4. 오직 1)-3) 에 의하여 얻어진 표현식만 식이다.

식이 자유 변수를 갖지 않으면 닫힌 식 또는 문장이라고 한다.

  • 3) 에서 \(A'\) 을 \(\forall x\) 와 \(\exists x\) 의 스코프(scope)라고 한다.

  • 사실 자유 변수와 종속 변수의 구별이 본질적이지는 않지만, 이로써 발생하는 기술적인 편의성이 대단히 크다.

  • 3) 에서 \(A\) 에 \(x\) 가 나타나지 않아야 한다는 제한이 \(\forall x(C(x) \land \exists xB(x))\) 같은 식을 없애준다. 그러나 이 제한 때문에 표현력이 약화되지 않는데, 이런 식은 \(\forall y(C(y) \land \exists xB(x))\) 와 같이 치환될 수 있기 때문이다.

  • 가장 바깥쪽 괄호도 자주 생략된다. 이때 1) \(\lnot\), 2) \(\land, \lor\), 3) \(\supset\) 순서로 우선순위를 갖는다. 따라서 \(\lnot A \land B\) 는 \((\lnot A)\land B\) 이고, \(A \land B \supset C\) 는 \((A \land B) \supset C\) 이다.

    \((A \supset B) \land (B \supset A)\) 를 \(A \equiv B\) 로 표기한다.

정의 1.4

표현식 \(A\) 를 잡자. 서로 다른 원시 기호 \(\tau_1,\dots ,\tau_n\) 과 임의의 기호 \(\sigma _1,\dots ,\sigma _n\) 를 잡자. 다음을 \(A\) 에서 나타난 \(\tau_1,\dots ,\tau_n\) 을 각각 \(\sigma _1,\dots ,\sigma _n\) 로 치환하여 얻은 표현식이라고 정의한다. 이때 \(\tau_1,\dots ,\tau_n\) 가 \(A\) 에서 실제로 나타날 필요는 없다.

\[ \left( A \frac{\tau_1,\dots, \tau_n}{\sigma _1,\dots ,\sigma _n} \right) \]

명제 1.5

  1. \(A\) 가 \(\tau_1,\dots ,\tau_n\) 을 갖지 않으면 \(\left( A \dfrac{\tau_1,\dots ,\tau_n}{\sigma _1,\dots ,\sigma _n} \right)\) 은 \(A\) 그 자체이다.

  2. \(\sigma _1,\dots ,\sigma _n\) 이 서로 다른 원시 기호이면

    \[\left( \left( A \dfrac{\tau_1,\dots ,\tau_n}{\sigma _1,\dots ,\sigma _n} \right)\dfrac{\sigma _1,\dots ,\sigma _n}{\theta_1,\dots ,\theta_n} \right)\]

    는 \(\left( A \dfrac{\tau_1,\dots ,\tau_n}{\theta _1,\dots ,\theta _n} \right)\) 와 같다.

정의 1.6

  1. 식 \(A\) 와 항 \(t_1, \dots, t_n\) 을 잡자. 다음을 만족하는 식 \(B\) 와 \(n\)개의 서로 다른 자유 변수 \(b_1, \dots, b_n\) 가 존재한다고 가정하자.

    • \(A\) 는 \(\left( B \dfrac{b_1, \dots, b_n}{t_1, \dots, t_n} \right)\) 이다.

    그러면 위 치환에 의하여 나타난 각 \(i ( 1 \leq i \leq n)\) 에 대한 \(t_i\) 들이 \(A\) 에서 표시되었다고 한다.

    이때 \(B\) 를 \(B(b_1, \dots, b_n)\) 라고 쓰고 \(A\) 를 \(B(t_1, \dots, t_n)\) 라고 쓴다.

  2. 어떤 식 \(B\) 에 대하여 \(A\) 가 \(\left( B \dfrac{b_1}{t} \right)\) 인 경우에서 \(A\) 의 모든 항 \(t\) 가 얻어졌다면, 항 \(t\) 가 \(A\) 에서 완전히 표시되었다 또는 \(A\) 에서 나타난 모든 \(t\) 가 표시되었다고 한다.
  • 치환에 의하여 \(A\) 를 얻어낼 수 있는 식 \(B\) 와 자유변수는 유일하지 않다. 그러므로 \(A\) 에서 표시된 항은 식 \(B\) 와 자유변수에 상대적이다.

명제 1.7

\(A(a)\) 가 식이고(\(a\) 가 \(A\) 에서 완전히 표시될 필요는 없다) \(x\) 가 \(A(a)\) 에서 나타나지 않는 종속 변수이면, \(\forall xA(x)\) 와 \(\exists xA(x)\) 는 식이다.

  • 증명

    \(A(a)\) 의 논리적 기호의 갯수에 대한 귀납법으로 증명된다. ■

정의 1.8 시퀸트(sequent)

이제 \(\Gamma ,\Delta ,\Pi_{}^{}, \Lambda,\Gamma _0,\Gamma _1, \dots\) 를 콤마로 구분되는 비어있어도 되는 유한한 식의 열로 정의한다.

임의의 \(\Gamma\) 와 \(\Delta\) 에 대하여 \(\Gamma \to \Delta\) 를 시퀸트라고 부른다. \(\Gamma\) 를 선행자(antecedent), \(\Delta\) 를 후행자(succedent)라고 하고, \(\Gamma\) 와 \(\Delta\) 안의 각 식을 시퀸트식(sequent-formula)이라고 한다.

\(m,n \geq 1\) 에 대한 시퀸트 \(A_1, \dots, A_m \to B_1, \dots, B_n\) 는 \(A_1 \land \dots \land A_m\) 이면 \(B_1 \lor \dots \lor B_n\) 이라는 것을 의미한다.

\(m \geq 1\) 에 대한 시퀸트 \(A_1, \dots, A_m \to\) 는 \(A_1 \land \dots \land A_m\) 가 모순을 낳는다는 것을 의미한다.

\(n \geq 1\) 에 대한 시퀸트 \(\to B_1, \dots, B_n\) 는 \(B_1 \lor \dots \lor B_n\) 가 성립한다는 것을 의미한다.

빈 시퀸트 \(\to\) 는 모순이 존재한다는 것을 의미한다.
  • 시퀸트를 보통 \(S\) 로 표기한다.

Formal proofs✔

정의 2.1 추론(inference)

추론은 시퀸트 \(S_1,S_2,S\) 에 대한 다음과 같은 형태의 표현식이다. 이때 \(S_1, S_2\) 를 상시퀸트, \(S\) 를 하시퀸트라고 한다.

\[ \dfrac{S_1}{S} \enspace \text{ or }\enspace \dfrac{S_1 \quad S_2}{S} \]

이것의 의미는 각각 \(S_1\)(또는 \(S_1\) 과 \(S_2\))가 주장되면, 그것으로부터 \(S\) 를 추론할 수 있다는 것이다.

식 \(A,B,C,D,F(a)\) 에 대하여 다음과 같이 추론 규칙을 제한한다.

  1. 구조적 규칙

    1. 약화(weakening): \(D\) 를 약화식(weakening formula)이라고 한다.

    2. 축소(contraction):

    3. 교환(exchange):

    위 3가지 추론규칙을 약한 추론(weak inference)이라고 하고, 나머지 아래의 추론규칙을 강한 추론(strong inference)이라고 한다.

    1. 절단(cut): \(D\) 를 절단식(cut formula)이라고 한다.

  2. 논리적 규칙

    1. \(\lnot\): \(D\) 와 \(\lnot D\) 를 각각 보조식(auxiliary formula), 주요식(principal formula)라고 한다.

    2. \(\land\): \(C\) 와 \(D\) 를 보조식, \(C \land D\) 를 주요식이라고 한다.

    3. \(\lor\): \(C\) 와 \(D\) 를 보조식, \(C \lor D\) 를 주요식이라고 한다.

    4. \(\supset\): \(C\) 와 \(D\) 를 보조식, \(C \supset D\) 를 주요식이라고 한다.

    지금까지의 4가지 추론을 명제 추론이라고 한다.

    1. \(\forall\): \(t\) 는 임의의 항이고, \(a\) 는 하시퀸트에서 나타나지 않는 자유변수이다. \(F(t)\) 와 \(F(a)\) 를 보조식, \(\forall xF(x)\) 를 주요식이라고 한다. 오른쪽 \(\forall\) 에서 \(a\) 를 고유변수(eigenvariable)라고 한다.

      오른쪽 \(\forall\) 의 \(F(a)\) 에서 나타난 모든 \(a\) 는 표시되었다.

      왼쪽 \(\forall\) 에서 \(F(t)\) 와 \(F(x)\) 는 각각 어떤 자유변수 \(a\) 에 대하여 \(\left( F(a)\dfrac{a}{t} \right)\) 와 \(\left( F(a) \dfrac{a}{x} \right)\) 이다. 따라서 모든 \(F(t)\) 안의 \(t\) 가 표시될 필요는 없다.

    2. \(\exists\): \(a\) 는 하시퀸트에서 나타나지 않는 자유변수이고, \(t\) 는 임의의 항이다. \(F(a)\) 와 \(F(t)\) 를 보조식, \(\exists xF(x)\) 를 주요식이라고 한다. 왼쪽 \(\exists\) 에서 \(a\) 를 고유변수(eigenvariable)라고 한다.

      왼쪽 \(\exists\) 의 \(a\) 는 완전히 표시된 반면, 오른쪽 \(\exists\) 의 모든 \(t\) 가 표시될 필요는 없다. \(F(t)\) 는 어떤 \(a\) 에 대한 \((F(a)\frac{a}{t})\) 이다.

    지금까지의 2가지 추론을 양화 추론이라고 한다. 고유변수 \(a\) 가 하시퀸트에 나타나지 않아야 한다는 조건을 고유변수 조건(eigenvariable condition)이라고 한다.

정의 2.2 초기 시퀸트(initial sequent, 공리, axiom), 증명(proof)

\(A \to A\) 형태의 시퀸트를 초기 시퀸트 또는 공리라고 한다.

(\(\mathsf{LK}\) 안의) 증명 \(P\) 또는 \(\mathsf{LK}\)-증명은 다음 조건을 만족하는 시퀸트 트리이다. (트리의 시작 노드를 루트, 트리의 마지막 노드를 리프라고 한다.)

  1. \(P\) 의 루트 시퀸트는 초기 시퀸트이다.
  2. \(P\) 의 리프를 제외한 모든 시퀸트는 하시퀸트가 \(P\) 에 속하는 어떤 추론의 상시퀸트이다.
  • 편의상 \(\Gamma , \Delta, \Lambda\) 등을 공집합으로 두면 추론규칙이 훨씬 쉽게 이해된다.

정의 2.3 끝시퀸트(end-sequent), 증명가능성(provability), 정리(theorem)

정의 2.2 로부터 증명 \(P\) 에는 유일한 리프 시퀸트가 존재한다는 것을 알 수 있다. 이것을 \(P\) 의 끝시퀸트라고 한다.

끝시퀸트 \(S\) 를 갖는 증명을 \(S\) 의 증명이라고 한다.

시퀸트 \(S\) 에 대하여 그것의 \(\mathsf{LK}\)-증명이 존재하면 \(S\) 가 \(\mathsf{LK}\) 에서 증명가능하다고 한다.

식 \(A\) 에 대하여 시퀸트 \(\to A\) 가 \(\mathsf{LK}\)-증명가능하면 식 \(A\) 를 \(\mathsf{LK}\)-증명가능하다 또는 \(\mathsf{LK}\) 의 정리(theorem)라고 한다.
  • 프리픽스 \(\mathsf{LK}\)-는 자주 생략된다.

  • 증명의 부분을 요약하여 \(\proofpart\) 라고 표기한다. 가령, 다음은 각각 \(S\) 증명과, \(S_1\) 과 \(S_2\) 로부터의 \(S\) 의 증명을 뜻한다.

  • 증명은 \(P, Q, \dots\) 로 표기된다. 표현식 \(P(a)\) 는 \(P\) 안에서 나타난 모든 \(a\) 가 표시되었다는 것이다. 물론 이러한 표기는 다른 항에 의한 \(a\) 의 치환이 고려되었을 때에만 유용하다. \(P(t)\) 는 \(P(a)\) 안의 모든 \(a\) 를 \(t\) 로 치환한 결과이다.

  • 가령, 시퀸트 \(\Gamma \to \Delta ,A\) 와 \(\Pi_{}^{}\to \Lambda,B\) 로부터 추론규칙을 적절히 적용하여 \(\Gamma ,\Pi_{}^{},\Delta ,\Lambda,A \land B\) 를 도출할 수 있다. 이런 경우 중간 과정을 생략하고 다음과 같이 표기한다.

  • \(\mathsf{LK}\) 의 양화사가 없는 부분체계를 명제 계산(propositional calculus)이라고 한다.

정의 2.8

  • 증명 \(P\) 의 시퀸트 열이 다음을 만족하면 (\(P\) 의) 스레드(thread)라고 한다.

    1. 열이 초기 시퀸트로 시작하고 끝시퀸트로 끝난다.
    2. 마지막 시퀸트를 제외한 열의 모든 시퀸트가 추론의 상시퀸트이고, 그 추론의 하시퀸트가 뒤따라온다.

  • 증명 \(P\) 안의 시퀸트 \(S_1, S_2, S_3\) 를 잡자. \(S_1\) 가 \(S_2\) 이전에 나오는 스레드가 존재하면 \(S_1\) 이 \(S_2\) 위에 있다 또는 \(S_2\) 가 \(S_1\) 아래에 있다고 한다. \(S_1\) 이 \(S_2\) 위에 있고 \(S_2\) 가 \(S_3\) 위에 있으면 \(S_2\) 가 \(S_1\) 과 \(S_3\) 사이에 있다고 한다.

  • \(P\) 안의 추론에 대하여 그것의 하시퀸트가 \(S\) 아래에 있으면 그 추론이 \(S\) 아래에 있다고 한다.

  • 증명 \(P\) 를 잡자. \(P\) 의 부분이 그 자체로 증명이면 그것을 \(P\) 의 부분증명(subproof)이라고 한다. 즉, \(P\) 의 임의의 시퀸트 \(S\) 에 대하여 \(S\) 그 자체와 \(S\) 위에 있는 모든 시퀸스로 구성된 \(P\) 의 부분을 끝시퀸트 \(S\) 를 갖는 \(P\) 부분증명이라고 한다.

  • 다음과 같은 형태의 증명 \(P_0\) 를 잡자. \((*)\) 는 \(\Gamma \to \Theta\) 아래의 \(P_0\) 의 부분이다.

    \[ \begin{smallmatrix} & \proofpart \\ & \Gamma \to \Theta \\ (*) & \proofpart \\ \end{smallmatrix} \]

    \(\Gamma ,D \to \Theta\) 로 끝나는 증명 \(Q\) 를 잡자. \(Q\) 로부터의 \(P_0\) 의 복사(copy)를 다음과 같은 형태의 증명 \(P\) 로 정의한다.

    \[ \begin{smallmatrix} Q& \proofpart \\ Q& \Gamma ,D \to \Theta \\ (**) & \proofpart \\ \end{smallmatrix} \]

    이때, \((**)\) 는 \((*)\) 의 각 시퀸트, 가령 \(\Pi_{}^{}\to \Lambda\) 에 대하여, \(\Pi_{}^{},D \to \Lambda\) 로 이루어져있다. 즉, \(P\) 는 \(P_0\) 로부터 \(\Gamma \to \Theta\) 로 끝나는 부분증명은 \(Q\) 로 교체하고, \((*)\) 의 각 시퀸트의 선행자에 식 \(D\) 를 추가하여 얻어진다.

    이것처럼 복사는 후행자에 식을 추가하는 방식으로도 정의될 수 있다.
        Takeuti, G. (2013). Proof theory. Courier Corporation.

  1. 가령, 플라톤 주의, 비플라톤 주의(anti-platonism), 직관주의, 형식주의, 유명론(nominalism) 등등. ↩