양상논리적으로 생각해 본 증명가능성

(Provability considered modal-logically)

 

계산가능성과 논리 : George S. Boolos   Richard C. Jeffrey 저, 김영정.최훈.강진호 옮김, 문예출판사 (393-5681), 1996 (원서 : Computability and Logic, 3rd ed, Cambridge Univ. Press, 1989), page 333~353

 

우리는 16 장에서 Q 의 확장 T 에 대한 증명가능성 술어 개념을 정의했다. 또 만약 B(y) 가 T 의 증명가능성 술어라면 T 의 언어의 임의의 문장 A 에 대해서 T B (A)→A 이면 T A 이다라는 내용의 룁의 정리를 증명했다. 이 장에서는 Q 를 확장한 이론들에 대한 증명가능성 술어를 탐구하기 위해 명제 양상논리의 개념들과 기교들을 약간 이용하려고 한다. (양상논리에 대한 지식이 미리 꼭 있을 필요는 없다.) 명확하게 하기 위해 T=Z 이고 B(y)=Prov(y) 라고 가정하겠다 (16장을 보라). 그러나 실제로 우리의 방식은 Q 의 확장인 이론들과 그 이론들의 증명가능성 술어들에 일반적으로 적용된다.

우리는 우선 'G' 라고 하는 명제 양상논리의 체계를 기술하려고 한다. (The Unprovability of Consistency: An Essay in Modal Logic (George Boolos 지음, Cambridge University Press, 1979) 은 G 의 확장된 연구이다. G 는 때때로 'L' 또는 'GL' 이라고 부른다.) G 의 구문론은 상당히 표준적이다. 우리는 열거가능할 만큼 많은 양의 문장문자가 있다고 가정하고 (G의) 문장 을 다음과 같이 귀납적으로 정의한다.

는 언제나 거짓이라는 값을 갖는 0항의 진리함수적 연결사이다. -B 는 B 의 부정이고 (B→) 라고 정의할 수 있다. 다른 연결사들은 - 와 → 로부터 일반적인 방식으로 정의된다고 생각할 것이다. □ 는 양상논리에서 보통 '필연적으로' 의 뜻으로 쓰이는 기호이다. ◇ 는 보통 '가능적으로' 를 뜻하는데 -□- 를 줄인 것이라고 생각할 수 있다.

부분문장 이라는 개념은 일반적인 방식으로 정의된다. 곧 모든 문장은 자신의 부분문장이다. 만약 (B→C) 가 A 의 부분문장이라면 B 와 C 도 A 의 부분문장이다. 만약 □B 가 A 의 부분문장이면 B 도 A 의 부분문장이다.

한 문장이 (G의) 공리 가 될 필요충분조건은 그 문장이 동어반복 (tautology) 이거나 (□ 가 하나 이상 나와도 괜찮다) 아니면 문장 □(B→C)→(□B→□C), 문장 □B→□□B, 문장 □(□B→B)→□B 라는 것이다. (G의) 두가지 규칙 은 전건긍정법 (A 와 A→B 에서 B 를 추론하기) 과 필연화 (necessitation, A 에서 □A 를 추론하기) 이다. 문장이 (G의) 정리 가 되는 조건은 여느 때처럼 그 문장이 문장들의 유한한 일련체 - 그 일련체의 각 문장은 공리이거나 아니면 더 앞에 나온 문장들로부터 한 가지 규칙에 의해 추론가능하거나 해야 한다 - 의 맨 마지막 원소가 되는 경우이다. (□B→□□B 가 다른 공리들과 규칙들로부터 도출될 수 있다는 것은 기술적으로 볼 때 흥미롭다. 문장 B→(□(□B&B)→□(B&B) 는 동어반복 B→(□□B&□B)→□B&B) 에서 도출될 수 있고, 그렇다면 □B→□(□(□B&B)→□B&B) 와 □B→□(□B&B) 가 도출될 수 있고, 그래서 □B→□□B 가 도출된다.)

 G A 는 A 가 G 의 정리임을 뜻한다.

G 의 공리들과 규칙들은 16장에서 언급한 Z 와 Prov(y) 에 대한 사실들과 우연하지 않게 꽤 많이 닮았다. 그리고 다음의 정의들과 정리는 Z 와 G 사이에 중요한 관련이 있음을 보여준다.

우리는 'Ø' 를 문장문자 각각에 Z 의 문장을 부여하는 함수에 대한 변항으로 쓰겠다.

만약 A 가 G 의 문장이라면 AØ 는 다음과 같이 귀납적으로 정의된다.

pØ = Ø (p) (p 는 문장문자).
Ø= 0 = 1.
(B→C)Ø = (BØ→CØ).
(□B)Ø = Prov(BØ).

산수의 건전성 정리

만약  G A 이면 모든 Ø 에 대해서 Z AØ 이다. (이 역은 만약 모든 Ø 에 대해서 Z AØ 이면 G A 라는 내용의 산수의 완전성 정리 인데 Robert Solovay 가 증명했다. 그의 "Provability interpretations of modal logic", Israel Journal of Mathematics 25 (1976), 287-304 나 Boolos, Unprovability of Consistency, 12장을 보라.)

