논리학, 그 열여섯 번째 이야기 | 1차 논리에서의 완전성 정리 ( Completeness Theorem for First Order Logic )  By 초코맛 도비

이번 글에서는 1차 논리에서의 완전성 정리에 대하여 설명할 것이다. 완전성이란, 명제논리를 다룰 때 설명했듯이, 의미론적 함의 관계 가 구문론적 함의 관계 를 함의한다는 것이다. 즉, "Γφ이면 Γφ이다"라는 성질을 완전성이라고 한다. 1차 논리에서의 완전성 정리는 1차 논리는 완전하다는 정리이다. 1차 논리에서의 완전성 정리를 증명하기에 앞서, 그의 유명한 동치 명제에 대해 알아보도록 하자.

 

Theorem 1. Completeness Theorem and Its Equivalence

1차 논리 언어가 주어졌다고 하자. 그러면 다음 두 명제는 동치이다.
(a) Γφ이면 Γφ이다.
(b) ΓConsistent하면 ΓSatisfiable하다.

 

Proof.

Part (a) -> (b)

귀류법을 이용한 증명을 하기 위해 (a)가 성립하고 Γ가 consistent하지만, Γ가 satisfiable하지 않다고 가정하자.

그러면 임의의 ψΓ에 대하여 Aψ[s]가 성립하도록 하는 구조 A와 함수 s:V|A|가 존재하지 않으므로, 임의의 wff φ에 대하여 Γφ가 공허하게 참이다.

이때, (a)와 Γφ로부터 Γφ를 얻을 수 있으며, 비슷하게 Γ¬φ를 얻을 수 있다.

그런데, 이는 Γ가 consistent하다는 가정에 모순이다.

따라서 (a)는 (b)를 함의한다.

 

Part (b) -> (a)

귀류법을 이용한 증명을 하기 위해 (b)가 성립하고 어떤 wff φ에 대하여 Γφ이지만 Γφ라고 가정하자.

여기서 Γφ라는 사실에 주목하자.

Γφ이므로 Γ(φφ)가 성립함을 알 수 있으며, 따라서 Γ(¬φ¬φ)임을 알 수 있다.

이로 인해 Γ{¬φ}¬φ가 성립하며, Γφ라는 사실을 함께 생각하면, 이는 곧 Γ{¬φ}가 unsatisfiable함을 의미한다.

따라서 (b)에 의해 Γ{¬φ}는 inconsistent하게 되고, 폭발 원리에 의해 Γ{¬φ}φ임을 알 수 있다.

따라서 연역 정리에 의해 Γ¬φφ가 성립한다.

처음의 Γφ라는 가정과 배중률을 함께 적용하면, Γ¬φ임을 알 수 있으며, 위에서 얻은 결론과 함께 MP를 적용한다면, Γφ를 얻을 수 있다.

이는 처음의 Γφ라는 가정에 모순이다.

따라서 (b)는 (a)를 함의한다.

 

이번 글에서 동치명제를 먼저 소개한 데에는 이유가 있는데, 완전성 정리를 직접 증명하는 것보다는 그의 동치명제를 증명하는 것이 더 간단하기 때문이다. 그럼 다음 정리를 보자.

 

Theorem 2. 1차 논리에서의 완전성 정리 ( Completness Theorem for First Order Logic )

1차 논리 언어 L이 주어졌다고 하자. L의 wff의 집합 Γ와 wff φ가 주어질 때, ΓφΓφ를 함의한다.

 

Proof.

Theorem 1에 의해 consistent하면 satisfiable하다는 것만 보여도 충분하다.

1차 논리 언어 LL의 wff의 집합 Γ가 주어졌으며, Γ가 consistent하다고 가정하자.

이 증명의 대략적인 개요를 설명하자면, 임의의 consistent한 Γ를 maximal consistent set Δ로 확장 가능하다는 것을 보인 후, maximal consistent set Δ가 satisfiable하다는 것을 보이는 방식으로 정리를 증명할 것이다.

먼저, Γ를 어떻게 확장할 수 있는지에 대해 논의해보자.

일단, L의 기수가 무한기수 λ라고 하자. 즉, L의 모든 변수의 집합의 기수가 λ라고 하자. 그러면 자명하게 L의 모든 wff의 집합의 기수 역시 λ이다. 만약 L의 변수의 집합이 유한집합이라면 가산개의 변수를 추가하여 변수의 집합이 가산무한집합이 되도록 하면 아래의 논의를 이어나갈 수 있다.

