L을 양화사,variable , 상수 0, 함수 기호 S를 포함하는 formal language, I를 페아노 공리계를 만족하는 자연수 집합을 포함하는 모델이라고 하자. 


그리고 0, S(0), SS(0), ....와 같이 S가 n개 있는 기호를 n'으로 표현하자.  0' 은 그냥 0이고,  3'은 SSS(0)이다. 그리고 n'은 모델의 자연수 원소인 n에 대응한다.


그리고 L은 유한 개의 symbol들을 갖고, 모든 formula들은 finite length를 가진다. 즉, 주어진 기호들의 나열이 명제인지, free variable을 가지는지 등 일반적인 1st order logic 구조를 갖고, 이 구조를 분석할 수 있는 알고리즘이 있다는 것이다. 그리고 L의 모든 명제들의 집합과 모든 formula들의 집합은 countably infinite하다. 


그냥 일반적인 1st order logic을 생각하면 된다. 


알고리즘이 존재한다는 것은, 컴퓨터 코드로 구현 가능하다는 의미로 생각하면 된다. 

알고리즘은 주어진 input에 대해, 언제나 동일한 동작을 하면 된다. 동작으로는 error를 뱉어 내도 되고, 무한 loop에 빠져도 되고, 아무 것도 반환하지 않고 종료해도 되고, true나 false 등을 반환해도 된다. 하지만, input이 동일하면 동일한 동작을 해야 한다. 



핵심정인 정의들을 간략하게 설명해 주자면, 


집합 X의 부분 집합 P에 대해, P가 effectively decidable하다는 것은, 임의의 X의 원소 n에 대해, n이 P의 원소인지 아닌지를 판단하는 알고리즘이 존재한다는 것이다.


L의 theory라는 것은 모든 원소가 L의 명제(혹은 formula)들로 이루어진 집합이라고 생각하면 된다. 


명제 R이 theory T의 theorem이라는 것은 T로부터 R이 증명 가능하다는 것이다. 


theory T가 consistent하다는 것은, 임의의 명제 R에 대해, T로부터 R 또는 ~R 둘 중 하나 이상은 증명할 수 없다는 것이다. 


theory T가 sufficiently strong하다는 것은, 

임의의 effectively decidable한 자연수 집합의 부분집합 P에 대해, 어떤 formula R(x)가 존재하여, R(x)는 한 종류의 free variable을 갖고, 모든 n∈N에 대해, n∈P이면, TㅏR(n')이고, n이 P의 원소가 아니면, Tㅏ~R(n')이라는 것이다. (다른 말로는, T가 formula R(x)로 집합 P를 표현할 수 있다는 의미이다.)


theory T가 effectively axiomatized하다는 것은, 

                        1. L의 formula들이 T의 원소인지 아닌지 알고리즘에 의해 판다할 수 있다. 

                        2. 임의의 명제들의 유한 나열이 T로부터의 증명인지 아닌지를 알고리즘에 의해 판단할 수 있다. 

                        3. 임의의 명제 R에 대해, 임의의 증명(명제들의 유한 나열)이 TㅏR의 증명인지 아닌지를 알고리즘에 의해 판단할 수 있다. 


theory T가 decidable하다는 것은, 임의의 명제 R이 T의 theorem인지 아닌지를 알고리즘에 의해 판단할 수 있다는 것이다. 


집합 X가 effectively enumerable하다는 것은, X가 공집합이거나 어떤 함수 f : N -> X가 존재하여, f가 surjection이고, 어떤 알고리즘이 존재하여, 임의의 자연수 n에 대해, f(n)을 해당 알고리즘으로 계산할 수 있다는 것이다. 그냥 f(n)이 계산 가능하다고 생각하면 된다. 좀 더 직관적으로는, X의 원소들을 열거할 수 있는데, 각 n번째항을 계산할 수 있다는 것이다. (참고로, f가 injective할 필요는 없다.)  효과적으로 열거하자고 표현하자. 


그러면, 다음의 정리가 성립한다. 