증명. Prov(y) 는 Z 에 대한 증명가능성 술어이다. 그리고 A 가 동어반복 문장이거나 문장 □(B→C)→(□B→□C) 또는 □B→□□B 이면 AØ 가 Z 의 정리라는 사실은 증명가능성 술어와 AØ 의 정의에서 바로 따라나온다. 더구나 만약 AØ 와 (A→B)Ø 가 Z 의 정리이면 BØ 도 Z 의 정리라는 사실과 AØ 가 Z 의 정리이면 (□A)Ø(=Prov(AØ) 도 Z 의 정리라는 사실 또한 바로 따라나온다. 따라서 A 가 공리 □(□B→B)→□B 일 때 Z AØ 라는 것을 보여주는 일이 남아 있다. 룁의 정리에 의해 Z Prov(AØ)→AØ 를 보이면 충분하다. S=BØ 라고 하자. 그러면

이다. 16장의 (ii) 에 의해서

와

는 Z 의 정리들이고, (iii) 에 의해서

도 Z 의 정리이고, 따라서 이 세 문장의 진리함수적 귀결인

곧 Prov(AØ)→AØ 도 역시 Z 의 정리이다.

우리가 증명하려고 하는 G 에 관한 정리들을 진술하기 위해 다음과 같은 정의들을 하겠다.

만약 문장 A 에서 문장문자 p 가 나타날 때 모두가 필연성 기호 □ 의 영역 안에 나타난다면 A 를 p 에서 양상화되어 있다 (modalized in p) 고 할 것이다. 그러므로 -□p, □p, □p→□-p, , , □(□□→) 는 p 에서 양상화되어 있지만 p, □p→p, →p 는 모두 p 에서 양상화되어 있지 않다. 만약 A 가 p 에서 양상화되어 있다면 A 는 p 를 제외한 문장문자와 문장들 □B 의 진리함수적 결합이다. ( 와 는 어떤 종류의 문장들이건 상관없이 그 문장들의 진리함수적 결합이라고 '규약적으로' 간주될 것이다.)

임의의 문장 A 에 대해서 A 는 문장 (□A&A) 라고 정의할 것이다. 이 정의는 □A→A 가 언제나 G 의 정리인 것은 아니므로 의미가 있다.

우리는 G 에 대한 고정점 정리 (fixed point theorem) 를 증명하려고 한다. 만약 H 가 A 에 포함된 문장문자들만 포함하고, H 가 p 를 포함하지 않고, G (p↔A)→(p↔H) 라면 H 는 (문장문자 p 와 관련해서) A 의 고정점 이라고 한다. 딕 드 종 (Dick de Jongh) 과 지오바니 샘빈 (Giovanni Sambin) 이 증명한 고정점 정리는 만약 A 가 p 에서 양상화되어 있다면 A 의 고정점이 있다고 주장한다. 우리가 제시하려는 정리의 증명은 아주 간단하다. 이 정리는 샘빈과 리자 라이다르-올슨 (Lisa Reidhaar-Olson) 이 증명한 것이다.

우리는 만약 A 가 표 27-1 의 윗줄에 있는 문장들 중 하나라면 H 는 아랫줄에서 그것과 상응하는 문장이 될 것이라는 것을 알게 될 것이다.

                 표 27.1

A

□p

-□p

□-p

-□-p

-□□p

□p→□-p

□p→q

-□(q→p)

H

-□

□

-□□

□□→□

□q→q

-□-q

보기를 들어보면 만약  Z S↔Prov(-S) 이면  Z S↔Prov(0=1) 이라는 결론이 따라나온다. 그 까닭은 이렇다.  Z S↔Prov(-S) 라고 가정하자. 그러면  Z Prov((S↔Prov(-S)))&(S↔Prov(-S)) 이다. Φ 는 Φ (p)=S 를 만족하는 것이라고 하자. 그러면 Z ((p↔□-p))Ø 이다. 고정점 정리에 의해서 G (p↔□-p))→(p↔□) 이고, 따라서 산수의 건전성 정리에 의해서  Z ((p↔□-p)→(p↔□))Ø, 곧  Z ((p↔□-p))Ø→(p↔□)Ø 이다. (Z에서) 전건긍정법에 의해서  Z (p↔□)Ø, 곧  Z S↔Prov(0=1) 이다. 양상 체계 G 에 대한 다른 비슷한 정리들도 비슷한 방식으로 Z 에 대한 정리들로 바꿀 수 있다.

우리의 두번째 정리를 위해 정의 두 가지가 더 필요하다. 문자 없는 (letterless) 문장이란 문장문자를 전혀 포함하지 않는 문장을 말한다. 보기를 들어보면 , , -□, -□→-□-□ 가 있다. 문장 없는 문장은 귀납적인 정의를 갖는다. 곧 는 문자가 없다. 만약 A 와 B 가 문자가 없으면 (A→B) 도 그렇다. 만약 A 가 문자가 없으면 □A 도 그렇다.

또 □nA 를 정의하겠다. □0A=A. □n+1A=□□nA

우리가 증명하려고 하는 두 번째 정리는 문자없는 문장에 대한 표준 형식 정리 (normal form theorem) 이다: 만약 A 가 문자가 없다면 문장들 □n 의 어떤 진리함수적 결합 B 에 대해서 G A↔B 이다.

이 두 정리를 합하면 다음과 같은 것을 알게 된다. 만약 A 가 p 에서 양상화되어 있고 p 이외의 문장문자를 전혀 포함하지 않는다면

를 만족하는 문장들 □n 의 진리함수적 결합 H 가 있게 된다.

고정점 정리에서 따라나오는 Z 에 대한 일반적인 정리가 있다. 그 내용은 대충 다음과 같이 말할 수 있따. 만약 P(y) 가 Prov(y) 와 진리함수적 조작 '으로부터 만들어진' Z 의 술어라면, P(y) 의 Z 에서의 임의의 고정점, 곧  Z S↔P(S) 인 임의의 문장 S 는 Z 에서 0=1, Prov(0=1), Prov(Prov(0=1)) 등의 어떤 진리함수적 결합과 동치이다. 이 문장들은 보기만 해도 진리조건을 알 수 있다. 왜냐하면 어떠한 (산수의 언어 L 에 대한 표준적 해석 에서의) 거짓도 Z 에서 증명가능하지 않으므로 그 문장들은 모두 거짓 이기 때문이다. 따라서 진리 함수와 Prov(y) 로부터 만들어진 어떤 술어의 고정점이라고 '자기 지시적으로' 기술된 임의의 문장은 어떤 거짓 문장들의 진리함수적 결합과 동치이다. 그 결합은 술어로부터 계산할 수 있고 앞으로 보겠지만 그 계산은 아주 간단하다.

우리의 세번째 정리는 다음과 같다. p0, ..., pn-1

이다. 우리는 이 정리를 교호 정리 (reciprocation theorem) 라고 부르겠다. 우리는 이 정리의 증명을 먼저 한 다음 그 의미를 논의하겠다.

