En matemáticas , la conjetura de Takeuti es la conjetura de Gaisi Takeuti que una formalización Sist de lógica de segundo orden tiene corte de eliminación (Takeuti 1953). Se resolvió positivamente:
- Por Tait, utilizando una técnica semántica para probar la eliminación de cortes, basada en el trabajo de Schütte (Tait 1966);
- Independientemente de Prawitz (Prawitz 1968) y Takahashi (Takahashi 1967) mediante una técnica similar (Takahashi 1967), aunque las demostraciones de Prawitz y Takahashi no se limitan a la lógica de segundo orden, sino que se refieren a la lógica de orden superior en general;
- Es un corolario de Jean-Yves Girard prueba sintáctica 's de una fuerte normalización de System F .
La conjetura de Takeuti es equivalente a la consistencia de la aritmética de segundo orden en el sentido de que cada uno de los enunciados puede derivarse entre sí en el sistema débil PRA ; la consistencia se refiere aquí a la verdad de la oración de Gödel para la aritmética de segundo orden. También es equivalente a la fuerte normalización del Sistema F de Girard / Reynold .
Ver también
Referencias
- Dag Prawitz , 1968. Hauptsatz para lógica de orden superior. J. Symb. Log., 33: 452–457, 1968.
- William W. Tait , 1966. Una prueba no constructiva del Hauptsatz de Gentzen para la lógica de predicados de segundo orden. En Bulletin of the American Mathematical Society , 72: 980–983.
- Gaisi Takeuti , 1953. Sobre un cálculo lógico generalizado. En Japanese Journal of Mathematics , 23: 39–96. Se publicó una errata de este artículo en la misma revista, 24: 149-156, 1954.
- Moto-o Takahashi, 1967. Una prueba de eliminación de cortes en la teoría de tipos simples. En Japanese Mathematical Society , 10: 44–45.