Sección (teoría de la prueba)

Una teoría de corte en la prueba es una regla de inferencia que le permite eliminar ("cortar") una declaración intermedia : $A$

{\cfrac {\ \Gamma \ \rightarrow \ \Delta ,\ A\qquad A,\ \Theta \ \rightarrow \ \Lambda \ }{\Gamma ,\ \Theta \ \rightarrow \ \Delta ,\ \ lambda }}

Dado que la regla de la sección no tiene la propiedad de subfórmula (que exige que las premisas estén formadas por subfórmulas de la conclusión), adquieren especial significación los cálculos lógicos con removibilidad de sección (incluso por la posibilidad de probar constructivamente su consistencia ) , es decir, aquellos en los que cualquier el secuente derivable se puede deducir sin secciones. Para el cálculo secuente clásico e intuicionista , la propiedad fue demostrada por Gentzen , posteriormente establecida para una gran serie de teorías clásicas y no clásicas de órdenes superiores.

Literatura

G. Takeuchi. La teoría de la evidencia. - M. : Mir, 1978. - 412 p.
La propiedad de la subfórmula es un artículo de la Enciclopedia de Matemáticas . S. Yu Maslov