G 에 대한 기본적인 사실 몇 가지를 말하겠다.

사실 1. G 의 정리들은 진리함수적 귀결 아래에서 닫혀 있다. 그 까닭은 이렇다. G A1, ..., G An 이고 또 B 가 A1, ..., An 의 진리함수적 귀결이라고 가정하자. 그러면 (A1→(A2→...(An→B)...)) 는 동어반복 문장이고 따라서 G 의 정리이다. 전건긍정법을 n 번 적용하면 G B 가 된다.

사실 2. G □A&□B↔□(A&B) 이다. 그 까닭은 이렇다. A→(B→(A&B)) 는 동어반복 문장이고 필연화에 의해서 G □(A→(B→(A&B))) 이다.

와 □(B→(A&B))→(□B→□(A&B)) 는 G 의 공리들이므로 사실 1 때문에  G □A&□B→□(A&B) 가 된다. 그 역을 보자면, (A&B)→A 와 (A&B)→B 는 동어반복 문장이므로  G □(A&B)→□A 와  G □(A&B)→□B 가 되고, 따라서  G □A&□B↔□(A&B) 가 된다.

사실 3. 만약 G A1&...&An→B 이면  G □A1&...&□An→□B 이다. n 에 대한 귀납으로 증명을 하겠다. 만약 n=1 이고  G A1→B 라면 필연화에 의해서  G □(A1→B) 이다. 그리고 G □(A1→B)→(□A1→□B) 이므로  G □A1→□B 이다.  G A1&...&An&An+1→B 라고 가정하자. 그러면  G A1&...&(An&An+1)→B 인데 여기서 귀납 가설에 의해서  G □A1&...&□(An&An+1)→□B 이다. 사실 1과 사실 2 때문에  G □A1&...&□An&□An+1→□B 라는 결론을 얻게 된다.

사실 4. 만약 G □A1&A1&...&□An&An&□B→B 이면

이다. 그 까닭은 이렇다. 만약 가설이 성립한다면

이고 따라서 사실 3에 의해서

이다. G □Ai&□□Ai 이고  G □(□B→B)→□B 이므로 G □A1&...&□An→□B 이다.

이제 (G 에 대한) 모형 개념을 정의하고 그 개념에 대한 적합성 (=건전성과 완전성) 정리를 증명하겠다. (G 에 대한 적합성 정리는 Segerberg 가 처음으로 증명했다. 양상논리체계에 대한 위와 같은 형태의 적합성 정리는 크립크 (S. Kripke) 가 처음으로 증명했다.) 모형이란 비공집합인 유한한 집합 W 와, 그 W 에서의 ('W 에서의' 는 wRx 이면 w, x∈W 임을 뜻한다) 이행적이고 (wRxRy 이면 wRy) 비재귀적인 (xRx 가 아닌) 관계와, W 의 원소와 문장문자로 이루어진 각 순서쌍에 진리값 (1 또는 0) 을 부여하는 함수 P 로 이루어진 삼중체 <W, R, P> 이다.

M〔 = <W, R, P> 〕을 모형이라고 하자. ('<W, R, P>' 는 'M' 이라고 줄여 쓸 것이다.) W 의 각 w 와 문장 A 에 대해서 M, w A ('A 는 M 의  w 에서  참이다' 라고 읽어라) 의 개념을 다음과 같이 정의하겠다.

M, w p 인 꼭 그 경우에 P(w, p)=1 (p 는 문장문자),
M, w ,  
M, w B→C 인 꼭 그 경우에  M, w B  또는  M, w C,
M, w □B 인 꼭 그 경우에 wRx 를 만족하는 모든 x 에 대해 M, w B.

그러므로 M, w (B&C) 일 경우 그리고 오직 그 경우에만 M, w B 와  M, w C 가 동시에 성립하고, 이는 다른 진리함수적 연결사에 대해서도 비슷하다.

만약 W 의 모든 w 에 대해서 M, w A 이면 문장 A 를 M 에서 타당하다 고 하고 만약 A 가 모든 모형에서 타당하다면 A 를 타당하다 고 할 것이다.

그러면 적합성 정리는 A 가 타당하면 (완전성) 그리고 오직 그 경우에만 (건전성) A 는 정리라고 말한다.

등급 (rank) 개념이 중요하다는 것은 다음을 보면 알 수 있다.

만약 R 이 W 에서 이행적이고 비재귀적인 관계이고 wiR...Rw1Rw0 이면, w0, ..., wi 는 모두 서로 다르다. 왜냐하면 i≥j>k≥0 이면 이행성에 의해서 wjRwk 이고 그러면 비재귀성에 의해서 wj≠wk 이기 때문이다. 따라서 W 가 또한 유한하고 (이를테면) m 개의 원소를 포함한다면 i≥m 일 때 wiR...Rw1Rw0 인 경우는 결코 없다. 따라서 M 이 모형이면 W 의 각 w 에 대해서 W 의 어떤 wi, wi-1, ..., w1, w0 에 대해 w=wiRwi-1R...w1Rw0 을 만족하는 가장 큰 자연수 i(<m) 가 있다. 우리는 이 자연수를 M 에서의 w 의 등급 이라고 부를 것이고, 문맥이 M 을 언급하지 않아도 괜찮다면 'rk(w)' 라고 쓰겠다. (만약 어떤 x 에 대해서도 wRx 가 아니라면 rk(w)=0 이다.)

분명히 wRx 이면 rk(w)>rk(x) 이다. 그리고 j<i=rk(w) 이면 wRx 를 만족하는 어떤 x 에 대해서 rk(x)=j 이다. 그 이유는 이렇다. 만약 w=wiR...RwjR...Rw0 이면 분명히 rk(wj)≥j 이지만, rk(wj)>j 이면 rk(w)≥(i-j)+rk(wj)>i=rk(w) 이고 이는 모순이다. 따라서 rk(wj)=j 이고 이행성에 의해서 wRwj 이다.

의미론적 건전성 정리

만약  G A 이면 A 는 타당하다.

