Craig's re-axiomatization theorem

https://blog.naver.com/wnstkd1928/223318707075

괴델의 불완전성 정리를 공부하면서 발견한 짤막한 재밌는 주제입니다. 구성하고 있는 내용 자체는 논리학이나 수리철학이지만, 이에 둘러싼 내용은 과학철학과 연관되어 테그를 과학철학으로 했습니다.

Craig's theorem(Craig's interpolation theorem와는 구분될 필요가 있다)는 다음에 대한 따름 정리로 흔히 불려지는 것이다.

I. 공리들의 재귀적으로 열거적인 집합을 수용하는 모든 이론은 재귀적으로 공리화될 수 있다.

여기에는 몇 가지 사전 설명이 필요하다.

Def 1. 이론(a theory)은 wffs의 무한 집합인데, 이 때, wff들은 일반적인 추론 규칙에 의해 닫혀있다.

Def 2. 만일 T가 공리들의 집합 S를 가지는 이론이라면, 이 때, T의 subset인 S'가 다음의 조건을 만족하면, 이 때, S'는 T에 대한 공리들의 대체적인 집합(be called an alternative set of axiom for T)이라 한다 : "S의 모든 원소들이 S'안의 문장들로부터 연역될 수 있다"

Def 3. 집합 S가 재귀적이다(recursive) iff 이것은 결정가능하다(decidable), 즉 ,임의의 wff가 S에 속하는지에 대한 여부를 말할 수 있는 효과적인 절차(effective procedure)가 존재한다. 이 때, '효과적인 절차'를 우리는 '튜링 머신'으로 쓸 수 있다.

Def 4. 이론이 재귀적으로 공리화가능하다(recursively axiomatizable)이라는 것은 적어도 하나의 재귀적인 공리들의 집합이 존재한다.
참고로 모든 유한 집합은 재귀적이다. 따라서 유한한 공리들을 가진 모든 이론들은 재귀적으로 공리화가능하다.

Def 5. 집합이 재귀적으로 열거적이다는 것은 이 집합의 원소가 마찬가지로 효과적으로 생성(be effectively produced)될 수 있는 어떤 시퀸스 S_1, S_2, S_3, ...의 맴버일 때를 일컫는다(이 때, 효과적으로 생성된다 함은, 튜링 머신에 의한 것으로 흔히 이해된다).

이 때, 모든 재귀적으로 열거적인 집합이 재귀적인 것은 아니다. 간단히 말하자면, 양의 정수들의 집합 D는 재귀적으로 열거가능하지만 재귀적이지 않다. 가령, a_1, a_2,...인 수열은 우리가 원하는 대로 효과적으로 지속될 수 있는 수열이지만, 임의의 정수가 이 수열에 나타나는지를 항상 결정할 수 있는 이러한 원리를 지닌 방안은 존재하지 않는다(there is no method in principle).


그리고 어느 재귀적으로 공리화된 이론 T의 정리들의 집합은 마찬가지로 재귀적으로 열거적인 집합이다. 이것의 증명에 대한 발상은 T에서의 증명들을 전부 효과적으로 형성된 시퀸스로 배열하는 것이다(가령, 증명의 길이순으로). 만일 이러한 시퀸스의 결과인 proof_1, proof_2,...의 k번째 맴버인 proof_k를 proof_k에 의해 증명된 wff로 대체한다면, 우리는 T의 정리들로만 구성된, 그리고 그것들의 전부를 목록화 할 수 있다(물론 이는 무한하게 많은 증명과정에서 불필요한 재 반복을 제거할 수 있다는 것이 가정된다).

※역자 첨언 : 이에 대한 비형식적이고 다소 직관적인 증명을 구성하자면, 공리들의 집합이 재귀적이며, 증명은 그 자체의 정의에 따라 유한한 길이를 가져야 하기 때문에 가능하다.
우리는 공리들의 집합이 재귀적이기 때문에 공리를 결정할 수 있으며, 이로 부터 연역되는 정리들에 대한 각 증명들은 유한한 과정으로 이루어지기 때문에, 우리는 정리에 대한 증명의 각 단계가 얼마나 많은 길이로 구성되는지 셀 수 있다. 따라서 공리들을 결정하는 절차가 존재하고, 이로부터 정리들의 길이를 세는 절차 또한 존재하게 되기 때문에, 정리들에 관한 증명을 길이 순으로 나열하는 절차가 존재할 수 있다.

이제 I을 증명할 것인데, 이것은 모든 재귀적으로 열거적인 이론들은 재귀적으로 공리화된다는 것이다. 만일 이론 T가 재귀적으로 열거가능하다면(이는 공리들의 재귀적으로 열거가능한 집합을 가지는 것과 동치이다), T에 대한 공리들의 집합인 재귀적인 집합 S를 찾을 수 있다.

pf I) T가 재귀적으로 열거가능한 집합 S를 공리로 가지는 이론이라 하자. 그리고 그러한 공리들이 S1, S2,...가 되며, 이들의 공리들로 구성되는 효과적으로 생성된 시퀸스가 존재한다고 하자. 우리는 T에 대한 공리들의 대안적인 집합인 새로운 집합 S'를 구성할 것이다.

