FirstOrder

19세기 말 까지 논리와 증명은 매우 자명해보였기 때문에 논리는 깊게 연구되지 않았다. 하지만 비유클리드 기하학이 발견되면서 해석학에 대한 엄밀한 기반이 요구되자 논리와 증명이 다시 한 번 연구되기 시작했다. 그럼에도 불구하고 수학자들은 논리를 그렇게까지 열정적으로 연구하지는 않았다. 하지만 모순이 발견되면서 수학자들이 쇼크를 먹자 그때부터 논리와 증명에 대한 연구가 열정적으로 이루어지기 시작했다. 모순이란 러셀의 모순, 칸토어의 모순, Burali-Forti 의 모순, 거짓말쟁이 모순, Richard 의 모순, Berry 의 모순, Grelling 의 모순 등등이 있었다. 이 모순들은 집합론의 개념에 관련된 모순과 의미론적인 모순으로 구분되는데, 수학자들은 의미론적 모순보다 논리적 모순을 더 심각하게 생각했다.

모순에 대한 연구는 지금까지 존재했던 수학의 소박한 개념을 제한하여 모순으로 빠지는 것을 방지하게 하는 방법들을 만들어내었다. (논리주의) 러셀은 모든 모순의 근본에 자기지시가 있다고 보고 이것을 해결하는 체계를 만들어서 『Principia Mathematica』 (수학원리) 에 소개했다. 수학원리는 알려진 모순을 해결했지만 여전히 어설펐고 단점이 있었다. (공리주의) 다른 방법으로는 공리적인 접근이 있었다. 첫번째 공리적 집합론은 체르멜로에 의해 만들어졌고 이후에 다양한 공리적 집합론들이 만들어졌다. (직관주의) 모순에 대한 급진적인 접근도 있었는데, 그것은 직관주의이다. 직관주의는 \(P\) 는 참이거나 거짓이라는 배중률 같은 논리학의 보편적인 기본 원리들을 부정했다.

진리는 무엇인가? 참과 거짓이란 근본적으로 무엇인가? 어떤 것이 참되다는 것을 어떻게 증명할 수 있는가? 타당한 증명이란 무엇인가?

기호 논리는 연역적 생각의 수학 모델이다. 확률론이 확률적이고 불확실한 상황의 모델인 것처럼 말이다. 모델은 어떻게 만들어지는가? 비행기 같은 자연 대상으로부터 시작하여 본질적이라고 판단되는 대상의 특성을 추출한다. 가령 비행기의 모양을 제외하고 비행기의 나머지 속성을 다 제거하는 것이다.

자연 대상의 모델을 만들면 수학적으로 다루기 쉬워진다. 옛부터 인류는 자연 대상을 모델링하여 발전해왔다. 가령, 지구와 해와 달을 직접 다룰 수 없으니 그것을 원과 원들의 관계로 추상화시켰다. 이것은 행성을 행성의 무게, 실제 크기, 그 안에 있는 디테일한 내용물들을 모두 제거하고 원이라는 수학적 대상으로 변환시킨 것이다. 이렇게 자연 대상을 수학의 세계로 끌어내리면 수학의 세계는 매우 명료하고 구체적이며 어둠이 없으며 말싸움도 논쟁도 전쟁도 없기 때문에 대상을 효과적으로 다룰 수 있다. 그리고 이미 수학의 세계에 수천년간 쌓여온 강력한 도구들을 사용할 수 있다. 또한, 수학의 세계로 이끌어내린 것들은 기계화시키기에도 편하고, 또는 기계화 가능한지 따지는 것도 편하다.

이제 우리는 처음에 했던 질문에 대한 대답이 무엇인지 논해보기 위하여 인간의 생각을 추상화시켜서 모델링하고 결국 수학적 대상으로 만들 것이다. 이로써 우리가 무엇을 참되다고 생각하고, 거짓되다고 생각하며, 참된 것들은 어떻게 증명할 수 있고, 혹은 증명 불가능하지만 참되다고 할 수 있는 것들이 존재하는지에 대해서 논해볼 것이다.

인간의 생각은 그 자체로써 이미 비행기나 행성 보다 더 추상적이다. 그래서 인간의 생각을 추상화하는 작업은 다른 물리적 대상을 추상화하는 작업보다 더욱 어려울 수 있지만, 더욱 고귀하고 가치있는 작업이다. 가령, 우리는 다음과 같이 생각한다.

1. 모든 인간은 죽는다.
2. 소크라테스는 인간이다.
3. 소크라테스는 죽는다.

공리적 수학은 이런 유의 연역으로 구성되어 있다. 이 연역은 그 특성이 모델(수학적 대상)로 사상될 수 있는 현실 세계의 자연 대상의 실제를 구성한다.

우리는 이렇게 연역된 논리를 참되다고 생각한다. 하지만 이 논리의 참됨은 소크라테스의 특성 같은 문장의 내부적인 의미에 의존하지 않고, 문장의 형태와 구조에 의존한다. 그러므로 "소크라테스" 나 "죽음" 의 의미 같은 문장 내부적 의미가 중요한 것이 아니라 "모든" 이라는 단어가 중요하다.

하지만 이 표준이 아직은 애매하다. 그러므로 우리의 목적은 모델 안에서 정확한 표준을 정립하는 것이다. 구체적으로 말하면 다음과 같은 질문에 대답하는 것이다.

1. 어떤 문장에서 다른 문장으로 논리적으로 넘어가는 것은 어떤 것인가?
2. 어떤 문장에서 다른 문장으로 논리적으로 넘어갔다면, 이 사실을 정립하기 위한 증명이란 어떤 것인가?
3. 공리 체계에서 증명할 수 있는 것과 진리 사이에 괴리가 존재하는가? 즉, 참이라고 믿을 수 있는 사실들은 모두 증명가능한가?
4. 논리와 계산가능성의 관계는 무엇인가?

3) 의 질문에 대한 대답은 중요한데, 진리를 밝혀내기 위하여 항상 증명에 의존해도 되는지 여부를 결정해주기 때문이다.

이제 우리는 두 가지 모델을 살펴본다. 첫번째는 명제 논리(sentential logic, propositional logic)이고, 두번째는 1차 논리(first-order logic)이다. 명제 논리는 간단하지만 유의미한 연역을 다룰 수 없다. 1차 논리는 수학에서의 수행해야 하는 연역을 다루기에 적합하다. 그래서 수학자가 집합론의 공리에서 도출된 문장을 1차 논리로 다룰 수 있다.

형식 언어(informal language)를 사용하면 자연 언어에 남아있는 모호함과 어두움을 제거할 수 있다. 형식 언어를 사용하는 대표적인 대상은 컴퓨터이다. 가령, 컴퓨터는 다음과 같은 형식 언어를 사용한다.

프로그래밍 언어는 가령 다음과 같은 형식 언어를 사용한다.

프로그래머는 자신의 생각을 이 형식 언어로 변환해시켜야만 컴퓨터를 다룰 수 있다. 반면 형식 언어를 다시 자연어로 격상시킬 수 있다면 더욱 놀라운 일들을 할 수 있다.

컴퓨터가 사용하는 이러한 형식 언어에 대해서는 컴퓨터를 모델링한 튜링의 논문을 보면서 더 심도있게 살펴보기로 하고, 지금은 인간의 생각을 논리로 정형화시켜서 나타내어줄 수 있는 형식 언어를 구성하려 한다. 첫 시작은 명제 논리(sentential logic, propositional logic)이다.

Propositional Calculus✔

• \(A = F\) 일 때는 \(B\) 와 관계 없이 참이 된다. 만약 \(A = F\) 일 때 \(A \implies B\) 를 거짓으로 정의하면 "임의의 \(x\) 에 대하여, \(x\) 가 홀수이면 \(x ^{2}\) 도 홀수이다" 라는 일반적인 명제를 선언할 수 없다. 왜냐하면 \(x\) 가 짝수인 경우 이 명제 자체가 거짓이 되기 때문이다.

• 함의는 다음과 같은 진리표를 갖는다.

  \(A\)	\(B\)	\(A \implies B\)
  \(T\)	\(T\)	\(T\)
  \(F\)	\(T\)	\(T\)
  \(T\)	\(F\)	\(F\)
  \(F\)	\(F\)	\(T\)

  그러므로 \(A \implies B\) 는 \(\neg A \lor B\) 와 같다.

• 명제가 진리 함수이다.

  가령, \(((A \iff B) \implies ((\neg A) \land B))\) 는 다음과 같은 진리표를 갖는다.

  \(A\)	\(B\)	\((A \iff B)\)	\((\neg A)\)	\(((\neg A) \land B)\)	\(((A \iff B) \implies ((\neg A) \land B))\)
  \(T\)	\(T\)	\(T\)	\(F\)	\(F\)	\(F\)
  \(F\)	\(T\)	\(F\)	\(T\)	\(T\)	\(T\)
  \(T\)	\(F\)	\(F\)	\(F\)	\(F\)	\(T\)
  \(F\)	\(F\)	\(T\)	\(T\)	\(F\)	\(F\)

  그러면 \(((A \iff B) \implies ((\neg A) \land B))\) 를 진리값 \(2\) 개를 받아서 진리값을 출력하는 진리 함수라고 볼 수 있다.

• 예시

  \(A \lor \neg A\)

• 예시

  \(A \land B \vDash A\)

• 예시

  \(A \vDash \Dashv\neg (\neg A)\)

• 증명

• 예시

  \(A \iff \neg A\) 는 모순이다.

• 모순으로부터 얻은 문장을 논리적으로 거짓이라고 한다.

• 예시

  항진식 \(((A \lor B) \land \neg B) \implies A\) 을 단어들로 치환하여 "만약 비가 오거나 눈이 오고, 그리고 눈이 오지 않으면, 비가 오는 것이다" 는 논리적으로 진실이다.

• 증명

• 증명

• 증명

• 예시

  다음이 연산된다.

  \[ \begin{align}\begin{split} &A \iff (\neg B) \lor C \implies A \\ &A \iff ((\neg B) \lor C) \implies A \\ &A \iff (((\neg B) \lor C) \implies A) \\ \end{split}\end{align} \tag*{} \]

• 예시

  다음과 같이 연산된다.

  \[ \begin{align}\begin{split} & A \implies \neg B \implies C \\ & A \implies (\neg B) \implies C \\ & (A \implies (\neg B)) \implies C \\ \end{split}\end{align} \tag*{} \]

• 이 정리는 임의의 명제 \(x_1, x_2, \dots, x_n\) 의 진리값 할당에 대응되는 진리 함수를 우리가 완전히 인위적으로 만들어내어도 그 진리 함수가 성분 명제들을 \(\neg , \land ,\lor\) 로 연결한 형태로 이루어져있다는 것을 보장해준다.

  이 정리는 컴퓨터를 구성할 때 가장 기초적인 논리 게이트에서 사용된다.

• 증명

  진리 함수 \(f(x_1, \dots, x_n)\) 를 잡자. \(f\) 는 \(2 ^{n}\) 행을 갖는 진리표로 표현된다. 각 행은 변수 \(x_1, \dots, x_n\) 에 할당되는 진리값을 나타낸다. \(1 \leq i \leq 2 ^{n}\) 에 대하여 \(C_i\) 를 \(U _{1}^{i}\land U _{2}^{i} \land \dots \land U _{n}^{i}\) 로 정의하자. \(U _{j}^{i}\) 는 \(i\)번째 행의 \(x_j\) 가 \(T\) 이면 \(A_j\) 가 되고, \(F\) 이면 \(\lnot A_j\) 가 된다. \(A_i\) 란 진리값 \(x_i\) 를 부여받는 명제이다.

  이제 \(D\) 를 \(f\) 가 \(i\)번째 행에서 \(T\) 값을 갖는 모든 \(C_i\) 의 분리로 정의하자. 만약 \(f\) 가 모든 행에서 \(F\) 값을 가지면 \(D\) 를 \(A_1 \land \lnot A_1\) 로 정의하면 정리가 성립한다.

  \(D\) 는 \(\lnot , \land ,\lor\) 만을 포함한다. \(D\) 가 \(f\) 에 대응되는 진리함수라는 것을 보이기 위하여 명제 기호 \(A_1, \dots, A_n\) 에 대한 진리값 할당을 잡고, 이 할당이 \(f\) 에 대한 진리표의 \(k\)행에 해당하는 변수 \(x_1, \dots, x_n\) 에 대한 할당이라고 하자.

  그러면 \(C_k\) 는 이 할당에 대하여 \(T\) 값을 갖는데 비해, 다른 모든 \(C_i\) 는 \(F\) 값을 가진다. \(f\) 가 \(k\)행에서 \(T\) 값을 가지면 \(C_k\) 는 \(D\) 의 분리에 속하고, 그러므로 \(D\) 는 이 할당에서 \(T\) 값을 가진다.

  \(F\) 가 \(k\)행에서 \(F\) 값을 가지면 \(C_k\) 는 \(D\) 의 분리에 포함되지 않고 나머지 \(C_i\) 들이 이 할당에서 \(F\) 값을 가진다. 그러므로 \(D\) 는 \(F\) 값을 가진다. 따라서 \(D\) 는 진리함수 \(f\) 를 생성한다. ■