증명. 우리는  G A 이면 A 가 임의의 모형 M 에서 타당하다는 걸 보이겠다. M 은 증명 내내 고정되어 있으므로 'M, w ' 대신에 'w ' 라고 종종 쓰겠다.

만약 A 가 동어반복 문장이라면 ' ' 의 정의에서 와 → 에 해당하는 구절로부터 w A 가 따라나온다. 만약 w □(B→C) 이고 w □B 이면 wRx 를 만족하는 모든 x 에 대해서 x B→C 이고 x B 이며, 따라서 wRx 를 만족하는 모든 x 에 대해서 x C, 곧 w □C 이다. 따라서 w □(B→C)→(□B→□C) 이다. 만약 w □B 이면 wRx 를 만족하는 모든 x 에 대해서 x □B 이다. 왜냐하면 xRy 이면 R 의 이행성에 의해서 wRy 이고 그러면 y B 이기 때문이다. 그러므로 만약 w □B 이면 w □□B 이고 따라서 w □B→□□B 이다.

이제  □(□B→B)→□B 의 꼴을 갖는 공리를 생각해 보겠다. w □B 라고 가정해 보자. 그러면 어떤 x 에 대해서 wRx 이고 x B 이다. x 를 wRx 와  x B 를 만족하는 가장 낮은 등급 이라고 해보자. xRy 라고 가정해 보자. 그러면 rk(y)<rk(x) 이다. 이행성에 의해서 wRy 이고, x 의 등급이 가장 낮기 때문에  y B 이다. 따라서  x □B 이고  x □B→B 이고, wRx 이므로  w □(□B→B) 이다. 그러므로  w □(□B→B)→□B 이고 G 의 모든 공리는 M 에서 타당하다.

만약 M, w A 이고  M, w A→B 이면  M, w B 이다. 그리고 만약 A 가 M 에서 타당하면 □A 도 M 에서 타당하다. 왜냐하면 W 의 모든 w 에 대해서, wRx 이면 M, x A 이고, 따라서 M, w □A 이기 때문이다. 그러므로 M 에서 타당한 문장들로부터 전건긍정법과 필연화에 의해 추론가능한 어떠한 문장도 M 에서 역시 타당하다. 따라서 G 의 모든 정리는 M 에서 타당하다.

의미론적 완전성 정리

만약 A 가타당하면  G A 이다.

증명. (여기서의 증명은 Solovay 와 Warren Goldfarb 덕분에 매우 간단해졌다.) A 가 G 의 정리가 아니라고 가정해 보자. 우리는 A 가 타당하지 않게 되는 모형을 만들 것이다. 만약 문장 B 가 A 의 부분문장이거나 A 의 부분문장의 부정이면 그 B 를 식 이라고 부를 것이다. 식들의 집합 X 는 X 의 원소들의 연언의 부정인 -∧X 가 G 의 정리가 아니라면 일관적 이라고 부를 것이다. 만약  G --A 이면  G A 인데 이것은 가정에 모순되므로 {-A} 는 일관적이다. 일관적인 집합 X 는 만약 A 의 모든 부분문장 B 에 대해서 B 가 X 에 있거나 -B 가 X 에 있으면 최대 (maximal) 라고 부르겠다. 모든 일관적인 집합은 어떤 최대집합의 부분집합이다. 그 까닭은 이렇다. ∧X 는 어떤 공집합이 아닌 선언과 동치인데 그 선언의 선언지 각각은 X 의 모든 원소들을 포함하고 A 의 각 부분문장 B 에 대해서 B 와 -B 가운데 정확히 하나만 포함하는 연언이다. X 가 일관적이므로 선언을 이루는 이 연언들 중 적어도 하나의 연언의 연언지들은 일관적인 집합을 이룰 것이고, 실제로 X 의 모든 원소들을 포함하는 최대집합이 될 것이다. 만약 X 가 최대이고, B1, ..., Bn∈X 이고, C 는 A 의 부분문장이고,  G B1&...&Bn→C 이면 C∈X 이다. 왜냐하면 그렇지 않으면 -C∈X 이고 그래서  G -∧X 이며 이것은 X 의 일관성에 모순되기 때문이다.

W 를 최대집합들의 집합이라고 하자. {-A} 는 일관적이고 따라서 어떤 최대집합의 부분집합이므로 W 는 공집합이 아니다. W 는 유한하다. 왜냐하면 사실 A 의 부분문장들이 k 개 있다면 최대집합이 많아야 2k 개 있기 때문이다. w, x∈W 이고, 동시에 □C 가 w 에서 A 의 부분문장일 때마다 □C 와 C 가 x 에 있으면 그리고 오직 그 경우에만 wQx 라고 하자. Q 는 분명히 이행적이다. 왜냐하면 wQxQy 이고 □C 가 w 에서 A 의 부분문장이라면 □C 는 x 에 있고, 따라서 □C 와 C 가 y 에 있기 때문이다. wQx 이고 동시에 xQx 가 아닌 경우 그리고 오직 그 경우에만 wRx 라고 하자. R 은 분명히 비재귀적이다. 그리고 R 은 이행적이다. 왜냐하면 만약 wRxRy 이면 wQx, xQy 이고 yQy 는 아니며, Q 의 이행성에 의해서 wQy 이므로 wRy 가 되기 때문이다. W 의 모든 w 와 모든 문장문자 p 에 대해서 p∈w 일 경우 그리고 오직 그 경우에만 P(w, p)=1 이고 그 외의 경우에는 P(w, p)=0 이라 하자. M=<W, R, P> 라고 하자. 우리는 이제 A 의 모든 부분문장들 B 와 W 의 모든 w 에 대해서 B∈w 일 경우 그리고 오직 그 경우에만 M, w B 라는 걸 복합도 (complexity) 에 대한 귀납으로 증명하겠다. ('M' 은 종종 생략하겠다.)