Lemma 0 ) A가 effectively enumerable이고, B가 effectively decidable in A라면, B도 effectively enumerable하다. 

간략 설명 : A가 공집합인 경우는 자명하고, A가 공집합이 아니면 A를 효과적으로 열거한 뒤에, 각각의 n번째 항이 B의 원소인지 아닌지를 알고리즘에 의해 판단할 수 있으므로 그러한 B의 원소들이 나올 때마다 차례대로 b0, b1, b2, ... 라고 표현하면 된다.


 

Lemma 1) 모든 L의 formula들의 집합은 effectively enumerable하다. 

간략 설명 : 이는 length를 기준으로 모든 기호들의 유한 나열을  열거할 수 있고, 각 n번째 항을 계산할 수 있고, 각 n번째항이 formula인지 아닌지를 알고리즘에 의해 판별할 수 있으므로 formula들인 것들에 순서를 주면서 다시 나열할 수 있기 때문이고, n번째 formula들을 계산할 수 있기 때문이다. 



Lemma 2) T가 effectively axiomatized theory면, T의 모든 theorem들의 집합은 effectively enumerable하다. 

간략 설명 : 

명제들의 집합이 effectively enumerable하므로, 

명제들의 유한 수열들의 집합도 effectively enumerable하며,    (자연수의 유한 수열을 모두 모아 놓은 집합이 effectively enumberable하다.)

명제들의 유한 수열이 T의 proof인지 아닌지 판단할 수 있으므로

T의 proof들의 집합이 effectively enumerable하고, 

각 proof로부터 해당 proof에서 유도된 명제(마지막으로 나열된 명제)를 계산할 수 있기 때문이다. 




  Thm)  No consistent, sufficiently strong, effectively axiomatized theory of arithmtic is decidable.


pf) 핵심은  자연수 집합의 모든 decidable 부분 집합들의 집합이 effectively enumerable하지 않다는 것을 이용하는 것이다. 



귀류법을 쓰자. T가 consistent, sufficiently strong, effectively axiomatized, decidable theory 라고 하자. 


그리고 S={ R(x) | R(x)는 free variable이 x 한 종류인 L의 formula}이다. 

그러면, 주어진 formula를 분석해서, S의 원소인지 아닌지를 계산할 수 있으므로, S는 모든 formual들의 집합에 대해 decidable하다. 


즉, S는 effectively enumerable하다. 


그러면, S의 원소들을 s0(x), s1(x), s2(x), .... 라고 하자. sn(x)들은 계산될 수 있다.


이제, P={m∈N | Tㅏ~sm(m')}이라고 하자. 


그러면, 임의의 자연수 n에 대해, sn(x)가 계산 가능, sn(n')은 x에 n'을 대입하면 되므로 계산 가능, ~sn(n')도 계산 가능, T가 decidable하므로 Tㅏ~sn(n')인지 

계산 가능, 따라서 n∈P인지 아닌지 계산 가능하다. 


따라서 P는 N의 decidable subset이다. 그러면, T가 sufficiently strong하기 때문에 T가 P를 표현할 수 있는 S의 원소 R(x)가 존재한다. 


즉, 모든 자연수 n에 대해, n∈P이면 TㅏR(n')이고, 그렇지 않으면 Tㅏ~R(n')이다. 


그리고 수열 s0(x), s1(x), ... 은 surjective하므로, 어떤 자연수 m에 대해, sm(x)는 R(x)이다. 


근데, m∈P이면, Tㅏ~sm(m')이고, T는 consistent하므로 T는 sm(m')을 유도할 수 없고, P가 sm에 의해 표현되므로 T는 sm(m')을 유도해야 한다. 


m이 P의 원소가 아니면, T는 ~sm(m')을 유도할 수 없고, T~sm(m')을 유도할 수 없고, P가 sm에 의해 표현되므로 T는 ~sm(m')을 유도해야 한다.


두 경우 모두 모순이 발생했다.


따라서 consistent, sufficiently strong, effectively axiomatized, decidable theory 는 존재할 수 없고,


consistent, sufficiently strong, effectively axiomatized theory는 undecidable theory이다.