• 예시

  \(x_1\)	\(x_2\)	\(f(x_1, x_2)\)
  \(T\)	\(T\)	\(F\)
  \(F\)	\(T\)	\(T\)
  \(T\)	\(F\)	\(T\)
  \(F\)	\(F\)	\(T\)

  본 정리의 증명은 위와 같이 형성되는 진리 함수를 다음과 같은 \(D\) 로 표현할 수 있다는 것을 일반적으로 설명한 것이다.

  \[ \overbrace{(\lnot A_1 \land A_2)}^{C_2} \lor \overbrace{(A_1 \land \lnot A_2)}^{C_3} \lor \overbrace{(\lnot A_1 \land \lnot A_2)}^{C_4} \]

• 이 정리는 컴퓨터를 구성하는 논리게이트의 기초 블록의 본질의 선택지를 알려준다.

• 증명

  \[ B \land C \iff \lnot (\lnot B \lor \lnot C) \]
  \[ B \lor C \iff (\lnot B \implies C) \]
  \[ B \land C \iff \lnot (B \implies \lnot C) \]

  ■

• 예시

  \(A \darr B\) 는 \(A, B\) 둘 다 거짓일 때에만 참이된다.

  \(A\)	\(B\)	\(A \darr B\)
  \(T\)	\(T\)	\(F\)
  \(F\)	\(T\)	\(F\)
  \(T\)	\(F\)	\(F\)
  \(F\)	\(F\)	\(T\)

• 예시

  \(A | B\) 는 \(A, B\) 둘 다 참일 때에만 거짓이다.

  \(A\)	\(B\)	\(A \vert B\)
  \(T\)	\(T\)	\(F\)
  \(F\)	\(T\)	\(T\)
  \(T\)	\(F\)	\(T\)
  \(F\)	\(F\)	\(T\)

• 이 정리는 nor 이나 nand 만 사용하여 모든 진리 함수를 구현할 수 있음을 보장한다.

  nand2tetris 는 nand 게이트만 사용하여 컴퓨터를 구성하고 테트리스 프로그램까지 만들어 보이는 프로젝트이다.

• 증명

  \(h(A,B)\) 가 모든 진리함수를 구성해낼 수 있는 논리 접속사라고 하자. \(h(T,T)\) 가 \(T\) 라면, \(h\) 를 사용하여 구성된 임의의 명제는 그것의 모든 명제 기호가 \(T\) 값을 가질 때 \(T\) 값을 갖는다. 그러므로 \(\lnot A\) 는 \(h\) 로 정의불가능하다. 그러므로 \(h(T,T) = F\) 이다. 비슷한 논리로 \(h(F,F) = T\) 이다. 따라서 다음과 같은 부분 진리표를 얻는다.

  \(A\)	\(B\)	\(h(A, B)\)
  \(T\)	\(T\)	\(F\)
  \(F\)	\(T\)
  \(T\)	\(F\)
  \(F\)	\(F\)	\(T\)

  2,3행의 마지막 열이 \(F,F\) 또는 \(T,T\) 이면 \(h\) 는 \(\darr\) 또는 \(|\) 이다.

  (그러면 \(|\) 로 \(\lnot x := x|x\) 이고 \(x \land y := \lnot (x | y)\) 와 같이 \(\lnot\) 과 \(\land\) 가 정의가능하므로 정리 1.6 에 의하여 모든 진리 함수를 구성할 수 있다. \(\darr\) 도 마찬가지.)

  만약 \(F,T\) 이면 \(h(A, B) \iff \lnot B\) 이고, \(T,F\) 이면 \(h(A,B) \iff \lnot A\) 이다. 두 경우 모두 \(h\) 가 \(\lnot\) 으로 정의가능하다. 그러나 \(\lnot\) 단독적으로는 일변수 진리함수만 정의가능하고, 그것은 항등함수와 부정함수인데, 이것으로는 항상 \(T\) 값을 갖는 진리함수를 정의할 수 없다. ■

Formal Theory✔

• 4) 에 대한 예시로써 추론 규칙인 긍정 논법(modus ponens)을 생각하자. 긍정 논법은 \(B\) 와 \(B \implies C\) 가 참이면 \(C\) 도 참이라는 추론규칙이다. 이 규칙은 wff 의 관계로 정의되며, 임의의 wff \(B, C\) 에 대한 튜플 \(\left< B, B \implies C, C \right>\) 로 표기한다.

• 결정가능한 이론의 어떤 wff 가 정리인지 기계가 검증할 수 있고, 결정불가능한 이론의 wff 가 정리인지 결정하려면 어떤 독창성이 필요하다.

• \(\Gamma \vdash C\) 라고 하면 \(C\) 가 \(\Gamma\) 로부터 증명가능하다는 말이다.

• \(\Gamma\) 가 유한 집합 \(\{H_1, H_2, \dots, H_m\}\) 이면 \(\{H_1, H_2, \dots, H_m\} \vdash C\) 라고 표기하지 않고 \(H_1, H_2, \dots, H_m \vdash C\) 라고 표기한다.

• \(\Gamma = \varnothing\) 이면 \(\varnothing \vdash C\) 인 것과 \(C\) 가 정리인 것은 동치이다. 관례적으로 \(\varnothing\) 은 생략하고 \(\vdash C\) 라고 표기한다. 따라서 \(\vdash C\) 라고 하면 \(C\) 가 정리인 것이다.

• 귀결과 관련하여 다음이 성립한다.

  1. \(\Gamma \subset \Delta\) 이고 \(\Gamma \vdash C\) 이면 \(\Delta \vdash C\) 이다.
  2. \(\Gamma \vdash C\) 인 것은 \(\Delta \vdash C\) 인 \(\Gamma\) 의 유한 부분 집합 \(\Delta\) 가 존재하는 것과 동치이다.
  3. \(\Delta \vdash C\) 이고 각 \(B \in \Delta\) 에 대하여 \(\Gamma \vdash B\) 이면 \(\Gamma \vdash C\) 이다.

Propositional Calculus Theory✔

• 이렇게 정의된 공리가 타당하고, 추론규칙이 타당성을 보존한다는 보장이 필요하다. 이 역할을 해주는 것이 체계의 건전성 정리이다. 그러므로 건전성은 형식 체계에서 반드시 성립해야 하는 성질이다.

• 세 공리꼴(axiom schema) \((A1), (A2), (A3)\) 로부터 무한한 공리 집합이 주어진다. 임의의 wff 가 주어지면 그 wff 가 공리인지 아닌지 확인할 수 있으므로 \(L\) 은 공리적이다. 이제 우리의 목적은 모든 항진식을 정리로 만드는 것이다.

  그러나 이 공리꼴로 구성된 명제 논리가 유일한 진리가 아니다. 다른 공리를 선택하고, \(\neg , \implies\) 가 아닌 다른 원시 논리 연산을 사용하고도 충분히 명제 논리를 구성할 수 있다.

• 명제 논리의 형식적 공리적 이론에서는 다음과 같이 \(\land , \lor , \iff\) 를 정의한다.

  \[ \begin{align}\begin{split} & (B \land C) := \neg (B \implies \neg C) \\ & (B \lor C) := (\neg B) \implies C \\ & (B \iff C) := (B \implies C) \land (C \implies B) \end{split}\end{align} \tag*{} \]

• 증명

Deduction Theorem✔

• 증명

• 증명

• 증명

• 이 정리가 성립하지 않으면 형식 체계에서 공리에 추론규칙을 적용하여 얻는 정리가 아무런 의미도 갖지 않을 것이다.

  모든 건전성 정리는 공리가 타당하다는 것과 추론규칙이 타당성을 보존한다는 것을 증명함으로써 증명된다. 명제 논리에서 이 증명은 쉽고 간단하다. 증명이 책에 있다.

• 증명

• 예시

  \(B = \neg (\neg A_2 \implies A_5)\) 라고 하면 다음과 같은 진리표를 만들 수 있다.

  \(A_2\)	\(A_5\)	\(\neg (\neg A_2 \implies A_5)\)
  \(T\)	\(T\)	\(F\)
  \(F\)	\(T\)	\(F\)
  \(T\)	\(F\)	\(F\)
  \(F\)	\(F\)	\(T\)

  이 경우 3행에 대해서는 \(A_2 , \neg A_5 \vdash \neg \neg (\neg A_2 \implies A_5)\) 이고 4행에 대해서는 \(\neg A_2 , \neg A_5 \vdash \neg (\neg A_2 \implies A_5)\) 이라는 것이다.

• 증명

Completeness✔

• 이 정리가 명제 논리의 완전성을 보장해준다.

• 증명

  항진식 \(B\) 를 구성하는 명제 \(B_1, B_2, \dots, B_k\) 에 대하여 보조정리 1.13 에 의하여 \(B_1', \dots , B_k' \vdash B\) 가 성립한다. ▲

  \(B'_k = T\) 이면 \(B_1', \dots , B _{k-1}' , B_k \vdash B\) 이고 \(B'_k = F\) 이면 \(B_1', \dots , B _{k-1}' , \neg B_k \vdash B\) 이다. 연역 정리에 의하여 \(B_1', \dots , B _{k-1}' \vdash B_k \implies B\) 이고 \(B_1', \dots , B _{k-1}' \vdash \neg B_k \implies B\) 이다. ▲

  보조정리 1.11(7) 과 MP 에 의하여 다음이 성립한다.

  \[ \begin{align}\begin{split} \quad & (B_k \implies B) \\ \leadsto \quad & (B_k \implies B) \implies (( \neg B_k \implies B) \implies B) \\ \leadsto \quad & (( \neg B_k \implies B) \implies B) \\ \leadsto \quad & B \\ \end{split}\end{align} \tag*{} \]

  그러므로 \(B_1', \dots , B _{k-1}' \vdash B\) 이다. 이 과정을 \(k\) 번 반복하며 \(\vdash\) 왼쪽에 있는 항들을 제거하면, \(\vdash B\) 를 얻는다. ■

• 증명

Consistency✔

• 즉, \(B\) 와 \(\neg B\) 가 모두 \(L\) 의 정리가 되게 하는 wff \(B\) 는 존재하지 않는다. 이로써 이 정리는 명제 논리가 모순을 내뱉지 않는 체계라는 것을 보장해준다. 무모순성 정리가 있어야 수학자들은 해당 체계를 안심하고 사용할 수 있다. 그 체계가 언젠가 무너져내릴 것이라는 걱정 없이.

• \(L\) 이 무모순이면 정리가 아닌 wff 가 존재한다. 가령 정리의 부정은 정리가 아니다.

  모든 wff 가 정리가 아닌 이론을 완전히 무모순(absolutely consistent)이라고 하고, 이 정의는 부정 기호를 포함하지 않는 이론에도 적용된다.