임의의 양의 정수 k에 대해, S'는 S_k∧(S_k∧(S_k∧(...))의 형태를 지닌 wff들을 포함한다고 가정하고, 이 때, 이 형식은 k개의 연언들로 이루어진 것이다.

이제 S'가 재귀적임을 보일 것 이다.

만일 A가 wff라하고, 이제, A가 S'에 속하는지를 결정하는 문제를 고려하자. 만일 A≠S1이고, A는 B∧(B∧(...))의 형태가 아니면, A는 S'에 속하지 않는다. 만일 A가 B∧(B∧(...))혀익을 가지고 이때 k개의 B들이라면, A가 S'에 속한다는 것은 B=Sk와 동치이다.

우리는 시퀸스 S_1, S_2,...를 S_k를 얻고, 이를 B와 비교할 때까지 진행할 수 있다. 그래서 만일 B=S_k라면, A는 S'에 속하며, 그렇지 않으면 S'에 속하지 않는다.

Q.E.D.

그런데 우리는 위에서 A가 S'에 속하는지에 대한 여부를 결정하는 방안을 거넬 수 있었지만, 우리는 임의의 wff C가 S에 속하는지를 결정하는 것에 대한 방안을 여전히 모른다. 왜냐하면, 우리는 S의 원소들의 시퀸스 S_1, S_2,...의 k까지의 initial sequence, 즉 S_1, S_2,...,S_k가 얼마나 긴지 모르기 때문에, C가 해당 sequence에 없어서 S에 없다고 말하려면, 우리는 그 이전에 S_k를 생성해야만 한다. 그런데 S'는 S가 이 문제를 해결하기에 좋은 형태를 지니지 않은 그러한 것일지라도, 결정가능하다.

(다음의 증명은 바로 위의 증명과 동일한 정리에 대한 증명인데, 강조된 부분들에 대한 해명이 증명의 과정에서 다소 언급되기 때문에 가져왔다.)

pf ver of J.K) T가 재귀적으로 열거가능한 집합 S를 공리로 가지는 이론이라 하자. 이 때, S의 원소는 재귀적으로 열거가능하기 때문에, F가 자연수로부터 이것의 문장으로 지정되는 재귀적 함수인 F에 의해 F(0), F(1),..., F(n),.. 형태로 열거가능하다(우리는 괴델의 코드화와 관련된 어떤 방법으로 이를 진행할 수 있다). 일반적으로, 재귀적으로 열거가능한 집합이 자동적으로 재귀적인 것은 아니지만, 'Craig(T) := T를 연역적 폐쇄계(deductive closure)로 가진다'를 구성함으로써 여기서는 가능하다.

A를 문장이라하고, n을 자연수라 하자. A^n을 n+1개의 연언들이 중첩된 연언문이라 하자. 즉, A∧...∧A. 문장 An은 A와 상호연역적이다. 그 다음 F(n)^n의 형태의 문장을 고려하자. 그리고 다음을 정의한다.

Criag(T) := {F(n)^n | n in |N }

이 경우 Criag(T)의 연역적 폐쇄계는 T가 되어야 한다. 왜냐하면 T와 Criag(T)의 원소들은 전부 동치이기 때문이다. 그 다음 Criag(T)의 맴버임을 결정하는 비형식적인 결정절차를 고려한다.

A가 주어진다면, A in Criag(T)를 결정하기 위해

  1. A가 어떤 문장 B와 어떤 자연수 n에 대한 B^n의 형식을 가지는지 확인한다.
    이는 unique redability에 의해 확인가능하다.

※역자 첨언 : unique readability는 first-order logic의 교과서에서 흔히들 정의되는 개념으로 대충 말하자면, 모든 wff들은 서로 구분되는 다양한 표현식들과 동치일 수 없다는 것이다. 이는 귀납법으로 증명이 가능하며, 가능하다면 추후에 다른 글에서 다룰 것이다.

만일 A가 B^n의 형식이 아니라면, A not in Criag(T). 그래서 이제 A가 B^n의 형식이라 하자.

  1. 우리는 F(n)을 계산할 수 있다. 그래서 만일 F(n)=B라면, A in Craig(T). 그렇지 않으면 not in Craig(T).

이러한 결정절차의 존재는 Craig(T)가 재귀적임을 함의한다. 집합 Craig(T)는 그러므로 이론 T의 재귀적인 공리화이다.

Craig's theorem은 이제 다음과 같이 진술될 수 있다.


II. T가 재귀적으로 열거가능한 이론이라하고, T의 술어 문자들을 두 개의 서로소 집합으로 나누자. 즉, V_A = {T_1, T_2,...} 그리고 V_B = {O_1, O_2,...} . 그리고 T_B를 T의 정리들로 구성된 집합이라 하되, 이는 오직 V_B의 술어 문자만 포함한다고 하자. 그렇다면 T_B는 재귀적으로 공리화된 이론이다.

