이 질문은 mathoverflow에서 응용 수학에 대한 비슷한 질문에서 영감을 얻었으며 P 대 NP와 같은 TCS의 중요한 질문은 ZFC (또는 다른 시스템)와 무관하다고 생각합니다. 작은 배경으로 역 수학 은 중요한 이론을 증명하는 데 필요한 공리를 찾는 프로젝트입니다. 다시 말해, 우리는 사실이 될 것으로 기대되는 일련의 정리에서 시작하여이를 가능하게하는 최소한의 ‘자연’공리를 도출하려고 시도합니다.
역 수학 접근법이 TCS의 중요한 이론에 적용되었는지 궁금합니다. 특히 복잡성 이론. TCS의 많은 공개 질문에 대한 교착 상태로 인해 “어떤 공리를 사용해 보지 않았습니까?” 또는 TCS의 중요한 질문이 2 차 산술의 특정 하위 시스템과 무관 한 것으로 나타 났습니까?
답변
예, 주제는 증명 복잡성에 대해 연구되었습니다. 이것을 Bounded Reverse Mathematics 라고 합니다. Cook과 Nguyen의 저서 ” 논리적 복잡성 증명 복잡성 “, 2010 년 8 페이지에서 일부 역 수학 결과를 포함하는 표를 찾을 수 있습니다 . Steve Cook의 이전 학생들 중 일부는 Nguyen의 논문, ” Bounded Reverse Mathematics ” 와 같은 유사한 주제에 대해 작업했습니다. , 토론토 대학교, 2008.
Alexander Razborov (또한 다른 증명 복잡도 이론가)는 회로 복잡도 기법을 공식화하고 회로 복잡도 하한을 증명하는 데 필요한 약한 이론에 대한 결과를 가지고 있습니다. 그는 약한 이론에 대한 몇 가지 비현실적인 결과를 얻었지만 이론은 너무 약한 것으로 간주됩니다.
답변
최종 질문에 대한 긍정적 인 답변으로, 건축 미적분학과 같은 다형성 람다 미적분학의 정규화 증명에는 적어도 고차 산술이 필요하며, 더 강력한 시스템 (유도 적 건축의 미적분학)은 ZFC와 거의 일치하지 않는 수많은 시스템과 일치합니다.
더 철학적으로 일관성 강도를 추상화의 강도와 동일시하는 실수를하지 마십시오.
주제를 구성하는 올바른 방법은 일관성 강도 측면에서 엄격하게 필요하지는 않지만 명백하게 거친 이론 이론을 포함 할 수 있습니다. 예를 들어, 강력한 수집 원칙은 균일 성 속성을 나타내는 데 매우 유용합니다. 예를 들어, 범주 이론가들은 모든 그룹의 범주와 같은 사물을 마치 사물처럼 조작하기 위해 약한 큰 기본 공리를 원하게됩니다. 가장 유명한 예는 대수 기하학이며, 그 개발로 Grothendieck 우주를 광범위하게 사용하지만 Fermat의 Last Theorem과 같은 모든 응용 프로그램은 분명히 3 차 산술 내에 있습니다. 훨씬 더 간단한 예로, 일반 아이덴티티 및 컴포지션 작업은 전체 세트 유니버스에 걸쳐 인덱스되므로 기능이 아닙니다.
편집 : A의 일관성이 B의 일관성을 의미하는 경우 논리 시스템 A는 시스템 B보다 일관성 강도가 더 높습니다. 예를 들어 ZFC에서 PA의 일관성을 증명할 수 있기 때문에 ZFC는 Peano 산술보다 일관성 강도가 더 큽니다. A와 B가 동일하면 일관성 강도가 동일합니다. 예를 들어, Peano 산술은 Heyting (건설적) 산술 인 경우에만 일관됩니다.
논리에 대한 가장 놀라운 사실 중 하나 인 IMO는 일관성 강도가 “이 논리에서 총체적으로 증명할 수있는 가장 빠르게 성장하는 기능은 무엇입니까?”라는 질문으로 귀결된다는 것입니다. 결과적으로 많은 종류의 논리의 일관성을 선형 적으로 정렬 할 수 있습니다! 가장 빠르게 성장하는 기능을 설명 할 수있는 서수 표기법이있는 경우 두 논리에 총계가 표시 될 수 있으며, 하나는 다른 논리의 일관성을 증명할 수 있거나 동등 함을 삼분 절로 알 수 있습니다.
그러나이 놀라운 사실은 일관성 강도가 수학 추상화에 대해 이야기하기에 적합한 도구가 아닌 이유이기도합니다. 코딩 트릭을 포함하여 시스템의 변형이 아니며 좋은 추상화를 사용하면 트릭 없이 아이디어를 표현할 수 있습니다 . 그러나 우리는이 아이디어를 공식적으로 표현할 논리에 대해 충분히 알지 못합니다.