• 보조정리 1.11(3) 에 의하여 \(\neg B \implies (B \implies C)\) 인데, \(L\) 이 모순을 도출하면 wff \(B\) 와 그 부정 \(\neg B\) 도 증명되므로 MP 에 의하여 wff \(C\) 가 증명된다. \(C\) 는 명제 변수이므로 이는 곧, 모순적인 이론에서는 임의의 명제가 증명가능한 진실이 된다는 것이다. 그러므로 모순적인 체계에서는 아무리 말도 안되는 말이나, 아무리 편향적인 말이나, 아무리 거짓된 말이라도 증명가능하다.

  이 사실은 MP 를 추론 규칙으로 가지며, 보조정리 1.11(3) 이 증명가능한 이론에서 항상 성립한다.

• 증명

  정리 1.12 에 의하여 \(L\) 의 모든 정리는 항진식이므로 항진식의 부정은 정리가 될 수 없다. 따라서 \(B\) 나 \(\neg B\) 모두 \(L\) 의 정리가 될 수 없다. ■

Independence✔

• 다음의 증명은 3개의 진리값을 사용한다. 이렇게 여러 진리값을 사용하는 것을 다치논리(Many-valued logic)라고 한다.

• 증명

  공리꼴 \((A1) (B \implies (C \implies B))\) 의 독립성을 증명하기 위하여 다음의 진리표를 생각하자.

  \(A\)	\(\neg A\)		\(A\)	\(B\)	\(A \implies B\)
  \(0\)	\(1\)		\(0\)	\(0\)	\(0\)
  \(1\)	\(1\)		\(1\)	\(0\)	\(2\)
  \(2\)	\(0\)		\(2\)	\(0\)	\(0\)
  			\(0\)	\(1\)	\(2\)
  			\(1\)	\(1\)	\(2\)
  			\(2\)	\(1\)	\(0\)
  			\(0\)	\(2\)	\(2\)
  			\(1\)	\(2\)	\(0\)
  			\(2\)	\(2\)	\(0\)

  명제논리는 \(\neg\) 과 \(\implies\) 의 진리값만 정의되면 형성될 수 있으므로 이렇게 진리값을 이렇게 정의해도 괜찮다.

  wff \(B\) 의 명제 성분에 \(0, 1, 2\) 로 진리값 할당을 했는데 \(B\) 가 항상 \(0\) 이면 \(B\) 를 선택되었다고 하자. 그런데 \(B\) 와 \(B \implies C\) 가 선택되었으면 \(C\) 도 선택되었으므로 MP 는 선택성을 보존한다. 그러므로 공리꼴 \((A2), (A3)\) 의 인스턴스는 모두 선택되었다. 하지만 \((A1)\) 의 경우 \(B = 1, C = 2\) 일 경우 진리값이 \(2\) 가 되므로 선택되지 않았다. 그러므로 \((A1)\) 은 독립적이다. ▲

  공리꼴 \((A2) ((B \implies (C \implies D)) \implies ((B \implies C) \implies (B \implies D)))\) 의 독립성을 증명하기 위하여 다음의 진리표를 생각하자.

  \(A\)	\(\neg A\)		\(A\)	\(B\)	\(A \implies B\)
  \(0\)	\(1\)		\(0\)	\(0\)	\(0\)
  \(1\)	\(0\)		\(1\)	\(0\)	\(0\)
  \(2\)	\(1\)		\(2\)	\(0\)	\(0\)
  			\(0\)	\(1\)	\(2\)
  			\(1\)	\(1\)	\(2\)
  			\(2\)	\(1\)	\(0\)
  			\(0\)	\(2\)	\(1\)
  			\(1\)	\(2\)	\(0\)
  			\(2\)	\(2\)	\(0\)

  진리값 할당에 의하여 항상 진리값 \(0\) 을 갖는 명제를 그로테스크하다고 하자. MP 는 \((A1), (A3)\) 의 그로테스크함을 보존한다. 하지만 공리꼴 \((A2)\) 는 \(B = 0, C = 0, D = 1\) 이면 진리값 \(2\) 를 가지므로 그로테스크하지 않다. 그러므로 \((A2)\) 는 독립적이다. ▲

  \((A3) ((( \neg C) \implies (\neg B)) \implies (((\neg C) \implies B) \implies C))\) 의 독립성을 증명해보자.

  어떤 명제 \(B\) 의 모든 부정 기호를 제거하여 얻은 \(h(B)\) 가 항진식이면 \(B\) 를 강력하다고 하자. 공리꼴 \((A1), (A2)\) 는 강력하다. 또한 \(h(B \implies C)\) 와 \(h(B)\) 가 항진식이면 \(h(C)\) 도 항진식이므로 MP 는 강력함을 보존한다. 왜냐하면 \(h(B \implies C) = h(B) \implies h(C)\) 이고 정리 1.2 이기 때문이다. 따라서 \((A1), (A2)\) 에서 MP 로 도출된 wff 는 강력하다. 하지만 \((A3)\) 은 부정 기호에 의존적이어서 강력하지 않다. 그러므로 \((A3)\) 는 \((A1), (A2)\) 에서 증명될 수 없고, 이에 따라 독립적이다. ■

First-Order Logic✔

• 1차 논리 식 \(P(a)\) 에서 기호 \(P\) 는 개별 상수 \(a\) 에 적용되는 술어이다. 의미론적으로 술어는 관계로 해석된다. 아래에서 해석(구조)에서 보면, 술어는 n항관계, 즉, 곱집합의 부분집합으로 해석된다. 가령, 술어 \(\operatorname{father}\) 에 대한 식 \(\operatorname{father}(John)\) 은 John 의 아버지에 해당하는 객체를 나타낸다.

  명제 논리는 문장 전체를 다룰 수밖에 없었지만, 주어와 술어 구조에서 주어가 되는 객체에 양화사를 적용하여 술어 논리를 얻을 수 있다. 술어 논리는 1차 논리, 2차 논리, 고차 논리가 있다. 이 중 1차 논리에서는 완전성, 건전성 등 주요한 성질들이 성립하여 수학의 기초로 채택되었다.

  술어 논리에서 명제를 술어와 객체로 분리하여 표현하는데, 술어는 하나 이상의 객체를 수식한다. 객체는 상수가 될 수 있고 변수가 될 수도 있다.

  가령, 명제 논리에서 명제 "사과는 과일이다" 와 "오렌지는 과일이다" 의 내부구조를 분석할 수 없다. 그러나 술어 논리에서는 객체와 술어를 분리하여 \(\operatorname{fruit}(apple)\), \(\operatorname{fruit}(orange)\) 와 같이 나타낼 수 있고, "모든 과일은 떨어진다" 를 \(\forall x(\operatorname{fruit}(x) \to \operatorname{fall}(x))\) 라는 식으로 나타낼 수 있다.

• 명제 논리만으로는 복잡한 명제를 효과적으로 표현할 수 없다. 1차 논리는 양화사로 변수의 영역을 특정할 수 있다.

• \(\forall\) 과 \(\exists\) 의 부정 관계에 대한 이해는 다음과 같은 방식으로도 이해될 수 있다. 먼저 \((\forall x)P(x)\) 는 다음과 같이 모든 \(P(x)\) 의 \(\land\) 연산으로 볼 수 있다.

  \[ (\forall x)P(x) = P(x_1) \land P(x_2) \land \dots \land P(x_i) \land \dots \]

  \((\exists x)P(x)\) 는 다음과 같이 모든 \(P(x)\) 의 \(\lor\) 연산으로 볼 수 있다.

  \[ (\exists x)P(x) = P(x_1) \lor P(x_2) \lor \dots \lor P(x_i) \lor \dots \]

  그러면 드모르간의 법칙을 생각하면 두 명제의 관계가 쉽게 이해된다.

• \(\land , \lor , \iff\) 는 명제 논리 이론 \(L\) 에서처럼 정의된다. 또한, \(\exists\) 를 \(\forall\) 을 기반으로 정의할 수 있으므로 \(\exists\) 도 원시 기호로 채택할 필요 없다.

• 괄호를 생략하는 관례도 명제 논리의 그것을 따른다. 다만, 양화사를 괄호 우선순위 리스트에 추가하면 다음과 같이 된다.

  \[\neg , \land , \lor , \forall , \exists , \implies , \iff\]

  또한, 논리 연산 기호들이 나열되어 있을 때 왼쪽에서 오른쪽으로 연산했지만, 부정과 양화사가 연속적으로 있을 때 오른쪽에서 왼쪽으로 연산한다. 가령 다음과 같이 연산된다.

  \[ \begin{align}\begin{split} & (\forall x_1) \neg (\exists x_2)A _{1}^{2}(x_1, x_2) \\ & (\forall x_1) \neg ((\exists x_2)A _{1}^{2}(x_1, x_2)) \\ & (\forall x_1) (\neg ((\exists x_2)A _{1}^{2}(x_1, x_2))) \\ & ((\forall x_1) (\neg ((\exists x_2)A _{1}^{2}(x_1, x_2)))) \\ \end{split}\end{align} \tag*{} \]

• 가령, \(A _{1}^{2}(x_1, x_2)\) 에서 변수 \(x_1\) 은 양화사에 지칭되지 않고 자유로 나타나므로, \(x_1\) 은 자유변수이다. 양화사 \(\forall\) 이나 \(\exists\) 에 의하여 지칭되면 종속된 변수이므로 종속변수라고 한다.

  \(A _{1}^{2}(x_1, x_2) \implies (\forall x_1)(A _{1}^{1}(x_1))\) 에서 \(x_1\) 은 첫번째로 나타날 때 자유이지만 두번째, 세번째에서는 종속이다. 이때 \(x_1\) 은 동시에 자유변수이면서 종속변수이다.

• wff \(B\) 에서 변수 \(x_1, x_2, \dots, x_k\) 들이 자유변수이면 \(B\) 를 \(B(x_1, x_2, \dots, x_k)\) 라고 표기한다. 이것은 \(B\) 가 다른 자유변수를 갖지 않는다는 것이 아니다. 이렇게 표기하면 \(x_1, x_2, \dots, x_k\) 를 항 \(t_1, t_2, \dots, t_k\) 로 치환했다는 의미로 \(B(t_1, t_2, \dots, t_k)\) 라고 표기할 수 있다.

• wff \(B\) 와 항 \(t\) 에 대하여 \(B\) 의 자유변수 \(x_i\) 가 \(t\) 의 변수 \(x_j\) 의 양화사 \(\forall x_j\) 의 범위 안에 있지 않다면, \(t\) 를 \(B\) 에서 \(x_i\) 에 대하여 자유롭다고 한다. 이것의 의미는 \(t\) 가 \(B(x_i)\) 의 자유변수 \(x_i\) 에 대하여 치환되면, \(t\) 의 변수가 \(B(t)\) 에서 종속이 되지 않는다는 것이다.

• 예시

  항 \(x_2\) 는 \(A _{1}^{1}(x_1)\) 에서 \(x_1\) 에 대하여 자유롭지만, \((\forall x_2)A _{1}^{1}(x_1)\) 에서 \(x_1\) 에 대하여 자유롭지 못하다.

  항 \(f _{1}^{2}(x_1, x_3)\) 는 \((\forall x_2)A _{1}^{2}(x_1, x_2) \implies A _{1}^{1}(x_1)\) 에서 \(x_1\) 에 대하여 자유롭지만, \((\exists x_3)(\forall x_2)A_1 ^{2}(x_1, x_2) \implies A _{1}^{1}(x_1)\) 에서 \(x_1\) 에 대하여 자유롭지 않다.

• 그렇다면 다음의 사실은 자명하다.

  1. 변수가 없는 항은 임의의 wff 의 임의의 변수에 대하여 자유롭다.
  2. 항 \(t\) 의 어떠한 변수도 \(B\) 안에서 종속이 아니면 \(B\) 의 임의의 변수에 대하여 자유롭다.
  3. \(x\) 는 임의의 wff 에서 \(x_i\) 에 대하여 자유롭다.
  4. \(B\) 에 자유변수 \(x\) 가 있지 않으면 임의의 항은 \(B\) 에서 \(x\) 에 대하여 자유롭다.

First-Order Languages✔

wff 는 기호에 대한 해석이 주어졌을 때에만 의미를 갖는다. 우리는 보통 wff 의 기호가 특정 언어(language)로부터 왔을 때의 해석에 관심이 있다. 이제 1차 논리 언어를 정의하자.