만약 B 가 문장문자 p 라면 p∈w 인 꼭 그 경우 P(w, p)=1 이고 꼭 그 경우 w p 이다. 만약 B= 이면 w 이고 이것은 일관적이다. 그러나 또한 w 이다. 만약 B=(C→D) 이면 C 와 D 는 A 의 부분문장이고  G -B↔(C&-D) 이다. 따라서 Bw 인 꼭 그 경우 (최대성에 의해서) -B∈w 이고, 꼭 그 경우 C∈w 와 -D∈w 이고, 꼭 그 경우 C∈w 와 Dw 이고, 꼭 그 경우 (귀납 가설에 의해서) w C 와 w D 이고, 꼭 그 경우 w (C→D) 이고, 꼭 그 경우 w B 이다. 그러므로 B∈w 일 경우 그리고 오직 그 경우에만 w B 이다.

이제 B=□C 라고 가정하자. □C∈w 라고 가정하자. 만약 wRx 이면 wQx 와 C∈x 이고 거기서 귀납 가설에 의해서 x C 이다. 따라서 wRx 를 만족하는 모든 x 에 대해 x C 이고, 그래서 w □C 이다. 그 역을 위해서 w □C 라고 가정하자. □D1, ..., □Dn 은 모두 w 에 있는 문장 □D 라고 하자. X={□D1, D1, ..., □Dn, Dn □C, -C} 라고 하자. X 는 일관적인가? 일관적이라면 어떤 최대집합 x 에 대해 X⊆x 이다. 그러나 □D1, D1, ..., □Dn, Dn 은 모두 x 에 있으므로 wQx 이고, □C 와 -C 가 x 에 있으므로 xQx 는 아니다. 따라서 wRx 이고 x  C 이며 귀납 가설에 의해서 C∈x 이다. 그러나 -C∈X⊆x 이다. 따라서 X 는 일관적이지 않고, 그러므로  G □D1&D1&...&□Dn&□Dn&□C→C 이다. 사실 4에 의해서  G □D1&...&□Dn→□C 이다. □D1, ..., □Dn∈w 이고 □C 는 A 의 부분문장이므로 □C∈w 이다.

우리는 만약 B 가 A 의 임의의 부분문장이고 w∈W 이라면, B∈w 일 경우 그리고 오직 그 경우에만 M, w B 라고 결론짓겠다. {-A} 가 일관적이므로 W 의 어떤 w 에 대해서 -A∈w 이고 Aw 이다. 그러므로 M, w A 이고, A 는 모형 M 에서 타당하지 않다.

이제 G 에 대한 고정점 정리로 돌아가겠다.

사실 5.  G A→□A 이다. 그 까닭은 이렇다. 만약  G □A→□□A 이므로,  G □A→□□A&□A 이고, 그러므로  G □A→□(□A&A), 곧  G □A→□A 이며, 따라서  G A→□A 이다.

사실 6. 만약  G A→B 이면  G A→B 이다. 그 까닭은 이렇다. 만약  G A→B 이면  G □A→□B 이고 그러면 사실 5에 의해서  G A→□B 이다. 따라서  G A→□B&B, 곧  G A→B 이다.

A 는 문장, p 는 문장문자, F 는 문장이라고 하자. p 대신에 A 를 대입한 결과인 Fp(A), 줄여서 F(A) 는 다음과 같은 기계적인 귀납적인 정의를 갖는다.

사실 7 (대입). A, B 는 문장, p 는 문장문자, F 는 문장이라고 하자. 그러면  G (A↔B)→(F(A)↔F(B)) 이고, 따라서 사실 6에 의해서  G (A↔B)→(F(A)↔F(B)) 이다. (A↔B)→(F(A)↔F(B)) 가 타당하고 따라서 완전성에 의해 G 의 정리라는 것을 F 의 복합도에 따른 귀납에 의해 보여주겠다. M, 곧 <W, R, P> 는 모형이고 w∈W 라고 가정하자. 'M' 은 생략하자. F=□G 인 경우만 생각할 필요가 있다. w (A↔B) 라고 가정하자. 사실 5 (와 건전성) 에 의해서  w □(A↔B) 이다. 따라서 wRx 를 만족하는 모든 x 에 대해서 x (A↔B) 이다. 따라서 만약 w F(A) 이면 wRx 를 만족하는 모든 x 에 대해서 x G(A) 이고, 그러면 귀납 가설에 의해서 wRx 를 만족하는 모든 x 에 대해서 x G(B) 이고 따라서 w F(B) 이다. 그러므로 w F(A)→F(B) 이고 마찬가지로 w F(B)→F(A) 이다. 그러므로 (A↔B)→(F(A)↔F(B)) 는 타당하고 완전성에 의해서 G 의 정리이다.

사실 8. 만약 G A 이면 G □A 이고 G □A&A, 곧 G A 이다.

고정점 정리의 증명. 만약 서로 다른 문장문자의 어떤 (비어있을 수도 있는) 일련체 q1, ..., qn 과, p 는 포함하지 않지만 q1, ..., qn 은 포함하는 어떤 문장 B(q1, ..., qn) 과, 각각이 실제로 p 를 포함하고 있는 서로 다른 문장들의 어떤 일련체 C1(p), ..., Cn(p) 에 대해서 A=B(□C1(p), ..., □Cn(p)) 이면, 그 문장 A 를 등급 n 이라고 하자. 만약 A 가 p 에서 양상화되어 있으면, 어떤 n≥0 에 대해서 A 는 등급 n 이다.

만약 A 가 등급 0 이라면 A 는 p 를 포함하지 않으며 A 는 자신의 고정점이다. 정리를 증명하기 위해서는 p 에서 양상화된 등급 n 의 모든 문장이 고정점을 가진다는 가정에서부터 p 에서 양상화된 등급 n+1 의 모든 문장이 고정점을 가진다는 것을 보여주면 충분하다. 따라서 A 를 p 에서 양상화된 등급 n+1 의 문장이라고 하자. 그러면 어떤 적절한 B 와 q1, ..., qn+1 과 C1(p), ..., Cn+1(p) 에 대해서, A=B(□C1(p), ..., □Cn+1(p)) 이다. 1≤i≤n+1 인 각 i 에 대해서 Ai 는 문장

