La conjetura de Takeuti

En matemáticas , la conjetura de Takeuti es la conjetura de Gaisi Takeuti de que una formalización de secuencias de la lógica de segundo orden tiene eliminación de cortes (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);
• De forma independiente por Prawitz (Prawitz 1968) y Takahashi 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 lógicas de orden superior en general;
• Es un corolario de la prueba sintáctica de Jean-Yves Girard de la normalización fuerte para el Sistema F.

La conjetura de Takeuti es equivalente a la 1-consistencia de la aritmética de segundo orden en el sentido de que cada una de las afirmaciones puede derivarse de las demás en el sistema débil de aritmética recursiva primitiva (PRA) . También es equivalente a la normalización fuerte del sistema F de Girard/Reynolds .

• El segundo problema de Hilbert

• Dag Prawitz , 1968. Hauptsatz para lógica de orden superior. Journal of Symbolic Logic , 33:452–457, 1968.
• William W. Tait , 1966. Una demostración 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 . Una fe de erratas de este artículo fue publicada en la misma revista, 24:149-156 , 1954.
• Moto-o Takahashi, 1967. Una demostración de eliminación de cortes en la teoría de tipos simple. En Sociedad Matemática Japonesa , 10:44 – 45.