• 언어를 고정시키고, 그 언어를 기반으로 하는 무한히 많은 이론을 생성할 수 있다.

• 이때 1차 논리 언어로 만들어진 wff 들은 완전히 무의미한 기호 나열에 불과하다. 언어에 해석이 부여되어야만 wff 들이 비로소 의미를 부여받는다.

• 상수, 함수, 술어 기호를 비논리적 상수(nonlogical constant, 비논리 기호)라고 한다. 비논리 기호는 이론에 따라 달라진다.

• 예시

  수론은 \(+\) 이나 \(\cdot\) 의 함수 기호를 포함하고 \(=\) 의 술어 기호를 포함할 것이다. 그러나 군론은 수론과 같이 않은 비논리 기호를 갖는다.

먼저, 1차 논리의 의미론적 접근을 알아보자.

Interpretations✔

• 이 해석이 주어져야 wff 가 비로소 의미를 부여받는다.

• 해석이 주어지면 변수는 영역 \(D\) 의 범위 안에 있다고 생각하면 된다.

• 예시

  영역 \(D\) 가 인간이라면 이항관계 "~의 아버지는 ~이다" 는 \(x\) 가 \(y\) 의 아버지임을 뜻하는 모든 순서쌍 \(\left< x,y \right>\) 의 집합이 된다.

• 예시

  다음과 같은 wff 를 생각하자.

  1. \(A(x_1, x_2)\)
  2. \((\forall x_2)A(x_1, x_2)\)
  3. \((\exists x_1)(\forall x_2)A(x_1, x_2)\)

  이 wff 들은 아직 아무런 의미도 없는 무의미한 기호 나열에 불과하다.

  영역을 양의 정수 \(\Bbb{Z}_{+}\) 로 정하고, \(A(y, z)\) 를 \(y \leq z\) 라고 해석해보자. 그러면 이 해석은 술어기호 \(A\) 에 \(\Bbb{Z}_{+}\) 의 이항관계 \(\leq\) 를 할당한 것이다. 그러면 wff 1 은 \(x_1 \leq x_2\) 로 해석되고, \(a \leq b\) 를 만족하는 양의 정수 순서쌍 \(\left< a,b \right>\) 에 대하여 성립한다. wff 2 는 정수 \(1\) 에 대해서만 성립하고, wff 3 은 가장 작은 양의 정수가 존재한다고 주장하는 문장이다.

• 문장은 참이나 거짓인 명제와도 같다. 그에 비해 wff 는 자유 변수에 따라 참이나 거짓이 될 수 있다.

Satisfaction✔

• 진리란 무엇인가? 무엇이 참이고 무엇이 거짓이라고 말할 수 있는가? 참과 거짓을 정의하기 위해서는 먼저 이렇게 만족의 개념을 정의해야 한다.

• \(s ^{*}(t)\) 란 단지 \(t\) 의 모든 변수 \(x_j\) 들을 열 \(s\) 의 원소 \(s_j\) 로 치환하고, \(t\) 의 함수 기호를 해석에 대응되는 연산으로 치환한 \(D\) 의 원소에 불과하다.

  • 예시

    \(t\) 가 \(f _{2}^{2}(x_3, f _{1}^{2}(x_1, a_1))\) 이고, 해석의 영역이 \(\Bbb{Z}\) 이고, \(f _{2}^{2}, f _{1}^{2}\) 이 각각 \(\cdot , +\) 로 해석되고, \(a_1\) 이 \(2\) 로 해석된다면, 임의의 정수열 \(s = (s_1, s_2, \dots)\) 에 대하여 \(s ^{*}(t) = s_3 \cdot (s_1 + 2) \in \Bbb{Z}\) 이다.

• 그래서 쉽게 말해, 열 \(s = (s_1, s_2, \dots)\) 이 wff \(B\) 를 만족한다는 것은 각 \(i\) 에 대하여 \(B\) 의 모든 자유 변수 \(x_i\) 를 \(s_i\) 로 치환하여 얻은 명제가 주어진 해석에서 참되다는 것이다.

• 만족가능성과 진리가 직관적으로 명료한 개념이지만 이렇게 엄밀한 정의도 내려야만 다양한 수학적 결과에 대한 정확한 증명을 수행할 수 있다.

• 예시

  해석의 영역이 실수 집합 \(\R\) 이고 \(A _{1}^{2}\) 의 해석이 관계 \(\leq\) 이고 \(f _{1}^{1}\) 의 해석이 함수 \(e ^{x}\) 이면 실수열 \(s = (s_1, s_2, \dots )\) 이 \(A _{1}^{2}(f _{1}^{1}(x_2), x_5)\) 를 만족시킨다는 것은 \(e ^{s_2} \leq s_5\) 인 것과 동치이다.

  영역이 정수 집합 \(\Bbb{Z}\) 이고 \(A _{1}^{4}(x,y,u,v)\) 의 해석이 \(x \cdot v = u \cdot y\) 이고 \(a_1\) 의 해석이 \(3\) 이면 정수열 \(s = (s_1, s_2, \dots )\) 이 \(A _{1}^{4}(x_3, a_1, x_1, x_3)\) 을 만족시킨다는 것은 \((s_3) ^{2} = 3s_1\) 과 동치이다.

Truth, Falsity, Model✔

• 진리란 무엇인가? 무엇이 참이고 무엇이 거짓이라고 말할 수 있는가? 먼저 정의된 만족의 개념을 기반으로 이렇게 참과 거짓의 개념을 정의할 수 있다.

• 변수 \(x _{i_1}, \dots , x _{i_k}\) 에 대하여 \(B(x _{i_1}, \dots , x _{i_k})\) 를 오직 \(x _{i_1}, \dots , x _{i_k}\) 만을 자유변수로 갖는 wff 라고 하자.

• 예시

  \(B\) 가 \(A _{1}^{2}(x_2, x_5) \implies \neg (\exists x_2)A _{1}^{3}(x_1,x_2,x_3)\) 이면 이것의 폐포는 \((\forall x_5)(\forall x_3)(\forall x_2)(\forall x_1)B\) 이다.

• 6) 에 의하여 \(B\) 가 참인 것과 \(B\) 의 폐포가 참인 것은 동치이다.

• 7) 에서 명제의 인스턴스는 명제의 모든 명제 기호를 wff 들로 치환하여 얻은 wff 이다.

  가령, \(A_1 \implies \neg A_2 \lor A_1\) 의 인스턴스는 \(A _{1}^{1}(x_2) \implies (\neg (\forall x_1)A _{1}^{1}(x_1)) \lor A _{1}^{1}(x_2)\) 이다.

• 9) 에서 \(B\) 는 물론 어떤 해석에서 참이지만 어떤 해석에서 거짓일 수 있다.

  가령 wff \(A _{1}^{1}(a_1)\) 에 대하여 해석 \(\mathrm{M}\) 이 영역으로써 \(\Bbb{Z}_{+}\) 를 갖고, \(A _{1}^{1}\) 을 소수의 성질로 해석하고, \(a_1\) 을 \(2\) 로 해석하면 \(A _{1}^{1}(a_1)\) 은 참이다. 그러나 \(a_1\) 을 \(4\) 로 해석하는 해석에서는 거짓이다.

• 11) 을 증명하기 위해서 아래의 두 보조정리가 필요하다.

• 증명

• 증명

• 증명

Validity✔

• 명제 논리의 항진식에 해당하는 개념이다.

• 라이프니츠는 \(B\) 가 논리적으로 타당한 것이 \(B\) 가 가능한 모든 세계에서 참인 것과 동치라고 정의했다.

• wff \(B\) 가 논리적으로 타당한 것은 \(\neg B\) 가 만족불가능한 것과 동치이다. \(B\) 가 만족가능한 것은 \(\neg B\) 가 논리적으로 타당하지 않은 것과 동치이다.

• 닫힌 wff 는 임의의 해석에서 참이거나 거짓이다. 즉, 닫힌 wff 는 모든 열에 의하여 만족가능하거나 그렇지 않다. 따라서 wff \(B\) 가 닫혀있으면 \(B\) 가 만족가능한 것과 \(B\) 가 어떤 해석에서 참인 것은 동치이다.

• wff 집합 \(\Gamma\) 가 만족가능하다는 것은 \(\Gamma\) 의 모든 wff 를 만족시키는 열이 존재하는 해석이 존재하다는 것과 동치이다.

• 이는 \(\neg B\) 가 논리적으로 타당하다는 것과 같다.

First-Order Theories✔

지금까지 1차 논리의 의미론적 접근을 알아보았다. 이제 의미를 배제한 구문론적 접근을 알아보자.

• 1차 이론은 형식 이론을 기반으로 정의된다. 형식 이론에서 정의한 증명, 정리, 귀결 등의 용어를 계속 사용한다.

• 예시

  (부분 순서) 언어 \(\mathcal{L}\) 이 단일 술어 기호 \(A _{2}^{2}\) 를 갖고 함수 기호나 상수를 갖지 않는다고 하자. \(A _{2}^{2}(x_i, x_j)\) 를 \(x_i < x_j\) 라고 쓰자. 이론 \(K\) 가 다음 고유 공리를 갖는다고 하자.

  1. \((\forall x_1)(\neg x_1<x_1)\) (비반사성, irreflexivity)
  2. \((\forall x_1)(\forall x_2)(\forall x_3)(x_1<x_2 \land x_2<x_3 \implies x_1<x_3)\) (추이성, transitivity)

  이 이론의 모델을 부분 순서 구조라고 한다.

• 예시

  (군론) 언어 \(\mathcal{L}\) 이 단일 술어 기호 \(A _{1}^{2}\) 와 단일 함수 기호 \(f _{1}^{2}\) 와 단일 상수 \(a_1\) 를 갖는다고 하자. \(A _{1}^{2}(t, s)\) 를 \(t = s\) 라고 쓰고, \(f _{1}^{2}(t, s)\) 를 \(t + s\) 라고 쓰고, \(a_1\) 를 \(0\) 이라고 쓰자. 군론 \(K\) 는 다음의 고유 공리를 갖는다.

  1. \((\forall x_1)(\forall x_2)(\forall x_3)(x_1 + (x_2 + x_3) = (x_1 + x_2) + x_3)\) (결합성, associativity)
  2. \((\forall x_1)(0 + x_1 = x_1)\) (항등원, identity)
  3. \((\forall x_1)(\exists x_2)(x_2 + x_1 = 0)\) (역원, inverse)
  4. \((\forall x_1)(x_1 = x_1)\) (\(=\) 의 반사성, reflexivity)
  5. \((\forall x_1)(\forall x_2)(x_1 = x_2 \implies x_2 = x_1)\) (\(=\) 의 대칭성, symmetry)
  6. \((\forall x_1)(\forall x_2)(\forall x_3)(x_1 = x_2 \land x_2 = x_3 \implies x_1 = x_3)\) (\(=\) 의 추이성, transitivity)
  7. \((\forall x_1)(\forall x_2)(\forall x_3)(x_2 = x_3 \implies x_1 + x_2 = x_1 + x_3 \land x_2 + x_1 = x_3 + x_1)\) (\(=\) 의 대체성, substitutivity)

  이 이론의 모델을 군(group)이라고 한다. 만약 wff \((\forall x_1)(\forall x_2)(x_1 + x_2 = x_2 + x_1)\) 이 참이면 아벨군(abelian)이라고 한다.

• 부분 순서 이론과 군론은 모두 공리적이다. 일반적으로 유한개의 고유 공리를 갖는 임의의 이론은 공리적이라고 한다. 왜냐하면 주어진 임의의 wff 가 논리적인 공리인지 효과적으로 결정할 수 있기 때문이다.

• 진리의 성질의 3) 과 6) 에 의하여 1차 이론의 모델에서 MP 와 Gen 이 공리에 적용되면 그 결과 또한 모두 참이다. 그러므로 \(K\) 의 모든 정리가 \(K\) 의 모든 모델에서 참이 된다.

이제 \(K\) 를 임의의 1차 이론이라고 하고 \(\vdash _K B\) 라고 표기하는 대신 편하게 \(\vdash B\) 라고 표기하자. 또한, \(\Gamma\) 를 wff 집합으로 생각하고 \(B, C\) 를 wff 로 생각하자.

