타케우티의 추측
Takeuti's conjecture수학에서 타케우티의 추측은 2차 논리학의 순차적 공식화가 절연성을 가지고 있다는 가이시 타케우티의 추측이다(타케우티 1953).그것은 긍정적으로 해결되었다.
- 바이 타이트(By Tait)는 슈트(Tait 1966)의 작업에 기반하여 컷 엘리미네이션(cut-rimination)을 입증하기 위한 의미 기법을 사용한다.
- Prawitz (Prawitz 1968년)와 타카하시 (Takahashi 1967년)에 의해 독립적으로 - Prawitz와 타카하시의 증명들은 2차 논리에 국한되지 않지만, 일반적으로 고차원의 로직은 우려된다.
- 그것은 시스템 F의 강력한 정상화에 대한 장-이브 지라드의 통사적 증거의 귀결이다.
타케우티의 추측은 약한 시스템 PRA에서 각각의 진술이 서로에게서 도출될 수 있다는 점에서 2차 산술의 일관성과 동등하다. 일관성은 여기서 2차 산술에 대한 괴델 문장의 진리를 가리킨다.또한 Girard/Reynold의 System F의 강력한 정상화에 해당한다.
참고 항목
참조
- 다그 프라위츠, 1968년Hauptsatz는 고차 논리학이다.J. 심브.로그, 1968년 33:452–457
- 윌리엄 W. 1966년 태트젠첸의 하우프트사츠가 두번째 순서 서술적 논리에 대한 비건설적 증거.미국수학협회 회보에서는 72:980–983.
- 게이시 다케우티, 1953년일반화된 논리 미적분학에서.일본 수학 저널에서 23:39–96.이 기사의 오류는 같은 저널인 1954년 24:149–156에 발표되었다.
- 다카하시 모토오 1967년단순 유형 이론에서 절삭의 증거.일본수학회는 10:44–45.