이다. 각 Ai 는 p 에서 양상화된 등급 n 의 문장이고, 따라서 귀납 가설에 의해서 고정점 Hi 를 가진다. H 는 문장

이라고 하자.

우리는 H 가 A 의 고정점이라는 것을 보여주겠다. 고정점의 이런 특징은 샘빈이 보여준 것이다. 우리는 이것을 보기 두 가지를 들어 설명하겠다.

(1) A=□-p 라고 하자. 그러면 B(q1)=q1 이고 C1(p)=-p 일 때 A=B(□C1(p)) 이다. A1= 인데 이것은 등급이 0 이고, 그러므로 자신의 고정점이다. 따라서 우리는 B(□C1())=□- 를 H 라고 할 수 있다.

(2) A=□(p→q)→□-p 라고 하자. 그러면 B(q1, q2)=(q1→q2) 이고 C1(p)=(p→q) 이고 C2(p)=-p 일 때 A=B(□C1(p), □C2(p)) 이다. A1=(→□-p) 인데 이것은 □-p 와 동치이고, A2=□(p→q)→ 인데 이것은 와 동치이다. (1) 에 의해서 □- 는 A1 의 고정점이고 는 A2 의 고정점이다. 따라서 우리는 B(□C1(□-), □C2())=(□(□-→q)→□-) 를 H 라고 할 수 있다.

샘빈의 구성이 올바르다는 것에 대한 다음의 증명은 라이다르-올슨이 발견했다.

M, 곧 <W, R, P> 는 임의의 모형이라고 하자. 'M' 은 생략하자. w E 일 경우 그리고 오직 그 경우에만 wRx 또는 w=x 를 만족하는 그러한 모든 x 에 대해서 x E 라는 사실을 주목하라.

보조정리 27.1

y 는 W 에 있고 1≤i≤n+1 이라고 하자. y (p↔A) 이고 y □Ci(p) 라고 가정하자. 그러면 y Ci(p)↔Ci(Hi) 이고 y □Ci(p)↔□Ci(Hi) 이다.

증명. y □Ci(p) 이므로 R 의 이행성에 의해서 yRz 를 만족하는 모든 z 에 대해서 z □Ci(p) 이다. 그러면 y □Ci(p)↔ 이고 yRz 를 만족하는 모든 z 에 대해서 z □Ci(p)↔ 이다. 따라서 y (□Ci(p)↔) 이다. 대입에 의해서 y (A↔Ai) 이고, 거기서 y (p↔A) 이므로 y (p↔Ai) 이다. 그러나 Hi 는 Ai 의 고정점이다. 따라서 사실 6에 의해서 y (p↔Ai)→(p↔Hi) 이다. 그러므로 y (p↔Hi) 이다. 사실 7에서 F=Ci 라고 놓으면 y Ci(p)↔Ci(Hi) 가 된다. F=□Ci 라고 놓으면 마찬가지로 y □Ci(p)↔□Ci(Hi) 가 된다.

보조정리 27.2

w 는 W 에 있고 1≤i≤n+1 이라고 하자. 그러면 w (p↔A)→(□Ci(p)→□Ci(Hi)) 이다.

증명. w (p↔A) 이고, wRy 또는 w=y 이고, y □Ci(p) 라고 하자. 그러면 y (p↔A) 이고 보조정리 27.1 에 의해서 y □Ci(Hi) 이다.

보조정리 27.3

w 는 W 에 있고 1≤i≤n+1 이라고 하자. 그러면 w (p↔A)→(□Ci(Hi)→□Ci(p)) 이다.

증명. w (p↔A) 이고, wRx 또는 w=x 이고, x -□Ci(p) 라고 하자. 그러면 가장 작은 M 등급의 어떤 y 에 대해서 xRy 이고 y -Ci(p) 이다. 가장 작기 때문에 y □Ci(p) 이다. w (p↔A) 이고 wRy (이행성) 이므로 y (p↔A) 이다. 보조정리 27.1 에 의해서 y Ci(p)↔Ci(Hi) 이다. 그러므로 y -Ci(Hi) 이고 따라서 x -□Ci(Hi) 이다.

보조정리 27.4

w 는 W 에 있고 1≤i≤n+1 이라고 하자. 그러면 w (p↔A)→(□Ci(p)↔□Ci(Hi)) 이다.

증명. 보조정리 27.2 와  27.3 에 의해서 성립한다.

이제 고정점 정리는 바로 따라나온다. 보조정리 27.4 와 대입을 n+1 번 사용하면 W 의 모든 w 에 대해서

곧 w  (p↔A)→(A↔H) 이고 여기서  w  (p↔A)→(p↔H) 이다. 따라서 (p↔A)→(p↔H) 는 타당하고 완전성 정리에 의해서 G 의 정리이다.

고정점 정리의 역은 어떤가? 만약 A 가 p 에서 양상화되어 있고 H 가 A 의 고정점이라면 (p↔H)→(p↔A) 는 타당한가? 골드파브 (Goldfarb) 가 한 논증의 도움을 받아 그렇다는 것을 보여주겠다.

그 까닭은 이렇다. M, 곧 <W, R, P> 는  (p↔H)→(p↔A) 가 타당하지 않게 되는 모형이라고 가정하자. w 는 M, w  (p↔H) 이지만 M, w (p↔A) 인 M 의 가장 작은 등급의 세계라고 하자. 만약 wRx 이면 M, x (p↔H) 이고 따라서 w 의 등급이 가장 작으므로 M, x (p↔A) 이다. 그러므로 M, w □(p↔A) 이다. P′ 는 P′(w, p) = 1-P(w, p) 라는 점만 제외하고는 P 와 똑같다고 하고, M′=<W, R, P′> 라고 하자. 식의 복합도에 따른 기계적인 귀납은 임의의 식 D 와 wRx 를 만족하는 임의의 x 에 대해서 M, x  D 일 경우 그리고 오직 그 경우에만 M′, x  D 라는 것을 보여준다. 그러므로 임의의 식 □D 에 대해서 M, w  □D 인 꼭 그 경우 wRx 를 만족하는 모든 x 에 대해서 M, x  D 이고 꼭 그 경우 wRx 를 만족하는 모든 x 에 대해서 M′, x  D 이고 꼭 그 경우 M′, w  □D 이다. 특히 M′, w  □(p↔A) 이다. 더구나 만약 q 가 p 이외의 임의의 문장문자라면 M, w  q 일 경우 그리고 오직 그 경우에만 M′, w  q 이다. A 와 H 는 p 이외의 문장문자와 문장 □D 의 진리함수적 결합이다. 거기서 M, w  A 인 꼭 그 경우에 M′, w  A 라는 것과 M, w  H 인 꼭 그 경우에 M′, w  H 라는 것이 따라나온다. M, w  (p↔H) 이고, M, w  (p↔A) 이므로 M′, w  (p↔H) 이고 M′, w  (p↔A) 이다. 따라서 M′, w  (p↔A) 이다. 그러나 고정점 정리에 의해서 M′, w  (p↔H) 이고 이것은 모순이다.