• 증명

Soundness✔

• 이 정리는 다음과 같이 표현된다.¹

  \[\vdash B \implies \vDash B\]

  건전성 정리는 형식 체계의 구문론적 연역이 의미론적으로 올바른 결론을 이끌어내준다는 것을 보장해준다. 이 정리가 없으면 연역은 무의미하다. 이 정리에 의하여 1차 술어 계산에서 구문론적(syntactic)으로 도달한 명제는 의미론적(semantic)으로도 참이다.

  괴델의 시대에 건전성 정리가 널리 알려져 있었지만 시대는 완전성 정리, 즉 의미론적으로 참인 명제라면 증명가능하다는 보장을 필요로 했다. 결국 괴델은 아래에서 살펴볼 완전성 정리를 증명했다.

• 증명

  먼저 공리가 논리적으로 타당한지 검증하고, 추론 규칙에 의하여 연역된 wff 가 논리적으로 타당한지 검증해보자.

  진리의 성질 7) 에 의하여 공리 \((A1), (A2), (A3)\) 는 논리적으로 타당하고, 성질 10) 과 11) 에 의하여 공리 \((A4), (A5)\) 도 논리적으로 타당하다. ▲

  성질 3), 6) 에 의하여 추론규칙 MP 와 Gen 는 논리적 타당성을 보존한다. ▲

  그러므로 술어 계산의 모든 정리는 논리적으로 타당하다. ■

• 예시

  wff \((\forall x_2)(\exists x_1)A _{1}^{2}(x_1, x_2) \implies (\exists x_1)(\forall x_2) A _{1}^{2}(x_1, x_2)\) 는 논리적으로 타당하지 않으므로 1차 술어 계산의 정리가 아니다.

  해석의 영역을 정수 집합 \(\Bbb{Z}\) 로 잡고 \(A _{1}^{2}(y,z)\) 를 \(y < z\) 로 해석하면 \((\forall x_2)(\exists x_1)A _{1}^{2}(x_1, x_2)\) 는 참이지만 \((\exists x_1)(\forall x_2) A _{1}^{2}(x_1, x_2)\) 는 거짓이다. 전자는 각 정수 \(x_2\) 마다 \(x_2\) 보다 작은 정수의 존재성을 주장하고, 후자는 최소 정수의 존재성을 주장하기 때문이다.

Consistency✔

• 증명

  wff \(B\) 와 \(\neg B\) 가 1차 술어 계산의 정리이면 정리 2.2 건전성 정리에 의하여 \(B\) 와 \(\neg B\) 가 논리적으로 타당하다. 그러나 이는 불가능하다. ■

• 만약 이론 \(K\) 가 모순적이면 \(K\) 의 모든 wff \(C\) 가 \(K\) 에서 증명가능하다. 왜냐하면 \(B\) 와 \(\neg B\) 가 둘 다 증명가능하면, wff \(B \implies (\neg B \implies C)\) 가 항진식의 인스턴스이므로 정리 2.1 에 의하여 \(\vdash C\) 가 도출되기 때문이다. \(C\) 는 문장 변수이므로 모든 wff 가 \(C\) 에 대입될 수 있다.

  그러므로 이론 \(K\) 의 어떤 wff 가 \(K\) 의 정리가 아니라는 것이 증명되면 \(K\) 는 무모순인 것이다.

  명제 논리의 정리 1.9 연역 정리는 1차 논리에서 그대로 사용할 수 없다. 가령, 임의의 wff \(B\) 에 대하여 추론규칙 Gen 에 의하여 \(B \vdash _K (\forall x_i)B\) 이지만, 반드시 \(\vdash _K B \implies (\forall x_i)B\) 가 된다고 할 수 없다. 최소한 두 원소 \(c, d\) 를 포함하는 영역을 두고, \(B\) 가 \(A _{1}^{1}(x_1)\) 라고 하자. 그리고 \(A _{1}^{1}\) 가 오직 \(c\) 에서 성립하도록 해석해보자. 그러면 \(A _{1}^{1}(x_1)\) 는 \(s_1 = c\) 인 임의의 열 \(s = (s_1,s_2,\dots )\) 에 의하여 만족되지만, \((\forall x_1)A _{1}^{1}(x_1)\) 는 만족되지 않는다. 그러므로 \(A _{1}^{1}(x_1) \implies (\forall x_1)A _{1}^{1}(x_1)\) 는 이 해석에서 참이 아니고, 논리적으로 타당하지 않다. 그러므로 정리 2.2 에 의하여 \(A _{1}^{1}(x_1) \implies (\forall x_1)A _{1}^{1}(x_1)\) 는 \(K\) 의 정리가 아니다. 즉, \(\vdash A _{1}^{1}(x_1) \implies (\forall x_1)A _{1}^{1}(x_1)\) 라고 할 수 없다.

• 위 증명 과정에서 알 수 있듯이 추론 규칙 Gen 에 의하여 임의의 wff \(B\) 에 대하여 다음이 성립한다.

  \[ B \vdash (\forall x_i) B \]

  그러나 이 결과에 의하여 다음이 반드시 성립하지는 않는다.

  \[ \vdash B \implies (\forall x_i) B \]

  가령, wff \(x = 0\) 에 대하여 추론 규칙 Gen 에 의하여 다음은 성립한다.

  \[ (x = 0) \vdash (\forall x)(x = 0) \]

  그러나 이 결과에 의하여 다음이 성립하지는 않는다.

  \[ \vdash (x = 0) \implies (\forall x)(x = 0) \]

  \(x = 1\) 인 경우 이 결과는 거짓이 되므로 1차 논리에서 정리가 될 수 없다.

Deduction Rules✔

• 증명

  \(\Gamma\) 와 \(B\) 에서의 \(C\) 에 대한 연역이 \(D_1, D_2, \dots, D_n\) 라고 하자. 즉, \(D_n = C\) 이다.

  귀납적 가정으로써 \(n\) 이하의 연역에서 명제들이 참이라고 가정하자.

  \(C\) 가 \(\Gamma\) 에 속하거나 공리라면 \(\Gamma \vdash C\) 이다. ▲

  \(C\) 가 이전의 한 wff 나 두 wff 로부터 Gen 이나 MP 에 의하여 도출되었다면 \(C\) 가 \(B\) 에 의존하지 않는다는 정리의 가정에 의하여 추론에 사용된 선행 wff 는 \(B\) 가 아니다. 귀납적 가정에 의하여 선행되는 모든 wff 는 오직 \(\Gamma\) 로부터 도출된다. 그러므로 \(\Gamma \vdash C\) 이다. ■

• 증명

  \(\Gamma\) 와 \(B\) 로부터의 \(C\) 에 대한 연역이 \(D_1, D_2, \dots, D_n\) 이라고 하자. 즉, \(D_n = C\) 이다.

  귀납적으로 각 \(i \leq n\) 에 대하여 \(\Gamma \vdash B \implies D_i\) 임을 보이자.

  • \(D_i\) 가 공리이거나 \(\Gamma\) 에 속하면 \(D_i \implies (B \implies D_i)\) 가 공리 \((A1)\) 이므로 \(\Gamma \vdash B \implies D_i\) 이다.

  • \(D_i\) 가 \(B\) 이면 \(B \implies B\) 가 항진식이므로 정리 2.1 에 의하여 \(\vdash B \implies D_i\) 이고, 그러므로 \(\Gamma \vdash B \implies D_i\) 이다.

  • \(i\) 보다 작은 \(j, k\) 에 대하여 \(D_k\) 가 \(D_j \implies D_i\) 이면 귀납적 가정에 의하여 \(\Gamma \vdash B \implies D_j\) 이고 \(\Gamma \vdash B \implies (D_j \implies D_i)\) 이다. 공리 \((A2)\) 에 의하여 다음은 공리이다.

    \[ \vdash (B \implies (D_j \implies D_i)) \implies ((B \implies D_j) \implies (B \implies D_i)) \]

    MP 를 적용하면 \(\Gamma \vdash B \implies D_i\) 를 얻는다.

  • \(i\) 보다 작은 \(j\) 에 대하여 \(D_i\) 가 \((\forall x_k)D_j\) 이면 귀납적 가정에 의하여 \(\Gamma \vdash B \implies D_j\) 이고, 정리의 가정에 의하여 \(D_j\) 는 \(B\) 에 의존하지 않거나 \(x_k\) 가 \(B\) 의 자유변수가 아니다.

    \(D_j\) 가 \(B\) 에 의존하지 않으면 정리 2.4 에 의하여 \(\Gamma \vdash D_j\) 이고 결국 Gen 에 의하여 \(\Gamma \vdash (\forall x_k)D_j\) 이므로 \(\Gamma \vdash D_i\) 이다. 공리 \((A1)\) 에 의하여 \(\vdash D_i \implies (B \implies D_i)\) 이므로 MP 에 의하여 \(\Gamma \vdash B \implies D_i\) 이다.

    \(x_k\) 가 \(B\) 의 자유변수가 아닌 경우 공리 \((A5)\) 에 의하여 \((\forall x_k) (B \implies D_j) \implies (B \implies (\forall x_k)D_j)\) 이다. 귀납적 가정에 의해 \(\Gamma \vdash B \implies D_j\) 인데 일반화에 의하여 \(\Gamma \vdash (\forall x_k)(B \implies D_j)\) 이고, 그렇다면 MP 에 의하여 \(\Gamma \vdash B \implies (\forall x_k)D_j\) 이다. 즉, \(\Gamma \vdash B \implies D_i\) 을 얻는다.

  위와 같은 귀납법으로 \(i = n\) 인 경우가 증명되었다. ■

• 증명

• 증명

• 증명

  1:

  먼저 다음이 성립한다.

  	연역	근거
  1	\(B\)	Hyp
  2	\((\forall x) B\)	1, Gen

  즉, \(B \vdash (\forall x)B\) 이다. \(x\) 가 \(B\) 에서 자유변수가 아니므로 따름정리 2.6 에 의하여 다음이 성립한다.

  \[ \vdash B \implies (\forall x)B \tag*{■}\]

• 증명

• 증명

• 예시

  1) 의 예시는 다음과 같다.

  \[ \vdash (\forall x)(A _{1}^{1}(x)\iff A _{2}^{1}(x)) \implies [(\exists x)A _{1}^{1}(x) \iff (\exists x)A _{2}^{1}(x)] \]

• 증명

• 가령 \((\exists x)(B(x) \implies C(x)), (\forall x)B(x) \vdash (\exists x)C(x)\) 를 증명할 때 다음과 같은 연역을 사용할 수 있다.

  	연역	근거
  1	\((\exists x)(B(x) \implies C(x))\)	Hyp
  2	\((\forall x)(B(x))\)	Hyp
  3	어떤 \(b\) 에 대하여 \(B(b) \implies C(b)\)	1
  4	\(B(b)\)	2, rule A4
  5	\(C(b)\)	3, 4, MP
  6	\((\exists x)C(x)\)	5, rule E4

  이때 \((\exists x)B(x)\) 라면 어떤 \(b\) 에 대하여 \(B(b)\) 라고 할 수 있다는 것을 보증해주는 규칙이 Rule C 이다. \(C\) 는 선택(choice)의 \(C\) 를 의미한다.

  그런데 일반적으로 이런 증명에서 Rule C 를 사용하지 않고도 똑같은 결과를 얻을 수 있다.

