직관 논리의 불가항력
나는 여기저기서 직관적 인 논리 안에서 셀 수없는 것이 자연의 부분 집합이 될 수 있다는 스 니펫을 읽었다 .
- 이것에 대해 생각하는 올바른 직감은 무엇입니까? Andrej Bauer는 위에서 다음과 같이 대답했습니다.
어떤 순서 주장 열거 감안할 때
e : Integer -> (Integer -> Bool),e순서를 놓칠 것이다contra i = not (e i i). 따라서 Haskell에서 유형을 열거 할 수 없습니다.
나는이 주장을 이해하지만, 그것에 대해 불편하다. "모델 내부"와 "모델 외부"를 언제 생각해야할지 모르겠습니다. 이것은 모델 내부의 것들이 그들이 원하는대로 어리석은 사실로 믿을 수 있다는 것을 의미하는 것 같습니다 powerset(X) = X. '내부'와 '외부'의 차이에 대해 어떻게 생각해야합니까?
- 나는 여기저기서 직관 론적 논리 (ZFC와 관련된)의 이상함에 대한 단편적인 언급을 집어 들었다. 나는 이러한 결과를 질서 정연한 방식으로 배치하는 교과서를 모른다. 교과서 추천 좀 주 시겠어요?
답변
나는 당신이 " 건설 수학을 받아들이는 다섯 단계 "에서 제기하는 질문에 답하려고 노력했습니다 .
다음은 몇 가지 교과서입니다.
- D. Bridges와 E. Bishop의 건설적 분석 은 건설 수학의 "성경"입니다.
- 건설 수학의 품종 D. 교량 및 F. 리치맨에 의해 건설적인 수학의 여러 종류를 고려, 그들이 가지고있는 병리와 미묘한 중 일부에 대해 설명합니다.
- D. van Dalen과 A. Troelstra의 수학 구성주의 (1 권 및 2 권) 는 구성 수학에 대한 심층적 인 처리를 제공합니다.
Haskell 및 유형에 관한 질문에 대해 (쉽게 번역 할 수있는) 답변을 드릴 수는 없지만 ZFC를 이미 언급 했으므로 다음 내용이 도움이 될 수 있습니다.
ZFC의 공리를 취하고 ZFC가 일관 적이라고 가정합시다. Löwenheim-Skolem Theorem Downwards (First-Order Predicate Logic에 대한 완전성 정리의 추론으로) 모델이 있습니다.$\mathfrak{M}$계산할 수있는 ZFC (ZFC는 단일 비논리적 기호로 공식화 됨). 따라서 외부 에서이 모델 을 들여다 보면 셀 수 있음을 쉽게 알 수 있습니다. 그러나이 모델 내에서 작업 할 때는 여전히$\omega$ 그리고 당신은 여전히 $\mathfrak{M} \models (\omega, 0^\omega, S^\omega) \models^\mathfrak{M} PA$, 그래서 $\mathfrak{M}$ 증명하다 $\omega$적절한 상수 및 적절한 함수와 함께 Peano Axioms의 모델이 있습니다. 또한 다음과 같은 정리가 있습니다.$\mathfrak{M} \models |P(\omega)| > |\omega|$, 원하는만큼 반복되었으므로 $\mathfrak{M}$여전히 더 많은 세트가 있음을 알고 있습니다 ( 외부 에서 볼 수 있지만 실제로는$|\omega^\mathfrak{M}| = |\mathfrak{M}|$). 과$\mathfrak{M}$않습니다 모른다 는 어떤을 놓친$w \subset \omega$.
이것을 쉽게 이해하기 위해 다음 게임을 고려하십시오. 나는 당신에게 자연수 세트를 주도록 도전하고 이전 에이 세트에 대해 생각했다면 솔직히 대답 할 것입니다. 내가 생각하지 않은 세트를 찾으면 승리합니다. 제 승리 전략은 다음과 같습니다. 우리 언어로 설명 할 수있는 모든 세트에 대해 생각합니다. 언어의 카디널리티는 셀 수 있기 때문에 이것으로 설명 할 수있는 세트는 상당히 많을뿐입니다. 그래서 여러분은 제가 생각하지 않았던 세트를 생각 해낼 수 없을 것입니다. 그리고 여러분과 저는 제가 모든 세트의 0 %에 대해 생각했다는 것을 압니다 (여기에 측정 이론을 적용하는 정도입니다).
그것은 당신이 언급 한 두 번째 것에 관한 한 가지 변칙입니다.
ZFC에서 세트가 항상 거듭 제곱 세트보다 작다는 것을 증명할 수 있으므로 (ZFC가 일관된 것에 의존하는) 모델은 $X = P(X)$. 그러나 이상한 모델이 있습니다. Gödel의 첫 번째 불완전 성 정리에 따르면 ZFC가 일관성이 있으면$ZFC \not \models Con(ZFC)$ 더 나쁜 경우에는 $ZFC + \neg Con(ZFC) \not \models \bot$, 즉 ZFC와 일관성이 없다는 가정에도 모델이 있습니다.
이러한 모델은 원하는만큼 이상하게 성장할 수 있습니다. 이 경우에 당신이하고 싶은 것은 당신이 외부에서 알고있는 자연수에 대해 어떤 문장에 대해 증명하는 속성을 가진 모델 / 이론을보고 싶어하는 것입니다.
MathOverflow에 대한 이러한 주제와 관련된 많은 질문과 토론이 있습니다. 예를 들면 다음과 같습니다. https://mathoverflow.net/questions/77628/question-about-godels-2nd-theorem