한편으로 고델의 제 2 차 불완전 성 정리는 기본적인 산술 진술을 표현하기에 충분히 강력한 일관성있는 형식 이론은 그 자체의 일관성을 증명할 수 없다고 말합니다. 반면에, 교회-로저의 공식 (재 작성) 시스템 속성은 모든 방정식이 도출 될 수있는 것은 아니라는 점에서 일관성이 있음을 알려줍니다 (예 : K).
≠나는 그것들이 같은 일반적인 형태를 갖지 않기 때문에.
그런 다음 CIC (Culculus of Inductive Constructions)는 두 조건을 명확하게 안정화시킵니다. 산술 제안을 표현하기에 충분히 강력합니다 (실제로 -calculus만으로도 이미 교회 숫자를 인코딩하고 모든 기본 재귀 함수를 나타낼 수 있음). 또한 CIC는 합류 또는 교회-로저 속성도 가지고 있습니다. 그러나:
λβηCIC가 2 차 불완전 성 정리에 의해 자체 일관성을 입증 할 수 없어야 하는가?
아니면 CIC가 시스템 내에서 자체 일관성을 증명할 수 없다고 말하고 합류 속성이 메타 정리라는 것입니까? 아니면 CIC의 합류 속성이 일관성을 보장하지 않습니까?
누군가 그 문제에 대해 밝힐 수 있다면 대단히 감사하겠습니다!
감사!
답변
먼저, 당신은 방정식 이론 으로서의 CIC의 일관성과 논리 이론으로서의 CIC의 일관성을 혼동하고 있습니다 . 첫 번째는 CIC의 모든 용어 (동일한 유형)가
βη-동등한. 두 번째는 유형이
⊥거주하지 않습니다. CR은 두 번째가 아닌 첫 번째 종류의 일관성을 의미합니다. 의견에서 지적했듯이 이것은 대신 (약한) 정규화에 의해 암시됩니다. 이 상황의 프로토 타입 예제는 순수합니다.
λ-미적분 : 그것은 방정식 적으로 일관성이 있지만 (CR 보유) 논리 시스템 (알론조 교회 또는 원래 의도 된대로)으로 간주하면 일관성이 없습니다 (실제로 정상화되지는 않습니다).
둘째, Emil이 지적했듯이 CIC에 특정 속성 (CR 또는 정규화)이 있더라도 CIC 자체가 해당 속성을 증명할 수는 없습니다. 이 경우 CIC가 자체 CR 속성을 입증 할 수 있다는 사실에 불일치가 보이지 않으며 실제로는 이것이 사실이라고 생각합니다 (기본 조합 인수는 일반적으로 CR에 충분하며 이러한 인수는 분명히 거대한 범위에 속합니다 CIC의 논리적 힘). 그러나 CIC는 확실히 두 번째 불완전 성 정리로 인해 자체 정규화 속성을 입증하지 못합니다.