• 조건 3) 은 꼭 필요하다. 왜냐하면 가령 wff \((\exists x)C(x)\) 에서 rule C 로 \(C(d)\) 를 연역했을 때, \(d\) 가 지칭하는 대상이 \((\exists x)C(x)\) 에 존재하는 자유 변수의 값에 의존할 수도 있기 때문이다. 그래서 그 대상이 \((\exists x) C(x)\) 의 모든 자유 변수의 값에 대하여 \(C(x)\) 를 만족하지 않을 수도 있다.

  이런 상황을 보여주는 연역 예시가 다음과 같다.

  	연역	근거
  1	\((\forall x)(\exists y)A _{1}^{2}(x, y)\)	Hyp
  2	\((\exists y)A _{1}^{2}(x, y)\)	1, rule A4
  3	\(A _{1}^{2}(x, d)\)	2, rule C
  4	\((\forall x)A _{1}^{2}(x, d)\)	3, Gen
  5	\((\exists y)(\forall x)A _{1}^{2}(x, y)\)	4, rule E4

  \((\exists y)(\forall x)A _{1}^{2}(x, y)\) 가 연역되었지만 이는 거짓이다. 영역을 \(\Bbb{Z}\) 로 잡고 \(A _{1}^{2}\) 를 \(<\) 로 잡으면 결론은 다음과 같은데, 이는 거짓이다.

  \[ \exists y \in \Bbb{Z} : \forall x \in \Bbb{Z} : x < y \]

• 이 정리는 선택의 규칙 rule C 가 타당하다는 것을 보증해주고, 또한 rule C 를 사용하여 증명된 wff 는 rule C 를 사용하지 않고도 충분히 증명 가능하다는 사실을 말해준다.

• 증명

• 예시

  \(\vdash (\forall x)(B(x) \implies C(x)) \implies ((\exists x)B(x) \implies (\exists x)C(x))\) 를 증명해보자.

  	연역	근거
  1	\((\forall x)(B(x) \implies C(x))\)	Hyp
  2	\((\exists x)B(x)\)	Hyp
  3	\(B(d)\)	2, rule C
  4	\(B(d) \implies C(d)\)	1, rule A4
  5	\(C(d)\)	3, 4, MP
  6	\((\exists x) C(x)\)	5, rule E4
  7	\((\forall x)(B(x) \implies C(x)), (\exists x )B(x) \vdash _C (\exists x)C(x)\)	1-6
  8	\((\forall x)(B(x) \implies C(x)), (\exists x )B(x) \vdash (\exists x)C(x)\)	7, 정리 2.10
  9	\((\forall x)(B(x) \implies C(x)) \vdash (\exists x )B(x) \implies (\exists x)C(x)\)	1-8, 따름정리 2.6
  10	\(\vdash (\forall x)(B(x) \implies C(x)) \implies ((\exists x )B(x) \implies (\exists x)C(x))\)	1-9, 따름정리 2.6

Completeness of first-order predicate calculus✔

Similar✔

• 즉, \(B(x_i)\) 와 \(B(x_j)\) 가 닮았다는 것은 두 wff 가 각 자유변수 \(x_i\) 와 \(x_j\) 에서만 다르다는 것이다.

• 예시

  다음 두 wff 는 서로 닮았다.

  \[ (\forall x_3)\left[ A _{1}^{2}(x_1, x_3) \lor A _{1}^{1}(x_1) \right] \]
  \[ (\forall x_3)\left[ A _{1}^{2}(x_2, x_3) \lor A _{1}^{1}(x_2) \right] \]

• 증명