pf II) S_1, S_2,...가 T의 정리들로 구성되는 효과적으로 생성된 시퀸스라 하자. subvocabulary V_B에 속하지 않는 wffs를 제거함으로써, 우리는 T_B의 맴버들을 V_1, V_2, ...로 말할 수 있게 된다. 따라서 T_B는 재귀적으로 열거적인 이론이며, 그리고 따라서 재기적으로 열거적인 공리화된 것을 얻는다.(이는 T_B 그 자체를 공리들의 집합 S로 취하면 된다). 따라서 I에 의해 T_B는 재귀적으로 공리화가능하다.

Q.E.D.

그러나 독자들은 여기서의 증명이 술어 문자 집합들, V_A, V_B가 그 자체로 재귀적임을 가정한 증명임을 확인할 수 있다; 엄격히 말하자면, 우리는 이에 대해 말해야 하지만, 실제로 이러한 집합들이 유한집합이라 하면, 이는 자명하게 재귀적이다.

※역자 첨언 : 인식론적인 상황으로 바라보자면, 실제로 무한한 집합은, 그 내용을 전부 확인하지 못하기 때문에 우리가 어떤 이론을 일일히 '완전하게' 다룰 수 있다 것은 이것들이 '실제로' 전부 확인할 수 있는 유한집합이여야 할 것이다. 따라서 굳이 유한집합임을 따로 가정하지 않아도 이러한 관점 하에선, 문제가 되지 않는 것이지만, 이 논문을 저술한 퍼트넘이 유한주의를 지지했는지는 미지수이며(역자 입장에서), 또한 유한주의에 대한 정당화가 필요할 것같다.

Craig's theorem의 철학적 중요성.

완전한 "과학의 언어"(entire "language of science)가 형식화 되는 것을 상상해보자, 그리고 원시적인 술어들(primitive predicates)을 두 부류들로 나눈다고 해보자 :

이른바 "이론적 용어들" T_1, T_2,...가 있고, 이른바 "관측 용어들" O_1, O_2,... 가 있다. 그리고 단일한 이론 T를 구성하기 위해, 이러한 언어로 형식화되는 과학의 주장들(assertions)을 상상해보자. T는 말할 것도 없이 매우 큰 이론일 것이다. 그리고 이론 T의 "예측들(predications)"은, 추정컨데, 단어 V_0 = {O_1, O_2,...}에 대한 T의 정리들 중에서 발견될 것이다.

이제 T_0을 관측적 단어 V_0로 표현되는 T의 모든 정리들로 구성되는 subtheory라 하자. 따라서 T_0에 속하는 문장은 단지 다음 두 조건을 만족하는 경우가 된다 :

  1. 문장은 이론적 용어들을 포함하면 안된다.

  2. 문장은 T의 공리들의 결론이여야 한다.

그렇다면, "Craig's theorem"은 T_0이 그 자체로 재귀적으로 공리화 가능한 것이라 주장한다 - 그리고 T_0은 명백히 T가 수행하는 모든 "예측들(predications)"을 포함한다!

이것은 몇몇 독자들에게 다음과 같이 읽힐 수 있다 : 과학의 목적은 성공적인 예측이기 때문에, 이론적 용어들은 이러한 원리 하에서 필수적이지 않다(theoretical terms are in principle unnecessary). 이러한 논쟁이 진행되면, 우리는 (이러한 원리 하에서) T를 전적으로 제외하고, 단지 T_0에만 의존할 수 있는데, 이는 T_0가 T가 수행하는 모든 예측들을 함의하기 때문이다. 그리고 T_0은 이론적 용어들을 포함하지 않는다.


과학에 관한 도구주의나 실증주의는 과학적 이론의 비관측적 내용에 회의적이다. 그러한 내용이 결여한, 재공리화 Craig(T)는 따라서, 도구주의나 실증주의의 이러한 회의와 양립할 수 있는(compatible with) 합리적인 믿음의 대상을 제공한다.


퍼트넘이 관측적 용어/이론적 용어의 두 서로소 class를 구성하여, 한 쪽을 제공한 이러한 제거 방식이 꼭 관측/이론의 구분 상에 기초할 필요가 없음에 주목하자. 이는 다양한 수정이 가능한데, 말하자면, 수학적 술어, 가령 집합에 대한 양화사, 함수, 등을 사용하여 형식화된 과학적 이론으로부터 수학적 내용을 제거하는 방식으로 사용될 수 있으며, 혹은 정신적 상태들을 언급하는 심리학적 이론들로부터 이론적 내용을 제거하는 방식으로도 이용할 수 있는 등 다양하다. 그래서 Craig의 재공리화는 다양한 실용주의적 입장들에 대한 가능한 제거 전략을 제공한다.

(이러한 Craig의 재공리화에 대한 비판은 추후 다룰 것이다)

출저

  1. Craig's theorem, 힐러리 퍼트넘(Hilary putnam, 1965), Journal of Philosophy.

  2. Craig's theorem, Jeffery Ketland, Logical Philosophy of Science(2012, fall), princeton.edu

4개의 좋아요