여기서 저번에 콜라츠 추측의 증명불가능성에 대해 질문을 남겼는데, 황당한 답변들이 달리는걸 보고 증명가능성에 대해 정리를 해보려고 한다.

물론 엄밀한 수리논리나 증명이론의 언어로 쓴건 아니니 자세한건 전공서적을 참고하기 바람. 


우선 참과 증명가능에 대해서 엄밀하게 이야기를 할 필요가 있는데 어떤 이론(공리계) T 가 있어서 명제 A가 증명가능하다는 것은 명제 A의 결론을 수반(entailment)하는 논리적 귀결이 존재한다는 것이고, 기호로는 T ⊢A 라고 표기한다. A를 증명하는 증명이 있으면 증명가능하다 라고 하는것이다. 


그리고 참 이라는것은 기호로는 T ⊨ A 라고 표기를 하는데 이것은 이론 T의 모든 모델중에서 A가 거짓인 모델이 없다는 것이다. 여기서 모델이라는 것은 간단하게 해석(interpretation)이라고 할 수 있는데,  해석이라는 것은 정말 간단하게 말해서 명제 T에서 증명하지 못하는 여러 명제들에 대한 가치(참 or 거짓)을 모순없이 부여해주는 거라고 생각하면 된다.  해석이란것을 간단히 말하면 ZF 공리계에서 명제 M = "실수의 모든 집합은 measurable하다" 라고 하자. 그러면 우리는 M이 참인 모델 S를 만들수도, 거짓인 모델 C를 만들수도 있다.  즉 참이라는 것은 어떤 경우에도 절대로 거짓일수가 없는 명제라고 생각하면 된다. 

자 그러면 참과 증명가능성을 1차 술어논리로 살펴보기로 하자.

만약 내가 정말 단순한 이론 T를 만들었다고 하자. 여기에는 단 하나의 공리밖에 없다. ¬¬A→A

자 그러면 여기에서 명제 P = "A→(B→A)"  생각해보자. 이 명제는 진리표를 만들어보면 당연히 참이다. 하지만 이론 T 는 공리가 부족해서 해당 명제 P를 증명할수가 없다. 그렇기 때문에 명제 M은 참이지만 증명불가능하다. 

물론 1차 술어논리는 완전성이 보장되어 있다. 완정성이라는 것은 참인 명제는 항상 증명가능하다는 것인데 1차 술어논리에서는 몇가지 axiom만 있으면 완전한 공리계를 만들수가 있다. 

하지만 괴델이 불완정성 정리에서 증명하였듯, 자연수를 포함하는 공리계는 필연적으로 불완전하다. 즉, 어떤 공리계이든 증명불가능한 명제가 존재한다는 것이다. 
이것의 가장 간단한 예시는 Goodstein sequence 라는 것인데 (https://en.wikipedia.org/wiki/Goodstein%27s_theorem),  이 수열이 유한한지, 무한한지가 주요 쟁점이다. 재밌는것은 페아노 공리계에서는 이 수열이 무한한지를 증명하는것이 불가능함이 알려져있다. 하지만 ZF공리계에서는 이 수열의 유한성을 증명할수 있기 때문에 페아노 공리계 관점에서는 이 수열의 유한성은 참이지만 증명불가능한 명제인 것이다. 여담으로 이 명제가 페아노 공리계에서 증명불가능한 이유는 이 수열의 길이가 너무나 길어서 (fast-growing hierarchy 기준으로 ε0) 페아노공리계의 언어로는 도저히 표현할 수가 없기 때문이다. 

자 그러면 콜라츠 추측으로 넘어가자면, 질문자는 콜라츠 추측이 ZFC공리계에서 증명 불가능함이 증명된다면 사실상 참이 아니냐고 질문을 하였다. 만약 실제로 콜라츠 추측이 증명불가능으로 증명된다면 가능성은 크게 두가지 일 것이다.
1.  콜라츠 추측이 "참"이지만 공리계가 부족해서 증명불가능 한 경우
2.  콜라츠 추측이 실제로 "거짓" 이지만, 즉, 수열의 길이가 유한하지만 그 수열이 너무나도 길어서 ZFC의 공리계의 언어로 표현 불가능한 경우.

1번 케이스라면 충분히 강력한 axiom등을 추가해서 콜라츠 추측이 참임을 보일수 있을것이고, 2번케이스도 마찬가지로, 공리계를 확장해서 콜라츠 수열의 길이를 bound 하는 함수를 구할수도 있을 것이다. 물론 이 외에의 제3의 케이스도 있을수도 있을 것이다. 

이런 이유 때문에 콜라츠 추측이 증명불가능하다고 증명이 되었어도, 실제로 추측이 참인지 거짓인지는 모른다고 생각한다. 물론 그렇다고 콜라츠 추측이 ZFC공리계와 독립일 것이라고 추측하기도 어렵다고 생각한다. 앞으로 많은 연구가 진행이 되어야 알 것이라 생각한다.