Prueba analítica

En matemáticas , una prueba analítica es una prueba de un teorema en análisis que solo hace uso de métodos de análisis, y que no hace uso predominante de 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 después, proporcionó una prueba del teorema que estaba libre de intuiciones sobre líneas que se cruzan entre sí en un punto, por lo que se sintió feliz de llamarlo analítico (Bolzano 1817).

El trabajo filosófico de Bolzano alentó una lectura más abstracta de cuándo una demostración podría considerarse analítica, donde una prueba 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 las 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.

En la teoría de la prueba, la noción de prueba analítica proporciona el concepto fundamental que pone de manifiesto las similitudes entre varios 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 existe una noción aceptada. Por ejemplo:

• En el cálculo de deducción natural de Gerhard Gentzen , las pruebas analíticas son aquellas en forma normal; es decir, ninguna ocurrencia de fórmula es a la vez la premisa principal de una regla de eliminación y la conclusión de una regla de introducción;
• En el cálculo secuencial 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 de modo que existan pruebas que satisfagan la condición pero que no sean analíticas. Por ejemplo, un ejemplo particularmente complicado de esto es la regla de corte analítica , utilizada ampliamente en el método de tabla , que es un caso especial de la regla de corte donde la fórmula de corte es una subfórmula de fórmulas secundarias de la regla de corte: una prueba que contiene un corte analítico no es analítica en virtud de esa regla.

Además, los cálculos de demostración que no son análogos a los cálculos de Gentzen tienen otras nociones de demostración analítica. Por ejemplo, el cálculo de estructuras organiza sus reglas de inferencia en pares, llamados fragmento de arriba y fragmento de abajo, y una demostración analítica es aquella que sólo contiene el fragmento de abajo.

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

• Bernard Bolzano (1817). Demostración puramente analítica del teorema de que entre dos valores cualesquiera que den resultados de signo opuesto, hay al menos una raíz real de la ecuación. En Abhandlungen der koniglichen bohmischen Gesellschaft der Wissenschaften Vol. V, pp.225-48.
• Frank Pfenning (1984). Pruebas analíticas y no analíticas. En Proc. 7th International Conference on Automated Deduction .
• Jan Šebestik (2007). La lógica de Bolzano. Entrada en la Stanford Encyclopedia of Philosophy .