• 증명

  \(K'\) 이 모순적이면 어떤 wff \(C\) 에 대하여 \(\vdash _{K'}C\) 이고 \(\vdash _{K'}\neg C\) 이다. 정리 2.1 에 의하여 항진식 \(C \implies (\neg C \implies \neg B)\) 는 정리이므로 \(\vdash _{K'} C \implies (\neg C \implies \neg B)\) 이다. 그러면 MP 를 적용하여 다음을 얻는다.

  \[\vdash _{K'}\neg B\]

  \(K'\) 에서 \(B\) 가 공리이므로 이는 \(K\) 에서 \(B\) 가 가정인 것이다. 따라서 \(B \vdash _K \neg B\) 이다. \(B\) 가 닫혀있으므로 따름정리 2.7에 의하여 \(\vdash _K B \implies \neg B\) 이다. \((B \implies \neg B) \implies \neg B\) 은 항진식이므로 정리 2.1 에 의하여 \(\vdash _K(B \implies \neg B) \implies \neg B\) 이다.

  그러므로 MP 를 적용하여 \(\vdash _K \neg B\) 를 얻는다. 그러나 이는 본 정리의 가정에 모순이다. ■

• 증명

  먼저 기호 \(u\) 에 다음과 같은 양의 정수 \(g(u)\) 를 부여하는 함수 \(g\) 를 정의하자.

  \((\)	\()\)	\(,\)	\(\neg\)	\(\implies\)	\(\forall\)
  \(3\)	\(5\)	\(7\)	\(9\)	\(11\)	\(13\)

  \(x_k\)	\(a_k\)	\(f _{k}^{n}\)	\(A _{k}^{n}\)
  \(13 + 8k\)	\(7 + 8k\)	\(1 + 8(2 ^{n}3 ^{k})\)	\(3 + 8 (2 ^{n}3 ^{k})\)

  그리고 식 \(u_0, u_1, \dots, u_r\) 에 \(r\)번째 소수 \(p_r\) 에 대한 정수 \(2 ^{g(u_0)}3 ^{g(u_1)}\dots p_r ^{g(u_r)}\) 을 부여하자. 그러면 가령 \(g(A _{1}^{1}(x_2)) = 2 ^{51}3 ^{3}5 ^{29}7 ^{5}\) 이다. 이때 식에 부여된 수를 기준으로 모든 식을 나열할 수 있다. 그러므로 식 집합은 가산 무한이다. ▲

  임의의 기호가 \(\mathcal{L}\) 의 기호인지 효과적으로 판정할 수 있으면 이 나열은 효과적으로 수행될 수 있고, 임의의 수가 \(\mathcal{L}\) 의 식에 부여된 수인지 효과적으로 검증할 수 있다. 이 사실은 항, wff, 닫힌 wff 들에도 성립한다. ■

• 언어 \(\mathcal{L}\) 의 이론 \(K\) 가 공리적이면, 즉, 주어진 wff 가 \(K\) 의 공리인지 효과적으로 판정할 수 있으면, \(K\) 를 다음과 같은 방식으로 효과적으로 나열할 수 있다.

  먼저 \(K\) 의 공리를 위와 같은 방식으로 나열한다. 그리고 이 공리들에 양화된 변수 \(x_1\) 로 MP 와 Gen 을 한번 적용한 직접적 귀결을 나열한다. 리스트에 두번째 공리를 추가하고 이 리스트의 wff 에 양화된 변수 \(x_1,x_2\) 로 MP 와 Gen 을 적용한 직접적 귀결을 나열한다. 이 방식을 \(k\)번 반복하면 양화된 변수가 \(x_1, x_2, \dots, x_k\) 가 생길 것이다. 이 방식으로 \(K\) 의 모든 정리를 얻을 수 있다.

  그러나 주어진 wff 가 궁극적으로 이 정리 리스트에 나타날지 미리 판정할 수 없는 공리적 이론 \(K\) 도 존재한다.

Completeness✔

• 완전성이란 모든 참인 명제는 증명가능하다는 성질이다. 이 완전성에 대한 정의는 모든 거짓이 명제가 그것의 부정이 증명가능하다는 의미도 포함한다.

Extension✔

Lindenbaum's Lemma✔

• 증명

  보조정리 2.13 에 의하여 \(K\) 의 언어의 모든 닫힌 wff 의 나열을 \(B_1, B_2, \dots\) 이라고 할 수 있다.

  다음과 같이 이론의 열 \(J_1, J_2, \dots\) 를 귀납적으로 정의하자. \(J_0\) 은 \(K\) 이다. \(n \geq 0\) 에 대하여 \(J_n\) 이 정의되었다고 하자. \(\vdash _{J_n}\neg B _{n+1}\) 이 아닐 경우 \(J _{n+1}\) 을 \(J_n\) 에 \(B _{n+1}\) 을 공리로 추가하여 얻은 이론이라고 하자. \(\vdash _{J_n}\neg B _{n+1}\) 이면 \(J _{n+1} = J_n\) 이라고 하자.

  이론 \(J\) 를 \(J_i\) 들의 모든 공리를 공리로 채택하여 얻은 이론이라고 하자. 명백히 \(J _{i+1}\) 은 \(J_i\) 의 확장이고, \(J\) 는 모든 \(J_i\) 들의 확장이다. ▲

  \(J\) 가 무모순임을 보이려면 모든 \(J_i\) 들이 무모순임을 보이기만 해도 충분하다. 왜냐하면 \(J\) 의 모순의 증명은 반드시 어떤 \(J_i\) 의 모순에 대한 증명이기도 하기 때문이다.

  가정에 의하여 \(J_0 = K\) 는 무모순이다. \(J_i\) 가 무모순이라고 하자. \(J _{i+1} = J_i\) 인 경우 \(J _{i+1}\) 는 무모순이다. \(J_i \neq J _{i+1}\) 인 경우 정의에 의하여 \(\neg B _{i+1}\) 이 \(J_i\) 에서 증명 불가능하다. 그러면 보조정리 2.12 에 의하여 \(J _{i+1}\) 는 무모순이다. 그러므로 모든 이론 \(J_i\) 들은 무모순이고 \(J\) 도 무모순이다. ▲

  \(J\) 의 완전성을 모이기 위하여 \(K\) 의 임의의 닫힌 wff \(C\) 를 잡자. 그러면 어떤 \(j \geq 0\) 에 대하여 \(C = B _{j+1}\) 이다. 그렇다면 \(\vdash _{J_j} \neg B _{j+1}\) 이거나 \(\vdash _{J _{j+1}}B _{j+1}\) 이다. 왜냐하면 \(\vdash _{J_j}\neg B _{j+1}\) 가 아닐 경우 \(B _{j+1}\) 이 \(J _{j+1}\) 의 공리로 추가되기 때문이다. 그러므로 \(\vdash _J \neg B _{j+1}\) 이거나 \(\vdash _J B _{j+1}\) 이다. 즉, 임의의 닫힌 wff 가 \(J\) 에서 증명되거나 반증된다. 그러므로 \(J\) 는 완전하다. ■

• 위 증명에서의 \(J\) 는 공리적이지 않을 수 있다. 즉, 주어진 wff 가 \(J\) 의 공리인지 효과적으로 판정할 수 없을 수도 있다. 설령 \(K\) 가 공리적이라고 해도 말이다.

Scapegoat Theory✔

• 증명

  \(K\) 에 새로운 개별 상수의 가산 무한 집합 \(\{b_1,b_2,\dots \}\) 을 추가하여 새로운 이론 \(K_0\) 를 정의하자. \(K_0\) 의 공리는 \(K\) 의 공리, 그리고 \(K\) 의 기호와 새로운 상수를 포함하는 논리적 공리이다.

  \(K_0\) 는 무모순이다. 그렇지 않다면 \(K_0\) 에 wff \(B \land \neg B\) 의 증명이 존재할 것이다. 이 증명에서 나타나는 각 \(b_i\) 를 증명에 나타나지 않는 변수로 교체하자. 이는 공리를 변환시키고, 추론 규칙의 적용의 타당성을 보존한다. 그러면 이 증명의 결론은 모순이지만, 어떠한 \(b_i\) 도 포함하지 않으므로 이 증명은 \(K\) 안에 속한다. 이는 \(K\) 의 무모순성에 위배된다. ▲

  보조정리 2.13 에 의하여 하나의 자유변수를 갖는 \(K_0\) 의 모든 wff 를 다음과 같이 나열할 수 있다.

  \[F_1(x _{i_1}), F_2(x _{i_2}), \dots, F_k(x _{i_k}), \dots\]

  각 \(b _{j_k}\) 가 어떠한 wff 들 \(F_1(x _{i_1}), \dots ,F_k(x _{i_k})\) 에도 속하지 않고, \(b _{j_k}\) 가 \(b _{j_1},\dots ,b _{j_{k-1}}\) 들과는 다르도록 어떤 열 \(b _{j_1}, b _{j_2}, \dots\) 을 잡자.

  다음과 같은 wff 를 생각하자.

  \[ (S_k)\quad (\exists x _{i_k})\neg F_k(x _{i_k}) \implies \neg F_k(b _{j_k}) \]

  \(K_0\) 의 공리에 \((S_1), \dots ,(S_n)\) 을 추가하여 얻은 이론을 \(K_n\) 라고 하고, \(K_0\) 의 공리에 모든 \((S_i)\) 들을 추가하여 얻은 이론을 \(K _{\infty}\) 라고 하자.

  \(K _{\infty}\) 의 임의의 증명은 오직 유한한 \((S_i)\) 들을 포함하므로 이는 반드시 어떤 \(K_n\) 의 증명이다. 그러므로 만약 모든 \(K_n\) 들이 무모순이면 \(K _{\infty}\) 도 무모순이다. 모든 \(K_n\) 의 무모순성을 귀납적으로 증명하자. ▲

  \(K_0\) 는 무모순이다.

  \(n \geq 1\) 에 대하여 \(K _{n-1}\) 이 무모순인데 \(K_n\) 이 모순적이라고 하자. 그러면 항진식 \(\neg A \implies (A \implies B)\) 와 정리 2.1 과 MP 에 의하여 \(K_n\) 에서 어떠한 wff 도 증명가능하다. 따라서 \(\vdash _{K_n} \neg (S_n)\) 이다. 공리 \((S_n)\) 이 이론 \(K _{n-1}\) 에서는 가정이므로 \((S_n) \vdash _{K _{n-1}} \neg (S_n)\) 이다. \((S_n)\) 은 닫혀있으므로 따름정리 2.7 에 의하여 \(\vdash _{K _{n-1}}(S_n) \implies \neg (S_n)\) 이다. 그러나 항진식 \((A \implies \neg A) \implies \neg A\) 와 정리 2.1 과 MP 에 의하여 \(\vdash _{K _{n-1}}\neg (S_n)\) 이다. 즉, \(\vdash _{K _{n-1}}\neg [(\exists x _{i_k})\neg F_n(x _{i_n}) \implies \neg F_n(b _{j_n})]\) 이다. conditional elimination 에 의하여 \(\vdash _{K _{n-1}} (\exists x _{i_n})\neg F_n(x _{i_n})\) 과 \(\vdash _{K _{n-1}}\neg \neg F_n(b _{j_n})\), 즉, \(\vdash _{K _{n-1}}F_n(b _{j_n})\) 을 얻는다.

  그러면 \(b _{j_n}\) 가 \((S_0), \dots ,(S _{n-1})\) 에 나타나지 않으므로 \(F_n(b _{j_n})\) 의 증명에 나타나지 않는 변수 \(x_r\) 에 대하여 \(\vdash _{K _{n-1}}F_n(x_r)\) 이다. 이는 단지 모든 \(b _{j_n}\) 을 \(x_r\) 로 교체한 것이다. Gen 에 의하여 \(\vdash _{K _{n-1}}(\forall x_r)F_n(x_r)\) 이고, 보조정리 2.11 과 biconditional elimination 에 의하여 \(\vdash _{K _{n-1}}(\forall x _{i_n})F_n(x _{i_n})\) 이다. \(F_n(x_r)\) 과 \(F_n(x _{i_n})\) 이 닮음이기 때문이다.

  그런데 이미 \(\vdash _{K _{n-1}} (\exists x _{i_n})\neg F_n(x _{i_n})\) 라는 결론을 얻었었는데, 이는 \(\vdash _{K _{n-1}} \neg (\forall x _{i_n})\neg \neg F_n(x _{i_n})\), 즉, \(\vdash _{K _{n-1}} \neg (\forall x _{i_n})F_n(x _{i_n})\) 와 같다. 이 결과는 모순인데, 이 모순은 \(K _{n-1}\) 의 무모순성에 위배된다. 그러므로 \(K_n\) 은 반드시 무모순이다. 그러므로 \(K _{\infty}\) 도 무모순이다. ▲

  \(K _{\infty}\) 는 \(K\) 의 확장이며, 공리 \((S_k)\) 들에 의하여 자명하게 희생양 이론이다. ■

• 증명

  \(J\) 의 임의의 개별 상수 \(a_i\) 에 대하여 \((a_i) ^{\mathrm{M}_{}} = a_i\) 라고 하자. \(J\) 의 임의의 함수 기호 \(f _{k}^{n}\) 와 임의의 닫힌 항 \(t_1, t_2, \dots, t_n\) 에 대하여 \((f _{k}^{n})^{\mathrm{M}_{}}(t_1, t_2, \dots, t_n) = f _{k}^{n}(t_1, t_2, \dots, t_n)\) 라고 하자. \(J\) 의 임의의 술어 기호 \(A _{k}^{n}\) 에 대해서는, \(D ^{n}\) 의 부분집합 \((A _{k}^{n})^{\mathrm{M}_{}}\) 가 닫힌 항 \(t_1, t_2, \dots, t_n\) 에 대하여 다음을 만족하는 모든 n-튜플 \(\left< t_1, t_2, \dots, t_n \right>\) 로 구성되어 있다고 하자.

  \[\vdash _J A _{k}^{n}(t_1, t_2, \dots, t_n)\]

  이제 \(J\) 의 임의의 닫힌 wff \(C\) 에 대하여 다음을 보이면 충분하다.

  \[ \mathrm{M}\vDash C \quad\text{iff}\quad \vdash _J C \tag{1} \]

  \((1)\) 이 증명될 경우 \(J\) 의 임의의 공리 \(B\) 에 대하여 \(B\) 의 폐포를 \(C\) 라고 하자. 그러면 공리 \(B\) 에 Gen 을 적용하여 \(\vdash _JC\) 이고, \((1)\) 에 의하여 \(\mathrm{M}\vDash C\) 이다. 그러면 진리의 성질 6)에 의하여 \(\mathrm{M}\vDash B\) 이다. 공리가 \(\mathrm{M}\) 에서 참이므로 해석 \(\mathrm{M}\) 은 1차 이론 \(J\) 의 모델이다.

  \((1)\) 의 증명은 \(C\) 의 연결사와 양화사의 수 \(r\) 에 대한 귀납으로 이루어진다. \((1)\) 이 연결사와 양화사가 \(r\) 보다 적은 모든 닫힌 wff 에 대하여 성립한다고 하자.

  1. \(C\) 가 닫힌 원자 wff \(A _{k}^{n}(t_1, t_2, \dots, t_n)\) 인 경우. \((1)\) 은 \((A _{k}^{n})^{\mathrm{M}}\) 의 정의의 직접적 귀결이다.

  2. \(C\) 가 \(\neg D\) 인 경우. \(C\) 가 \(\mathrm{M}\) 에서 참이면 \(D\) 는 \(\mathrm{M}\) 에서 거짓이고, 귀납적 가정에 의하여 \(\vdash _JD\) 가 아니다. \(J\) 가 완전하고 \(D\) 가 닫혀있으므로 \(\vdash _J \neg D\) 이고, 결국 \(\vdash _JC\) 이다. 그 역도 쉽게 보일 수 있다.

     \(C\) 가 \(\mathrm{M}\) 에서 거짓이면 \(D\) 가 \(\mathrm{M}\) 에서 참이고, 그러므로 \(\vdash _JD\) 이다. \(J\) 가 무모순이므로 \(\vdash _J \neg D\) 가 아니다. 즉, \(\vdash _JC\) 일 수 없다. 그 역도 쉽게 보일 수 있다.

  3. \(C\) 가 \(D \implies E\) 인 경우. \(C\) 가 닫혀있으므로 \(D\) 와 \(E\) 도 닫혀있다. \(C\) 가 \(\mathrm{M}\) 에서 거짓이면 \(D\) 가 참이고 \(E\) 가 거짓이다. 그러면 귀납적 가정에 의하여 \(\vdash _JD\) 가 성립하고 \(\vdash _JE\) 는 성립하지 않는다. \(J\) 가 완전하므로 \(\vdash _J \neg E\) 이다. 그러면 항진식 \(D \implies (\neg E \implies \neg (D \implies E))\) 에 MP 를 적용하여 \(\vdash _J \neg (D \implies E)\) 를 얻는다. 즉, \(\vdash _J \neg C\) 인 것이고, \(J\) 가 무모순이므로 \(\vdash _J C\) 는 성립하지 않는다.

     \(\vdash _J C\) 가 성립하지 않으면 \(J\) 가 완전하므로 \(\vdash _J \neg C\) 이다. 즉, \(\vdash _J \neg (D \implies E)\) 이다. conditional elimination에 의하여 \(\vdash _JD\) 이고 \(\vdash _J \neg E\) 이다. \(D\) 에 대한 \((1)\) 에 의하여 \(D\) 는 \(\mathrm{M}\) 에서 참이다. \(J\) 가 무모순이므로 \(\vdash _J E\) 가 성립하지 않고, 그러므로 \(E\) 에 대한 \((1)\) 에 의하여 \(E\) 가 \(\mathrm{M}\) 에서 거짓이다. 그러므로 \(C\) 는 \(\mathrm{M}\) 에서 거짓이다.

  4. \(C\) 가 \((\forall x_m)D\) 인 경우.

     1. \(D\) 가 닫힌 wff 인 경우. 귀납적 가정에 의하여 \(\mathrm{M}\vDash D\) 와 \(\vdash _J D\) 는 동치이다. 문제 2.32 1)에 의하여 \(\vdash _J D \iff (\forall x_m)D\) 이다. Biconditional elimination 에 의하여 \(\vdash _J D\) 와 \(\vdash _J (\forall x_m)D\) 는 동치이다. 또한, 진리의 성질 6) 에 의하여 \(\mathrm{M}\vDash D\) 는 \(\mathrm{M}\vDash (\forall x_m)D\) 와 동치이다. 그러므로 \(\mathrm{M}\vDash C\) 는 \(\vdash _JC\) 와 동치이다.

     2. \(D\) 가 닫힌 wff 가 아닌 경우. \(C\) 가 닫혀있으므로 \(D\) 는 오직 \(x_m\) 만을 자유변수로 갖는다. \(D\) 를 \(F(x_m)\) 라고 하자. 그러면 \(C\) 는 \((\forall x_m)F(x_m)\) 이다.

        • \(\mathrm{M}\vDash C\) 이고 \(\vdash _JC\) 가 아니라고 가정하자. \(J\) 가 완전하므로 \(\vdash _J \neg C\) 이다. 즉, \(\vdash _J \neg (\forall x_M)F(x_m)\) 이다. 문제 2.33 1) 과 biconditional elimination 에 의하여 \(\vdash _J(\exists x_m)\neg F(x_m)\) 이다. \(J\) 가 희생양 이론이므로 \(J\) 어떤 닫힌 항 \(t\) 에 대하여 \(\vdash _J \neg F(t)\) 이다.

          그러나 \(\mathrm{M}\vDash C\), 즉, \(\mathrm{M}\vDash (\forall x_m)F(x_m)\) 이다. 진리의 성질 10) 에 의하여 \((\forall x_m)F(x_m) \implies F(t)\) 가 참이므로 \(\mathrm{M}\vDash F(t)\) 이다. 그러면 1) 에 의하여 \(\vdash _JF(t)\) 이다. 이 모순은 \(J\) 의 무모순성에 위배된다. 따라서 \(\mathrm{M}\vDash C\) 이면 반드시 \(\vdash _JC\) 이다.

        • \(\vdash _J C\) 이고 \(\mathrm{M}\vDash C\) 가 아니라고 가정하자. 즉, 다음의 \((2)\) 는 성립하고 \((3)\) 은 성립하지 않는다.

          \[ \vdash _J(\forall x_m)F(x_m) \tag{2} \]
          \[ \mathrm{M}\vDash (\forall x_m)F(x_m) \tag{3} \]

          \((3)\) 이 성립하지 않으므로 \(D\) 의 원소의 어떤 열이 \((\forall x_m)F(x_m)\) 을 만족하지 않는다. 즉, 어떤 열 \(s\) 가 \(F(x_m)\) 을 만족하지 않는다. \(s\) 의 \(i\)번째 성분을 \(t\) 라고 하자. 한편, \((a_i)^{\mathrm{M}}\) 과 \((f _{k}^{n})^{\mathrm{M}}\) 의 정의에 의하여 \(J\) 의 모든 항 \(u\) 에 대하여 항상 \(s ^{*}(u) = u\) 이다. 또한, \(F(t)\) 는 \(C\) 보다 적은 연결사와 양화사를 가지므로 귀납적 가정이 적용되어 \((1)\) 이 \(F(t)\) 에 성립한다. 그러면 진리의 성질 11) 의 보조정리 2 의 1) 에 의하여 \(s\) 가 \(F(t)\) 도 만족하지 않는다. 따라서 \(F(t)\) 는 \(\mathrm{M}\) 에서 거짓이다. (\(F(t)\) 에 자유변수가 없으므로 \(F(t)\) 가 참이 아니라면 반드시 거짓이다.)

          그러나 2) 와 Rule A4 에 의하여 \(\vdash _JF(t)\) 이고 이에 대하여 \((1)\) 이 성립하므로 \(\mathrm{M}\vDash F(t)\) 이다. 이는 모순이므로 \(\vdash _JC\) 이면 반드시 \(\mathrm{M}\vDash C\) 이다. ■

