Removibilidad de secciones

La removibilidad de las secciones ( teorema de Gentzen, teorema de eliminación ) es una propiedad de los cálculos lógicos, según la cual cualquier secuente deducible en un cálculo dado puede deducirse sin aplicar la regla de la sección [1] . Desempeña un papel fundamental en la teoría de la demostración y un papel metodológico importante en la lógica matemática en general debido a que proporciona un método constructivo para probar la consistencia , en particular, para la lógica clásica e intuicionista de primer orden [2] .

Para los cálculos secuentes clásicos e intuicionistas , la propiedad fue demostrada por Gentzen en 1934 . En 1953 se planteó la conjetura de Takeuchi , según la cual la removibilidad de las secciones tiene lugar para la teoría simple de tipos y las lógicas de orden superior correspondientes a ella, posteriormente se confirmó -para la lógica clásica de segundo orden, la removibilidad de las secciones fueron probadas por Tate , para la teoría simple de tipos - Takahashi y Pravitsa , pronto se encontraron pruebas para una serie de teorías de orden superior no clásicas ( Dragalin ) y teorías de tipos avanzadas ( Girard para el sistema F ).

Formulación simbólica: sean y  sean secuentes demostrables del cálculo ; si  es un cálculo secuente , entonces es demostrable [3] .

Notas

  1. ↑ Teoría de la prueba, 1978 , p. 29
  2. ↑ P. I. Bystrov. Teorema de eliminación  // Nueva Enciclopedia Filosófica  : en 4 volúmenes  / anterior. ed. científica consejo de V. S. Stepin . — 2ª ed., corregida. y adicional - M.  : Pensamiento , 2010. - 2816 p.
  3. ↑ Ershov, 1987 , pág. 214.

Literatura