그러므로 만약 A 가 p 에서 양상화되어 있고 H 가 A 의 고정점이라면 (p↔H)→(p↔A) 는 타당하고 완전성에 의해서 정리이다. 이제 G 의 정리들은 대입 아래에서 닫혀 있다. 곧 G 의 임의의 공리에서 p 대신에 문장을 대입한 결과는 바로 G 의 공리이다. 그리고 만약 F=(G→H) 이면 F(A)=(G(A)→H(A)) 이고 또 만약 F=□G 이면 F(A)=□G(A) 이므로 G 의 임의의 정리에 대해서도 같은 게 성립한다. 따라서 (H↔H)→(H↔A(H)) 는 G 의 정리이다. 그러나 G H↔H 이다. 사실 8에 의해서 G (H↔H) 이고 따라서  G H↔A(H) 이다.

따라서 고정점은 p 에서 양상화된 어떤 A 에 대해서도 존재하고, A 의 임의의 고정점 H 에 대해서 G (p↔A)↔(p↔H) 이고  G H↔A(H) 이다. 만약 A 에 있는 유일한 문장문자가 p 라면 H 는 문자 없는 문장이고, 다음 정리가 보여주듯이 문자 없는 어떤 문장도 특별히 명확한 방식으로 쓸 수 있다.

문자 없는 문장에 대한 표준형식 정리

문자 없는 각 문장 A 에 대해 자연수들의 집합 A 를 다음과 같이 관련시킬 수 있다.

보조정리 27.5

A 가 문자 없는 문장이라고 가정하자. M=<W, R, P>, w∈W 라고 하자. 그러면 w A 일 경우 그리고 오직 그 경우에만 rk(w)∈A 이다.

증명. 만약 A= 이면 wA 이고 rk(w)ø=A 이다. 만약 A=(B→C) 이면 wA 인 꼭 그 경우 wB 또는 wC 이고 꼭 그 경우 (귀납가설) rk(w)B 또는 rk(w)∈C 이고 꼭 그 경우 rk(w)(N-B)∪C=(B→C)=A 이다.

A=□B 라고 가정하자. wA 라고 하자. 그러면 wRx 를 만족하는 모든 x 에 대해 xB 이고,다. 따라서 만약 i<rk(w) 이면 어떤 x 에 대해서 rk(x)=i 이고 wRx 이며, 따라서 xB 이고, 그러면 귀납 가설에 의해서 i∈B 이다. 그러므로 rk(w)∈□B=A 이다. 역으로 rk(w)∈A=□B 라고 가정하자. 그러면 모든 i<rk(w) 에 대해서 i∈B 이다. 따라서 만약 wRx 이면 rk(x)<rk(w) 이고 따라서 rk(x)∈B 이고 그러면 귀납 가설에 의해서 xB 이다. 그러므로 w□B, 곧 wA 이다.

보조정리 27.6

□n={m: m<n}.

증명. n 에 대한 귀납으로 증명을 하겠다. □0==ø={m: m<n} 이다. 만약 □n={m: m<n} 이면 □n+1=□□n={m: 모든 i<m 에 대해서 i∈□n}={m: 모든 i<m 에 대해서 i<n}={m: m≤n}={m: m<n+1} 이다.

이제 문자 없는 각 문장 A 에 대해 문장들 □n 의 진리함수적 결합 A# 를 관련시킨다.

A# 가 언제나 문장 □n 의 진리함수적 결합이라는 것은 분명하다.

이제 문자 없는 문장들에 대한 표준형식 정리를 증명하겠다.

정리

만약 A 가 문자가 없으면 G A↔A# 이다.

증명. A=□B 인 경우만 생각할 필요가 있다는 사실은 A# 의 정의에서 볼 때 분명하다.

경우 1. B = N. 그러면 A#= 이고 이것은 타당하다. 보조정리 27.5 에 의해서 M, w  A 일 경우 그리고 오직 그 경우에만 rk(w)∈A=□B={m: 모든 i<m 에 대해서 i∈B}=N 이다. 따라서 임의의 w 에 대해서 M, w  A 이다. 그러므로 A 도 또한 타당하고 따라서 A↔A# 이다.

경우 2. 어떤 n 에 대해서 nB 이다. n 은 B 에 있지 않은 가장 작은 자연수라고 하자. 그러면 A#=□n+1 이다. 보조정리 27.6 에 의해서 A#=□n+1={m: m<n+1} ={m: m≤n} 이다. 보조정리 27.5 를 두 번 적용하면 M, w  A 인 꼭 그 경우 rk(w)∈A 이고 꼭 그 경우 모든 i<rk(w) 에 대해서 i∈B 이고 꼭 그 경우 rk(w)≤n 이고 꼭 그 경우 rk(w)∈A# 이고 꼭 그 경우 M, w  A# 이다. 따라서 M, w  A 일 경우 그리고 오직 그 경우에만 M, w  A# 이고 A↔A# 는 다시 타당하다.

표 27.1 이 옳다는 것은 이제 검증할 수 있다.

Prov() 와 진리함수적 연결사를 반복해서 적용해 0=1 로부터 만들어진 Z 의 임의의 문장 S 에 대해서, 곧 보기를 하나 들어보면

