eliminación de cortes

Question

¿Qué es la regla de corte? No me refiero a la regla en sí, sino a una explicación de lo que significa y por qué los teóricos de la prueba siempre intentan eliminarla. ¿Por qué un sistema sin corte es más especial que uno con corte?

Answer 1

Supongamos que tengo una prueba de B partiendo de la suposición A. Y una prueba de C partiendo de la suposición B. Entonces la regla de corte dice que puedo deducir C de la suposición A.

Pero no necesitaba la regla del corte. Si era capaz de deducir B a partir de A, podía simplemente "alinear" la prueba de B a partir de A directamente en la prueba de C a partir de B para obtener una prueba de C a partir de A.

Así que la regla del corte es redundante. Es una buena razón para eliminarla.

Pero eliminarlo tiene un precio. Las pruebas se vuelven más complejas. He aquí una papel que cuantifique cuánto. Así que es una regla difícil de abandonar.

Answer 2

La eliminación de cortes es indispensable para estudiar fragmentos de aritmética. Consideremos, por ejemplo, el teorema clásico de Parsons-Mints-Takeuti:

Teorema Si $I\Sigma_1\vdash\forall x\,\exists y\,\phi(x,y)$ con $\phi\in\Sigma^0_1$ entonces existe una función recursiva primitiva $f$ tal que $\mathrm{PRA}\vdash\forall x\,\phi(x,f(x))$ .

La prueba es aproximadamente la siguiente. Formulamos $\Sigma^0_1$ -inducción como regla secuencial $$\frac{\Gamma,\phi(x)\longrightarrow\phi(x+1),\Delta}{\Gamma,\phi(0)\longrightarrow\phi(t),\Delta},$$ incluir axiomas de Q como secuentes iniciales adicionales, y aplicar la eliminación de cortes a una prueba del secuente $\longrightarrow\exists y\,\phi(x,y)$ de modo que las únicas fórmulas de corte restantes aparezcan como fórmulas principales en la regla de inducción o en algún axioma de Q. Puesto que otras reglas tienen la propiedad de subfórmula, todos fórmulas de la prueba son ahora $\Sigma^0_1$ y podemos demostrar por inducción sobre la longitud de la derivación que los cuantificadores existenciales en el sucesor son (demostrablemente en PRA) atestiguados por una función recursiva primitiva dados los testigos de los cuantificadores existenciales en el antecedente.

Ahora, ¿por qué necesitamos eliminar recortes aquí? Porque incluso si el secuencial $\phi\longrightarrow\psi$ consiste en fórmulas de baja complejidad (aquí: $\Sigma^0_1$ ), podríamos haberlo derivado mediante un corte $$\frac{\phi\longrightarrow\chi\qquad\chi\longrightarrow\psi}{\phi\longrightarrow\psi}$$ donde $\chi$ es una fórmula arbitrariamente compleja, y entonces se rompe el argumento testimonial anterior.

Por poner un ejemplo de un ámbito completamente distinto: la eliminación de cortes se utiliza a menudo para demostrar la decidibilidad de lógicas no clásicas (normalmente proposicionales). Si se demuestra que la lógica tiene un cálculo completo que disfruta de la eliminación de cortes y, por tanto, de la propiedad de subfórmulas, sólo hay un número finito de secuencias posibles que puedan aparecer en la demostración de una fórmula dada. De este modo, se pueden enumerar sistemáticamente todas las pruebas posibles, ya sea produciendo una prueba de la fórmula o mostrando que es indemostrable. Una vez más, la eliminación de cortes es necesaria aquí para tener un límite en la complejidad de las fórmulas que aparecen en la prueba.

Sigfpe escribió arriba en su respuesta que la eliminación de cortes hace que las pruebas sean más complejas, pero en realidad eso no es cierto: la eliminación de cortes hace que las pruebas sean más largo pero más elemental elimina los conceptos complejos (fórmulas) de la prueba. Esto último suele ser útil, y es la razón principal por la que se dedica tanto tiempo y energía a la eliminación de cortes en la teoría de la demostración. En la mayoría de las aplicaciones de la eliminación de cortes, a uno no le importa realmente que no haya cortes en la demostración, sino controlar qué fórmulas pueden aparecer en la demostración.

Answer 3

Otra razón es la búsqueda de pruebas. Considere que una regla como $\frac{\Gamma \vdash p \quad \Gamma \vdash q}{\Gamma \vdash p \wedge q}$ puede leerse como "encontrar una prueba para $\Gamma \vdash p \wedge q$ basta con encontrar pruebas para $\Gamma \vdash p$ et $\Gamma \vdash q$ ". Desde $p$ et $q$ son subfórmulas de $p \wedge q$ encontrar pruebas para ellos es más sencillo.

Para la regla de corte se obtiene "encontrar una prueba para $\Gamma \vdash p$ basta con encontrar pruebas para $\Gamma \vdash q$ et $\Gamma, q \vdash p$ para alguna fórmula $q$ ". El problema es cómo elegir qué $q$ usar? No tiene por qué ser una subfórmula de $p$ o cualquier fórmula de $\Gamma$ . Esto hace que la búsqueda de pruebas sea intratable.

Answer 4

Para profundizar en la respuesta de Alexey, para los cálculos secuenciales "habituales", las reglas distintas del corte "construyen estructura" en la prueba: las reglas de la izquierda construyen estructura de las suposiciones a partir de fórmulas más pequeñas, y las reglas de la derecha construyen estructura en la(s) conclusión(es). Así, las pruebas sin corte tienen una especie de estructura recursiva, y se puede razonar sobre la clase de pruebas sin corte para demostrar cosas como la consistencia, la completitud, etc.

Sin embargo, las pruebas sin corte no admiten todas las formas habituales en que razonamos en lógica; el modus ponens es un ejemplo que necesita corte para ser modelado. Así que para pasar de la clase de inferencias en la que queremos trabajar a la clase de inferencias en la que podemos razonar mejor, necesitamos el teorema de eliminación de cortes. Si no podemos encontrar un teorema de eliminación de cortes, es señal de que la "lógica" está rota.