이제 L의 constant symbol이 아닌 새로운 λ개의 constant symbol의 집합 C를 생각하고, 이 새로운 constant symbol들을 포함하는 언어 L=LC를 생각하자. 이때, C는 정렬된 집합으로 간주하자.

만약 ΓL에서는 inconsistent하다고 가정하면, Γα이면서 Γ¬αL의 wff α가 존재한다.

그러면 Generalization on Constants에 의해 Γ¬αyc이고 Γαyc이도록 하는 변수 y가 각 constant symbol c에 대하여 존재한다. 이때, α에 등장하는 C의 원소가 유한하므로 Γ¬α이고 Γα이도록 하는 L의 wff α이 존재한다.

이는 Γ가 consistent하다는 것에 모순이므로 ΓL에서도 consistent함을 알 수 있다.

이제 φL의 wff이고 x가 변수인 순서쌍 (φ,x)λ-수열 (φi,xi):i<λ를 생각하자. 단, 이 수열에서 wff φi는 중복되는 것이 없으며, 변수 xi 역시 중복되는 것이 없다. 또한, 모든 wff는 이 수열에서 적어도 한 번 등장하며, 모든 변수 역시 이 수열에서 적어도 한 번씩은 등장한다. 이러한 수열은 1차 논리 언어 L의 기수가 λ이기 때문에 존재한다.

이제 θ0(¬x0φ0)(¬φ0c0x0)로 정의하자. 이때, c0φ0에 등장하지 않는 C의 원소 중 첫 번째 원소로 정의된다.

이제 0이 아닌 순서수 ξ<λ에 대하여 θξ(¬xξφξ)(¬φξcξxξ)로 정의하자. 이때, cξφξγ<ξθγ에 등장하지 않는 C의 원소 중 첫 번째 원소로 정의된다.

또한, Θ={θξ|ξ<λ}, Θξ={θγ|γξ}라고 하자.

만약 ΓΘ가 inconsistent하다면, 연역과정이 유한하다는 사실로부터 ΓΘξ가 inconsistent한 xi가 존재한다.

그러한 ξ 중 최솟값을 생각하자.

만약 ξ=0이면, 귀류법에 의해 Γ¬θ0이다.

그러면 공리꼴 (A1), (A2), (A3)에 의해 Γ¬x0φ0이며 Γφ0c0x0임을 알 수 있다.

그런데, c0Gammaφ0에서 등장하지 않으므로 Generalization on Constants의 따름정리에 의해 Γφ0c0x0으로부터 Γx0φ0임을 알 수 있으며, 이는 Γ의 consistency에 모순이다.

만약 ξ가 따름 서수라면, ξ=γ+1γ를 선택하자.

만약 ξ0이 아닌 극한 서수라면, 연역과정은 유한하다는 사실로부터 고정된 wff β에 대하여 θγΓΘξ로부터 β 또는 ¬β로의 연역과정에 등장하는 γ<ξ 중 가장 큰 순서수를 γ로 선택하자.

그러면, ΓΘγ{θξ}는 inconsistent함을 알 수 있다.

이때, 귀류법에 의해 ΓΘγ¬θξ가 성립하며, 공리꼴 (A1), (A2), (A3)에 의해 Γ¬xξφxi이며 Γφξcξxξ임을 알 수 있다.

cξΓΘγφξ에서 등장하지 않으므로 Generalizatoin on Constants의 따름정리에 의해 Γφξcξxξ로부터 Γxξφξ를 얻을 수 있으며, 이는 ΓΘγ가 inconsistent함을 의미한다.

하지만, γ<ξ이며, ξΓΘξ가 inconsistent한 최소의 서수이므로 ΓΘγ가 inconsistent한 것은 모순이다.

따라서 ΓΘ는 consistent하다.

이제 maximal consistent set Δ를 구성할 차례이다.

먼저, ΓΘ{φ0}가 consistent하다면, 이것을 Δ0으로 정의하고, 그렇지 않다면, Δ0=ΓΘ{¬φ0}이라고 하자.

또한, 0이 아닌 서수 ξ에 대하여 γ<ξΔγ{φξ}가 consistent하다면, 이것을 Δξ로 정의하고, 그렇지 않다면, Δξ=γ<ξΔγ{¬φξ}라고 하자.

