혼자서 공부하다가 도저히 이해되지 않는 부분이 있어서 질문드리고 싶습니다.
고정점의 형식은 다음과 같습니다. Q↔φ(Q)
이때 룁에 따르면 고정점이라는 개념을 사용하여 다음의 명제를 유도합니다. ⊢Q↔(ProvQ→P)
그러나 룁의 명제를 잘 보시면 Prov연산자 범위밖에 P가 존재합니다. 즉 룁의 명제는 고정점 명제의 형식이 아닌것 같습니다..
그런데 왜 룁은 이것을 고정점이라고 가정한채 논증을 합니까?
저는 룁의 명제가 왜 가정으로서 정당화되는지 도저히 이해가가지 않습니다.
수학적 트릭의 일종인것 같습니다만, P의 존재가 자명하지 않아보이기 때문입니다.
제 나름대로 최대한 이해해보려 했으나 도저히 한계가 있어 질문드립니다.
또한, 불완전성 정리에 대한 질문입니다.
프뢰게 등의 이론에 따르면, "눈은 하얗다“ 와 "Snow is white" 는 문장은 다르지만 같은 명제입니다. 즉 명제는 문장이 아니라 의미입니다.
만일 이러한 명제 의미론이 맞다면, 괴델이 불완전성 정리에서 괴델수 트릭을 이용하여 자기언급적 명제를 회피하려고 했던 시도가 무너지는 것처럼 보입니다.
명제가 문장이 아닌 의미라면, 괴델수 트릭을 이용하여 자기언급을 회피하였음에도, 의미상으로는 여전히 자기언급적이기 때문입니다.
이는 메타수학적 관점이 아닌 수학적 관점에서도 명제의미론이 적용되기 때문에 괴델수는 자연수라는 문장을 표현하였지만, 여전히 의미론적으로는 그것이 자연수가 아닌 특정한 의미를 품게되기 때문입니다. (그리고 괴델본인이 그 의미를 따릅니다)
즉 문장으로는 그럴듯하지만 의미론을 적용하는 순간 괴델수가 무력화되는 것으로 보여집니다.
저의 두가지 이러한 견해들에 대해 여쭙고 싶습니다.
몇 가지 개념을 혼동하고 계신거 같은데 읽고 있는 문서를 알려주시면 더 잘 이해할 수 있고, 다른 분들이 더 쉽게 알려주실 수 있을 것 같습니다.
답변 감사드립니다.
2번에 대해서는 곰곰히 생각해보았는데 제가 프뢰게의 지시체이론을 오해한것 같습니다. 죄송합니다.
1번에 대해 말씀하신바에 따르면 고정점명제는 자기언급명제와 동치이다. 라는 것으로 이해됩니다. 즉 자기언급명제의 또다른 표현이 고정점명제라는 것으로 이해됩니다. 위 이해가 올바르다면 제가 고정점의 정의에 대해 오개념을 갖고 있었던것 같습니다.
제가 의문을 가진 부분은 Q↔(ProvQ→P) 부분을 풀어써보면 "Q가 참이면 iff Q가 증명가능하면 P이다" 가 되는데
이때 이 명제가 과연 자명한가? 에 대해 의문을 갖었습니다. 고정점의 존재가 보장된다 하더라도 그 고정점이 반드시 위의 형태를 갖는것으로 볼수는없어보입니다.
하지만 그럼에도 lob은 Q↔(ProvQ→P) 를 가정한것인데, 이는 자신이 원하는 결론을 유도하기 위한 억측적인 가정에 불과한것 아니냐. 라는 의문을 품습니다.
이것에 대해 답변부탁드리면 감사하겠습니다
위에서 이미 다른 분께서 말씀해주신 것과 같이 해당 논의들은 구문론적 체계에 대한 논의이며 그냥 단순히 증명인 것이기 때문에 명제의 의미론이나 참/거짓 여부는 고려할 필요 없습니다. 가정에서 원하는 결론만 따라 나오면 문제가 없어요.
자꾸 증명론적 귀결에 의미를 담는데, q iff provq ->p가 아무리 이상하게 생각되어도, 해당 formula형식에 고정점 정리를 이용할 수 있고, 그래서 Tㅏq iff provq->p를 통해 Tㅏp를 유도하는 lob의 정리에서 사용되는 전제에 위배되지 않으면, 고정점정리에 이용되는 어떠한 formula든 그게 어떤 형식으로 표현되든 문제가 없습니다. 형식적으로 타당하기만 하면 되니까요.
증명과정에서 왜 하필 그런 formula를 사용했냐에 대한 논의는 무의미합니다. 왜냐하면 해당 formula는 정리를 증명하기 위한 전제들의 조건에 위배되지 않으니 얼마든지 사용할 수 있고, 그래서 그것을 사용했더니 원하는 결론을 얻었다 이것에 지나지 않기 때문입니다.
lob의 정리는 T가 증명과 관련하여 어떤 특정한 조건을 가진 이론인데, Tㅏprovp->p이면, Tㅏp가 성립한다는 정리 입니다.
prov(x)->p는 wff이며, 따라서 이론 T는 formula x에 대한 대각화 lemma를 적용할 수 있기 때문에, 우리는 함수 f(x)=provx->p에 대해 f(q)=q값을 가지는 대각화 함수를 충분히 구성할 수 있습니다.
그리고 이러한 결과를 이용하여 증명하는 것이 해당 정리의 골자입니다.
f(x)=provx->p형식의 함수가 왜 가능한지, 그리고 f(x)가 왜 고정점 정리를 만족할 수 있는건지는 선행하는 정리들을 이해해야 알 수 있겠구요.
1개의 좋아요
그렇군요 시원한답변 감사합니다. 제가 알고싶었던 부분입니다.
증명가능성이론에 대해서는 아직알아가는 단계입니다만 다른 양상논리체계에서는 증명의 귀결을 받아들일수없어 분석하고 해석하는 논의들이 자연스럽게 있던것을 보았습니다.
반면 증명가능성이론에서는 Q↔(ProvQ→P) 같은것들이 자명한지에 대한 논의가 없는것 같아 이상해서 질문드린 부분이었습니다. 말씀하신바는 잘알겠습니다