Prueba analítica - Analytic proof

En matemáticas , una prueba analítica es una prueba de un teorema en el análisis que solo hace uso de métodos de análisis y que no usa predominantemente métodos algebraicos o geométricos. El término fue utilizado por primera vez por Bernard Bolzano , quien primero proporcionó una prueba no analítica de su teorema del valor intermedio y luego, varios años más tarde, proporcionó una prueba del teorema que estaba libre de intuiciones sobre las líneas que se cruzan entre sí en un punto, y así se sintió feliz llamándolo analítico (Bolzano 1817).

El trabajo filosófico de Bolzano fomentó una lectura más abstracta de cuándo una demostración podría considerarse analítica, dónde una demostración es analítica si no va más allá de su tema (Sebastik 2007). En la teoría de la prueba , una prueba analítica ha llegado a significar una prueba cuya estructura es simple de una manera especial, debido a condiciones sobre el tipo de inferencias que aseguran que ninguna de ellas vaya más allá de lo que está contenido en los supuestos y lo que se demuestra.

Teoría de la prueba estructural

En la teoría de la prueba, la noción de prueba analítica proporciona el concepto fundamental que resalta las similitudes entre una serie de cálculos de prueba esencialmente distintos , definiendo así el subcampo de la teoría de la prueba estructural . No existe una definición general indiscutible de prueba analítica, pero para varios cálculos de prueba hay una noción aceptada. Por ejemplo:

• En el cálculo de deducción natural de Gerhard Gentzen , las pruebas analíticas son las que están en forma normal; es decir, ninguna ocurrencia de fórmula es tanto la premisa principal de una regla de eliminación como la conclusión de una regla de introducción;
• En el cálculo posterior de Gentzen, las pruebas analíticas son aquellas que no utilizan la regla de corte .

Sin embargo, es posible extender las reglas de inferencia de ambos cálculos para que existan pruebas que satisfagan la condición pero no sean analíticas. Por ejemplo, un ejemplo particularmente complicado de esto es la regla de corte analítica , ampliamente utilizada en el método de tableau , que es un caso especial de la regla de corte donde la fórmula de corte es una subfórmula de fórmulas laterales de la regla de corte: una prueba que contiene un corte analítico es, en virtud de esa regla, no analítico.

Además, las teorías de prueba estructural que no son análogas a las teorías de Gentzen tienen otras nociones de prueba analítica. Por ejemplo, el cálculo de estructuras organiza sus reglas de inferencia en pares, llamados fragmento hacia arriba y fragmento hacia abajo, y una prueba analítica es aquella que solo contiene el fragmento hacia abajo.

Ver también

• Semántica de la teoría de la prueba

Referencias

• Bernard Bolzano (1817). Demostración puramente analítica del teorema de que entre dos valores cualesquiera que den resultados de signo opuesto, se encuentra al menos una raíz real de la ecuación. En Abhandlungen der koniglichen bohmischen Gesellschaft der Wissenschaften vol. V, págs. 225-48.
• Pfenning (1984). Pruebas analíticas y no analíticas. En Proc. VII Congreso Internacional de Deducción Automatizada .
• Sebastik (2007). La lógica de Bolzano . Entrada en la Enciclopedia de Filosofía de Stanford .