그리고 Δ=ξ<λΔξ로 정의하자.

만약 ΓΘ{φ0}이 inconsistent하다면, 귀류법에 의해 ΓΘ¬φ0이다. 이때, ΓΘ가 consistent하다는 것을 이미 위에서 보였으므로 ΓΘ{¬φ0}이 consistent하게 된다. 따라서 Δ0은 consistent하다.

이제 임의의 γ<ξ에 대하여 Δγ가 consistent하다고 가정하고 γ<ξΔγ{φξ}가 inconsistent하다고 가정하자.

그러면 귀류법에 의해 γ<ξΔγ¬φξ가 성립한다. 따라서 γ<ξΔγ가 consistent하다면, Δξ 역시 consistent함을 알 수 있다.

만약 γ<ξΔγ가 inconsistent하다면, 연역과정이 유한하므로, 고정된 wff β에 대하여 β 또는 ¬βγ<ξΔγ의 연역과정에서 등장하는 모든 ψγ<ξΔγ에 대하여 ψΔγ가 성립하도록 하는 γ의 최댓값이 존재한다.

이는 곧 Δγβ이면서 Δγ¬β임을 의미하며, 이는 귀납가정에 모순이다.

 따라서 γ<ξΔγ는 consistent하며, 이로 인해 Δξ 역시 consistent하다.

비슷한 논리로, Δ 역시 consistent함을 알 수 있다.

또한, 이후의 논의에서 Δ의 중요한 성질이 사용될 것이므로 해당 성질을 미리 증명하자.

만약 φΔ라면, Δφ임은 자명하다.

만약 Δφ이면, Δ가 consistent하므로 Δ¬φ이다.

따라서 ¬φΔ임을 알 수 있으며, 따라서 φΔ이다.

이제 Δ가 satisfiable하다는 것을 보이면 증명이 끝난다.

그러기 위해 Δ를 이용하여 L에서 등호 =2항 predicate symbol E로 대체한 언어의 구조 A를 구성할 것이다. 다음을 만족하는 구조 A를 생각하자.

(a) A의 universe |A|L의 모든 term의 집합이다.

(b) 두 term u, t에 대하여 (u,t)EA인 것은 (u=t)Δ인 것과 동치이다.

(c) 각 n항 predicate symbol P에 대하여 PA는 다음과 같이 정의된다.

(t1,t2,,tn)PA인 것은 Pt1t2tnΔ인 것과 동치이다.

(d) 각 n항 function symbol f에 대하여 함수 fA는 다음과 같이 정의된다.

fA(t1,t2,,tn)=ft1t2tn

또한, 함수 s:V|A|s:xx로 정의하자.

그러면 임의의 term t에 대하여 s¯(t)=t임을 귀납법을 통해 쉽게 알 수 있다.

 

이제 EA가 동치관계임을 보이자.

먼저, xEAxx=xΔ인 것과 동치이고, 이는 Δ의 성질에 의해 Δx=x와 동치이다. 그런데, x=x이므로 Δx=x가 성립함은 자명하며, 따라서 xEAx이다. 즉, EA는 반사적이다.

이번엔 EA가 대칭적이라는 것을 확인하자.

xEAy를 가정하면, x=yΔ임을 알 수 있으며, x=yy=x이므로 x=yΔΔy=x를 함의한다. 또한, 이는 Δ의 성질에 의해 Δy=x와 동치이며, 이는 yEAx와 동치이다.

이번엔 EA가 추이적이라는 것을 확인하자.

xEAyyEAz를 가정하면, x=y,y=zΔ임을 알 수 있으며, x=y,y=zx=z이므로 Δx=z임을 알 수 있다. 또한, 이는 Δ의 성질에 의해 x=zΔ와 동치이며, 이는 곧 xEAz임을 의미한다.

따라서 EA는 동치관계이다.

사실, EA는 동치관계일 뿐 아니라 A에서의 합동관계이다. 즉, 다음을 모두 만족한다.

(a) EA|A| 위의 동치관계이다.

(b) 각 n항 predicate symbol P에 대하여 다음이 성립한다.

(t1,t2,,tn)PA이고 동시에 각 1in에 대하여 tiEAti이면 (t1,t2,,tn)PA이다.