Denumerable Model✔

• 증명

  보조정리 2.15 에 의하여 \(K\) 는 희생양 이론이고 가산 무한한 닫힌 항을 갖는 무모순 확장 \(K'\) 를 갖는다. 린덴바움의 보조정리에 의하여 \(K'\) 은 \(K'\) 와 같은 기호를 갖는 무모순인 완전한 확장 \(J\) 를 갖는다.

  따라서 \(J\) 도 희생양 이론이다. 보조정리 2.16 에 의하여 \(J\) 는 \(J\) 의 닫힌 항의 가산 무한 집합이 영역인 모델 \(\mathrm{M}\) 을 갖는다. \(J\) 가 \(K\) 의 확장이므로 \(\mathrm{M}\) 은 \(K\) 의 가산 무한 모델이다. ■

Godel's Completeness Theorem✔

• 이 정리에 의하여 논리적으로 타당한 식에는 반드시 증명(유한한 연역)이 존재한다.

• 이 정리는 1차 술어 계산에서 참인 명제는 반드시 증명 가능하다는 것을 보장해준다. 즉, 건전성 정리의 역이 성립함을 보장한다. 즉, 다음이 성립한다.²

  \[ \vDash B \implies \vdash B \]

• 증명

  wff \(D\) 의 논리적 타당성은 그것의 폐포의 논리적 타당성과 동치이고, \(D\) 가 \(K\) 에서 증명가능한 것은 그것의 폐포가 \(K\) 에서 증명가능한 것과 동치이다. 그러므로 오직 닫힌 wff \(B\) 만 고려해도 된다. ▲

  \(B\) 가 \(K\) 에서 논리적으로 타당한 닫힌 wff 라고 하자. \(\vdash _KB\) 가 아니라고 해보자. 그러면 보조정리 2.12 에 의하여 \(\neg B\) 를 \(K\) 에 공리로 추가하여 얻은 이론 \(K'\) 은 무모순이다. 그러면 정리 2.17 에 의하여 \(K'\) 은 모델 \(\mathrm{M}\) 을 갖는다. \(\neg B\) 가 \(K'\) 의 공리이므로 \(\neg B\) 는 해석 \(\mathrm{M}\) 에서 참이다.

  그러나 \(B\) 가 논리적으로 타당하므로 \(B\) 도 해석 \(\mathrm{M}\) 에서 참이다. 즉, \(B\) 가 \(\mathrm{M}\) 에서 동시에 참이면서 거짓이다. 이는 진리의 성질 2) 에 위배된다. 그러므로 \(B\) 는 반드시 \(K\) 의 정리여야 한다. ■

• 이 정리는 1차 술어 계산에서 참됨과 증명가능성이 동치임을 보장한다. 즉, 다음이 성립한다.

  \[ \vDash B \iff \vdash B \]

  그러나 이미 언급했듯이 이는 메타 정리이므로 체계 내의 기호 \(\iff\) 를 사용하는 것은 부적절하다. 이는 정리는 알아보기 쉬게 하기 위한 비공식적인 표현이다.

• 힐베르트는 모든 수학의 발전상을 조망하고 수학이 몇가지 공리를 기반으로 몇가지 추론규칙을 대입하여 발전해온 것이라는 모델을 제안했다. 정말 그러하다면, 모든 수학의 진리가 자동적으로, 기계적으로 공리를 기반으로 추론규칙을 적용함으로써 밝혀질 수 있을 것이다. 이 성질이 완전성이다. 완전성이 성립하면 모든 참인 사실을 체계 내에서 증명가능하고, 건전성이 성립하므로 체계의 공리와 추론규칙을 안전하게 사용할 수 있다.

  괴델은 1930년에 힐베르트 프로그램이 추구하는 체계가 갖춰야 할 4가지 요건(독립성, 무모순성, 완전성, 결정가능성) 중 1차 술어 계산에서의 완전성을 증명했다. 하지만 1차 논리 자체만으로는 산술을 표현할 수 없었다. 산술을 위해서는 고유 공리를 추가해야만 했는데, 사람들은 고유 공리가 추가되어도 여전히 완전성이 성립할 것이고, 힐베르트 프로그램은 성공할 것이라고 낙관했다.

  그러나 괴델이 1931년에 불완전성 정리를 증명하면서 수학자들의 낙관론을 산산조각내었다. 괴델이 불완전성 정리를 발표하는 자리에서 유일하게 그 자리에서 증명을 이해한 폰 노이만이 같은 힐베르트 학파원들에게 "우린 이제 다 끝났군요" 라고 말했고, 이후 러셀은 수학의 기초를 마련하는 일에 염증을 느껴 관심사를 다른데에 돌렸으며, 폰 노이만은 수리논리학에 매달리고 있는 튜링에게 불완전성 정리 때문에 수리논리학을 너무 열심히 연구하지 마라고 조언했다.

• 증명

  정리 2.2 건전성 정리에 의하여 정리이면 논리적으로 타당한 wff 이고, 따름정리 2.18 에 의하여 논리적으로 타당한 wff 이면 정리이다. ■

• 따름정리 2.18, 2.19, 2.20 는 1차 논리 이론에서 구문론적 접근과 의미론적 접근(해석, 모델, 논리적 타당성 등)이 동치라는 것을 보여준다. 명제 논리에서는 따름정리 1.15 가 의미론적 개념(항진식)과 구문론적 개념(\(L\)의 정리)가 동치임을 보장한다.

  명제논리에서의 완전성을 보장해주는 정리 1.14 는 결정 문제의 해답으로 이어진다. 그러나 1차 논리에서 논리적 타당성이나 1차 술어 계산의 증명가능성에 대한 결정 절차를 얻을 수 없다.

• 증명

Skolem–Lowenheim Theorem✔

• 증명

  \(K\) 가 모델을 가지면 어떠한 wff 도 그 모델에서 참이면서 거짓일 수 없다. 그러면 1차 이론의 완전성에 의하여 \(K\) 는 무모순이다. 그러므로 정리 2.17 에 의하여 \(K\) 는 가산 무한 모델을 갖는다. ■

• 이 정리는 정리 2.17 보다 강력한 정리이다.

• 증명

Compactness✔

• 증명

First-Order Theories with Equality✔

• \(B(x, x)\) 의 모든 \(x\) 를 \(y\) 로 치환하여 \(B(x, y)\) 를 만들지 않아도 된다. 따라서 \(B(x, y)\) 는 자유 변수 \(x\) 를 포함할 수도 있고, 그렇지 않을 수도 있다.

• \((A7)\) 의 예시는 다음과 같다.

  \[ x_1 = x_2 \implies (x_1 \cdot x_3 \implies x_2 = x_3) \]

• 증명

• 이 정리로 \((A7)\) 을 더 단순하게 만들 수 있다.

• 증명

• 증명

• 예시

  기초(elementary)라는 단어가 종종 문헌에서 1차 논리를 라는 의미로 사용된다.

  군의 기초 이론 \(G\) 는 이렇게 정의된다. \(G\) 가 술어 기호 \(=\), 함수 기호 \(f _{1}^{2}\), 개별 상수 \(a_1\) 를 갖는다. \(f _{1}^{2}(t, s)\) 를 \(t+s\) 로 축약하고, \(a_1\) 를 \(0\) 로 축약하자. \(G\) 의 고유공리는 다음과 같다.

  1. \(x_1 + (x_2 + x_3) = (x_1 + x_2) + x_3\)
  2. \(x_1 + 0 = x_1\)
  3. \((\forall x_1)(\exists x_2)x_1 + x_2 = 0\)
  4. \(x_1 = x_1\)
  5. \(x_1 = x_2 \implies x_2 = x_1\)
  6. \(x_1 = x_2 \implies (x_2 = x_3 \implies x_1 = x_3)\)
  7. \(x_1 = x_2 \implies (x_1 + x_3 = x_2 + x_3 \land x_3 + x_1 = x_3 + x_2)\)

  정리 2.25 에 의하여 \(G\) 가 동등성을 지닌 이론이라는 것이 보장된다.

  다음의 wff 를 추가 공리로 갖는 이론을 아벨 군의 기초 이론이라고 한다.

  8. \(x_1 + x_2 = x_2 + x_1\)

  이론 \(F\) 가 \(G\) 의 기호와 고유공리에 추가적으로 \(f _{2}^{2}(t,s)\) 가 \(t \cdot s\) 로 축약되는 함수기호 \(f _{2}^{2}\) 와 \(1\) 로 축약되는 개별 상수 \(a_2\) 를 가진다고 하자. \(F\) 가 다음과 같은 고유공리를 가지면 체의 기초 이론이라고 한다. \(F\) 는 동등성을 가진 이론이다.

  9. \(x_1 = x_2 \implies (x_1 \cdot x_3 = x_2 \cdot x_3 \land x_3 \cdot x_1 = x_3 \cdot x_2)\)
  10. \(x_1 \cdot (x_2 \cdot x_3) = (x_1 \cdot x_2)\cdot x_3\)
  11. \(x_1 \cdot (x_2 + x_3) = (x_1 \cdot x_2)+(x_1 \cdot x_3)\)
  12. \(x_1 \cdot x_2 = x_2 \cdot x_1\)
  13. \(x_1 \cdot 1 = x_1\)
  14. \(x_1 \neq 0 \implies (\exists x_2)x_1 \cdot x_2 = 1\)
  15. \(0 \neq 1\)

  \((a)-(m)\) 의 공리를 갖는 이론을 가환환 이론이라고 한다. \(F\) 에 \(A _{2}^{2}(t,s)\) 가 \(t<s\) 로 축약되는 술어 기호 \(A _{2}^{2}\) 를 추가되고, 다음이 공리로 추가되면 순서체 이론이라고 한다.

  16. \(x_1 < x_2 \land x_2 < x_3 \implies x_1 < x_3\)
  17. \(x_1 = x_2 \implies \neg x_1 < x_2\)
  18. \(x_1 < x_2 \lor x_1 = x_2 \lor x_2 < x_1\)
  19. \(x_1 < x_2 \implies x_1 + x_3 < x_2 + x_3\)
  20. \(x_1 < x_2 \land 0 < x_3 \implies x_1 \cdot x_3 < x_2 \cdot x_3\)

Normal Model✔

• 집합 \(D\) 위의 관계 \(R\) 이 다음을 만족하면 항등관계라고 한다. 즉, 항등관계는 모든 원소가 오직 자기 자신과 관계된다.

  \[ R = \{(a,a) : a \in D\} \]

  즉, 정규 모델은 동등성 \(=\) 이 모델의 영역에서 오직 자기 자신과 관계된다는 것을 보장해준다. 그러므로 동등성을 가진 이론에서는 정규 모델을 사용해야 한다.

• 관계 \(E\) 가 동치관계인 것은 정리 2.23 이 보장한다.

Skolem–Lowenheim Theorem✔

• 증명

• 증명

Prenex Normal Forms✔

• \(n=0\) 인 경우 양화사가 존재하지 않는 프리넥스 표준형을 얻는다.

• 모든 wff 에 대하여 그와 동등한 프리넥스 표준형을 얻을 수 있다.

Isomorphism of Interpretations✔

• \(\operatorname{M}\approx \operatorname{M}^{*}\) 이면 이 둘의 영역의 기수는 반드시 같다.