18828번 - 배중률교 서브태스크스페셜 저지언어 제한번외

세상에서 가장 많은 신자 수를 거느리는 종교는 뭘까요? 기독교? 불교? 천주교?

물론 그럴 수도 있습니다. 하지만 이 세상을 거의 잠식하고 있는 무시무시한 종교가 있는데, 그것은 바로 배중률교입니다. 배중률은 아무 명제 P에 대해, P이거나 P가 아니라는 믿음이고, 배중률교는 배중률을 믿는 종교입니다. 이 문제를 읽으시는 여러분 중 적어도 99%는 이 종교를 믿고 있으리라 짐작합니다. 심지어는 교리를 뼛속 깊이 이해하고 믿고 있는 나머지 "그게 아니야?"라는 의문을 던졌을 수도 있겠습니다.

실제 종교 교리에서는 배중률교의 존재를 알기에 직접 드러내지는 않습니다만, 여러 교리 및 경전의 해석에서 다른 종교 신자들의 배중률교적 해석이 들어가게 됩니다. 예를 들어 불교의 경우, 有心으로 일컬어지는 도와 無心 사이의 차이를 얘기하는 칼럼이 있습니다. 제목 "모든 실상은 있음과 없음 양면이 있다"에서 유추할 수 있듯이, 있음이 아니고 없음도 아닌 중간을 배제하는 사고를 하고 있음을 알 수 있습니다.

그러나, 예를 들어, 명제 P : "P는 증명 불가능하다"와 같은 명제를 생각할 경우, 배중률교를 믿으면 P이거나 P가 아니어야 합니다. 또한 또 다시 배중률에 의해 어떤 명제 P는 증명 가능하거나 증명 불가능합니다. 만일 P가 아니라면, P는 증명 불가능하지 않기 때문에 증명이 가능하고, 따라서 P가 되어 모순이 이끌어집니다. 따라서 P일 수밖에 없는데, 이는 굉장한 사실을 함의합니다: 증명이 불가능하지만 참인 명제가 있다.

이 비직관적인 사실이 도대체 어디에서 기인한 것일까요? 이는 증명이 존재하지 않는 배중률 forall P : Prop, P \/ ~P을 증명 없이 단순히 믿어 버린 데서 있습니다. 사람이 보기에 직관적인 배중률을 기반으로 사람이 보기에 비직관적인 명제 P를 만들어서 보여 드린 것뿐입니다.

배중률은 다른 논리 법칙들로부터 증명이 가능할까요? 그건 모릅니다만, 만일 증명을 만들 수 있으면 떼돈을 벌 수 있습니다. 배중률의 증명이 있다고 합시다. 예를 들어 리만 가설을 그 증명에 넣으면, 그것이 증명이기 때문에 "리만 가설은 참이야, 그래서 리만 가설은 참이거나 거짓이야!"라고 얘기하거나 반대로 "리만 가설은 거짓이야, 그래서 리만 가설은 참이거나 거짓이야!"라고 얘기해 줄 것입니다. 여러분은 그 증명이 리만 가설에 대해 참이거나 거짓을 판단하는 과정을 보고 백만 달러를 타 가실 수 있습니다. 다른 여러 추측들도 마찬가지겠죠.

배중률을 믿지 않는 사람들을 직관주의자라고 합니다. 조심해야 할 것은 배중률을 믿지 않기 때문에 배중률이 증명될 수 없다고 거짓이라고 생각한다는 것은 아닙니다. 단지 배중률이 증명되지 않은 명제일 뿐, 거짓이 아니라고 믿는 것뿐입니다. (배중률을 믿지 않기 때문에 거짓이 아니라고 참인 것은 아닙니다.) 배중률을 믿지 않는 키파에게 구대기는 배중률교의 교리를 전파합니다.

구대기 : 모든 명제는 참 또는 거짓이야!
키파 : 그거 좀 이상한 주장인데. 증명할 수 있어?
구대기 : 너 명제가 거짓이 아니면 참이라고 생각하니?
키파 : 그건 당연한 거 아님? 아닌 게 아니면 맞는 거잖아.

평소 친구들 사이에서 득실한 배중률교 신자로 인정받던 구대기는 키파의 믿음을 통해 키파를 설득하기로 했습니다. 키파의 믿음은 귀류법이라고 부르는데, 배중률교 교리 넘버 1이 배중률이라면 귀류법은 넘버 2쯤 되는 녀석입니다. 배중률 forall P : Prop, P \/ ~P과 귀류법 forall P : Prop, ~~P -> P은 직관주의자들 사이에서도 동치로 알려진 명제입니다.

구대기 : (증명을 만들어서 보여 줌)
키파 : 우와 그렇네. 그런데 그러면 "거짓이 아니면 참"도 틀렸을 수 있잖아?
구대기 : 에휴... 네가 좋아하는 성질을 얘기해 봐. 그 성질에 대해서 배중률을 증명해 줄게.
키파 : 소수! 제곱수!
구대기 : 좋아. 아무 자연수가 주어지면, 그 성질이 성립하거나 성립하지 않음을 보여 주지.

여러분은 구대기를 도와 귀류법을 가정하고 배중률을 증명하고, 주어진 자연수가 소수이거나 소수가 아님, 제곱수이거나 제곱수가 아님을 증명해야 합니다.

증명은 Coq이라는 증명 보조 도구를 사용해서 합니다. 이 파일을 받아서 Code.v의 내용을 채운 후 Code.v를 제출하세요. Coq을 전혀 모르시는 분들이라도 검색해 볼 키워드가 있도록, Example.v에 간단한 Coq 프로그래밍 방법을 준비했습니다.

Coq을 사용하시려면, 여러분의 컴퓨터에 coqide를 설치하는 것이 가장 쉽습니다. 이 경우 coqide의 Make 메뉴를 이용해서 컴파일을 한 번 해 줘야 정상 작동하며, Make makefile은 절대 누르지 마세요. emacs의 company-coq 플러그인을 사용하시는 경우 make를 한 번 해 주시면 됩니다.

증명을 시도하려고 하는 문제는 주석 (* ... *)을 풀어서 시도하실 수 있습니다. 부분 점수를 노리는 경우, 컴파일 에러를 받지 않도록 반드시 증명하지 못한 정리는 주석을 넣어서 제출해 주세요. 이 이유로 컴파일 에러를 받는 경우 에러 메세지는 "(in proof [proof name]): Attempt to save an incomplete proof"입니다.

Axiom이나 Admitted와 같은 증명하지 않고 증명한 것처럼 정리를 쓰게 해 주는 단어들은 금지되어 있습니다. ./compile.sh를 통해서 확인해 볼 수 있습니다.

double_negation_excluded_middle의 증명이 있어야 합니다.

excluded_middle_square의 증명이 있어야 합니다.

excluded_middle_prime의 증명이 있어야 합니다.