(c) 각 n항 function symbol f에 대하여 다음이 성립한다.

1in에 대하여 tiEAti이면 fA(t1,t2,,tn)EAfA(t1,t2,,tn)이다.

(a)가 성립함은 이미 위에서 보였으니 (b)와 (c)만 보여도 충분하며, (b)와 (c)가 성립함은 공리꼴 (E2)에 의해 자명하다.

따라서 몫구조 A/E를 다음과 같이 정의할 수 있다.

몫구조 A/E는 다음을 만족하는 구조이다.

(a) |A/E|=|A|/EA이다. 이에 대해서는 동치류와 몫집합을 참고하라.

(b) 각 n항 predicate symbol P에 대하여 다음이 성립한다.

([t1],[t2],,[tn])PA/E(t1,t2,,tn)PA와 동치이다.

(c) 각 n항 function symbol f에 대하여 다음이 성립한다.

fA/E([t1],[t2],,[tn])=[fA(t1,t2,,tn)]

또한, 함수 s:V|A/E|s:x[x]로 정의하자. 그러면 임의의 term t에 대하여 s¯(t)=[t]가 성립함은 자명하다.

이제 이렇게 정의된 구조 A/E에 대하여 φΔA/Eφ[s]가 동치임을 보이면, Δ가 satisfiable하다는 것이 보여지게 된다.

φΔA/Eφ[s]가 동치임을 보이기 위해 귀납법을 사용하자. 즉, 다음의 5가지 경우에 대해 살펴보자.

(i) φ가 원자명제인 경우

(ii) φ=(¬ϕ)인 경우

(iii) φ=(ϕψ)인 경우

(iv) φ=xϕ인 경우

 

먼저, (i)의 경우를 살펴보자.

φt=t 꼴의 wff인 경우, 다음의 과정에 따라 주장이 성립한다.

φΔifftEAtiff[t]=[t]iffs¯(t)=s¯(t)iffA/Et=t[s]

\varphiPt_1t_2\cdots t_n$꼴의 wff인 경우, 다음의 과정에 따라 주장이 성립한다.

φΔiff(t1,t2,,tn)PAiff([t1],[t2],,[tn])PA/EiffA/EPt1t2tn[s]

 

이제 (ii)의 경우를 살펴보자.

φnegϕ 꼴의 wff인 경우, 다음의 과정에 따라 주장이 성립한다.

φΔiffϕΔiffA/Eϕ[s]iffA/Eφ[s]

 

이제 (iii)의 경우를 살펴보자.

φϕψ 꼴의 wff인 경우, 다음의 과정에 따라 주장이 성립한다.

φΔiffΔφiff¬ϕΔ or ψΔiffA/E¬ϕ[s] or A/Eψ[s]iffA/Eφ[s]

 

이제 (iv)의 경우를 살펴보자.

이번에는 right-side와 left-side를 나눠서 증명할 것이다.

먼저 right-side를 생각해보자.

A/Exϕ[s]if onlyA/Eϕ[s(x|[t])]for some t|A|if onlyA/Eψ[s(x|[t])]by Alphabetic Variants & Soundness Theoremif onlyA/Eψtx[s]by substitutionif onlyψtxΔby inductive hypothesisif onlyxψΔif onlyxϕΔby Alphabetic Variants & Soundness Theorem

이 과정에서 Alphabetic Variants를 사용하여 서술을 우회한 것은 만약 이와 같이 우회하지 않고 논리를 전개하는 경우에는 tϕ에서 x에 대해 substitutable한 경우에만 성립하는 반쪽자리 증명이 되기 때문이다.

이제 left-side를 생각하자.

A/Exϕ[s]if onlyA/Eϕ[s(x|[c])]for some constant symbol c|A|if onlyA/Eϕcx[s]by substitutionif onlyϕcxΔby induction hypothesisif onlyxϕΔsince there exists a constant symbolc such that (¬xϕ)(¬ϕcx)Δ

따라서 귀납법에 의해 φΔA/Eφ[s]가 동치임이 증명된다.

즉, ΔL에서 satisfiable하다.

따라서 ΓΔ 역시 L에서 satisfiable함을 알 수 있다.

또한, L에서 L로의 자연스러운 축소를 통해 ΓL에서도 satisfiable함을 알 수 있다.

따라서 완전성 정리가 증명된다.

댓글()