에 대해서 우리는 Z S↔S′ 를 만족하는 거짓 문장 0=1, Prov(0=1), Prov(Prov(0=1)) 등의 진리함수적 결합 S′ 를 찾을 수 있다. S 가 주어지면 문장문자를 전혀 포함하지 않고 AØ=S 를 만족하는 A 를 찾아 낼 수 있다. (ø 는 임의로 골라 낼 수 있다. A 는 문장문자를 포함하지 않으므로 모든 A Ø 는 똑같다.) 그러면  Z AØ↔A#Ø 이고, 그래서 우리는 S′=A#Ø 라고 할 수 있으며, 이 식은 0=1, Prov(0=1) 등의 진리함수적 결합이다. 따라서 그런 임의의 S 의 진리값은 증명가능성 값이 계산될 수 있듯이 계산될 수 있다. 왜냐하면 S 가 증명가능할 경우 그리고 오직 그 경우에만 Prov(S) 가 참이기 때문이다.

고호 정리

p0, ..., pn-1 은 문장문자의 일련체라고 하자. 그러면

이다.

증명. 여느 때처럼 M, 곧 <W, R, P> xRy y □A→A (y   A x   □A) x □A→A (*)

이제 w □(∧{(□pi→pi)| i<n}→-□n) 이고 w -□n i<n w □pi→pi

보조정리 27.5와 27.6 에 의해서 rk(w)≥n 이다. 따라서 어떤 w0, ..., wn-1 에 대해서 wRwn-1R...Rw0 이고 각 j<n 에 대해서 rk(wj)=j 이다. j<n 이라고 가정하자. 그러면 wRwj 이고 따라서 wj (∧{(□pi→pi)| i<n}→-□n) 이다. rk(wj)<n 이므로 wj □n 이다. 따라서 wj ∧{(□pi→pi)| i<n} 이고, 어떤 i<n 에 대해서 wj (□pi→pi) 이다. 따라서 모든 j<n 에 대해서 wj (□pi→pi) 를 만족하는 어떤 i<n 이 있다. (*) 에 의해서 모든 i<n 에 대해 wj (□pi→pi) 를 만족하는 어떤 j<n 이 많아야 하나 있다. 따라서 모든 i<n 에 대해 wj (□pi→pi) 를 만족하는 어떤 j<n 이 적어도 하나 있다. 만약 ∀j<n∃i<nRij 이고 ∀i, j, k < n(Rij&Rik→j=k) 이면 ∀j<n∃i<nRij 이다. 모든 j<n 에 대해서 wRwi 이므로, (*) 는 모든 i<n 에 대해서 w (□pi→pi) 를 함축한다.

Z1=Z 라고 하고 Zn+1 은 Zn 의 일관성 (곧 0=1 의 Zn 에서의 증명불가능성) 을 표현하는 Z 의 언어의 문장 Conn 을 Zn 의 공리들을 붙여서 Zn 으로부터 얻은 이론이라고 하자. Conn 은 Z 에서 문장

과 동치이다 (n=1 이면 똑같다). Z 의 모든 정리는 (에서 ) 참이고, 따라서 어떠한 거짓 문장도 Zn 의 정리가 아니며 Zn 는 일관적이며 Cn 은 참이다.

G □B→□□B 이고, 따라서 만약 n≤m 이면  G □n→□m이고  G -□m→-□n 이며, 산수의 건전성 정리에 의해서  Z Cm→Cn 이다. 그러나 만약 m<n 이고  Z Cm→Cn 이면 m+1≤n 이고, 방금 본 것처럼  Z Cn→Cm+1 이고 거기서  Z Cm→Cm+1 이 된다. 대우명제로 바꾸어 룁의 정리를 적용하면  Z -Cm 을 추론할 수 있는데 어떠한 거짓 문장도 Z 의 정리가 아니므로 이것은 불가능하다. 따라서 n≤m 일 경우 그리고 오직 그 경우에만  Z Cm→Cn 이다.

반사 원리 (reflection principle) 란 문장 Prov(S)→S 이다. 룁의 정리는 만약 반사 원리가 증명가능하면 그 귀결도 증명가능하다는 것을 주장한다. Z 와 일관적인 어떠한 문장도 모든 반사 원리를 함축하지는 않는다. 그 까닭은 이렇다. 만약 모든 S′ 에 대해서 Z S→Prov(S′)→S′ 이면 특히

이다. 명제 연산에 의해서 Z (Prov(-S)→-S 이고, 그러면 룁의 정리에 의해서  Z -S 이고 S 는 Z 와 비일관적이다.

C1 곧 -Prov(0=1) 은 Z 에서 반사 원리 Prov(0=1)→0=1 과 동치이다. C2 곧 -Prov(Prov(0=1)) 는 Z 에서 두 개의 반사 원리

와 Prov(0=1)→0=1 의 연언과 동치이다. 그리고 비슷한 방식으로 Cn 은 n 개의 반사 원리들의 연언과 동치이다.

Cn 이 그것을 함축하는 n 개의 반사 원리들의 연언을 함축한다는 것은 교호 정리로부터 따라나온다.

이라고 가정하자. 그러면

이다. p0, ..., pn-1 이 n 개의 문장문자의 일련체라고 하고 각 i<n 에 대해서 ø(pi)=Si 라고 하자. 그러면

이다. 교호 정리와 산수의 건전성 정리에 의해서

이다. 따라서

곧

이다.

이외에 n 개보다 적은 반사 원리들의 어떠한 연언도 Cn 을 함축하지 않는다는 것이 따라나온다. 그 까닭은 이렇다. 만약 B 가 m 개의 반사 원리의 연언이고 m<n 과 Z B→Cn 이면,  Z Cn→Cm 이므로  Z B→Cm 이고 따라서  Z Cm→B 이고  Z Cm→Cn 인데 이것은 룁의 정리에 의해서 불가능하다는 것을 이미 보았다.  

연습문제

A=□(-p→□)→□(p→□) 라고 하자. HA 를 찾아라.