cortar la eliminación

Question

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

Answer 1

Supongamos que tengo una prueba de B a partir de la asunción A. Y una prueba de C a partir de la asunción B. a Continuación, el corte de la regla dice que puedo deducir C de la asunción A.

Pero yo no tenía la necesidad de cortar la regla. Si yo era capaz de deducir B de Un yo podría simplemente "inline" la prueba de B a partir de Una directamente en la prueba de C de B para obtener una prueba de C de A.

Por lo que el corte imperio es redundante. Esa es una buena razón para eliminarla.

Pero eliminando viene a un precio. Las pruebas se vuelven más complejas. He aquí un papel que cuantifica cuánto. Así que es una regla estricta para dar.

Answer 2

Cortar la eliminación es indispensable para el estudio de los fragmentos de la aritmética. Consideremos por ejemplo el clásico Parsons–Mentas–Takeuti teorema:

Teorema Si $I\Sigma_1\vdash\forall x\,\exists y\,\phi(x,y)$$\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 va más o menos la siguiente. Formulamos $\Sigma^0_1$-inducción como un secuente regla $$\frac{\Gamma,\phi(x)\longrightarrow\phi(x+1),\Delta}{\Gamma,\phi(0)\longrightarrow\phi(t),\Delta},$$ incluyen los axiomas de P como extra inicial sequents, y aplicar el corte de eliminación para una prueba de que el secuente $\longrightarrow\exists y\,\phi(x,y)$, de modo que el único resto de la corte fórmulas aparecen como principales fórmulas en la inducción de la regla o en algunos axioma de P. Ya que otra de las reglas de la subformula propiedad, todas las fórmulas en la prueba son ahora $\Sigma^0_1$, y podemos demostrar por inducción sobre la longitud de la derivación que cuantificadores existencial en el succedent son (que probablemente se encuentre en PRA) se ha observado una primitiva de la función recursiva dada testigos de cuantificadores existenciales en el antecedente.

Ahora, ¿por qué necesitamos eliminar los recortes de aquí? Porque incluso si el secuente $\phi\longrightarrow\psi$ se compone de fórmulas de baja complejidad (aquí: $\Sigma^0_1$), se podría haber derivado por un corte $$\frac{\phi\longrightarrow\chi\qquad\chi\longrightarrow\psi}{\phi\longrightarrow\psi}$$ donde $\chi$ es una arbitrariamente compleja fórmula y, a continuación, el testimonio argumento por encima de los saltos.

Para dar un ejemplo de un área completamente diferente: corte de eliminación se utiliza a menudo para demostrar decidability de (generalmente proposicional) no clásica de la lógica. Si usted demuestra que la lógica tiene una completa cálculo disfrutando de corte de eliminación y por lo tanto subformula de la propiedad, hay sólo un número finito de posibles sequents que pueden aparecer en una prueba de una fórmula. Uno puede por lo tanto de forma sistemática lista de todos los posibles pruebas, ya sea de la producción de una prueba de la fórmula, o mostrando que es improbable. De nuevo, corte de eliminación es necesaria para tener un límite en la complejidad de las fórmulas que aparecen en la prueba.

Sigfpe escribí más arriba en la respuesta que cortar la eliminación hace pruebas más complejas, pero eso no es realmente cierto: cortar la eliminación hace que las pruebas más largo, pero más elemental, que elimina los conceptos complejos (fórmulas) de la prueba. El último es a menudo útil, y es la principal razón por la que tanto tiempo y energía se dedica a cortar la eliminación en la prueba de la teoría. En la mayoría de las aplicaciones de corte de eliminación no se preocupan realmente por no tener cortes en la prueba, pero trata de tener el control de que las fórmulas pueden aparecer en la prueba.

Answer 3

Para elaborar Alexey la respuesta, por "costumbre" sequent cálculos, las reglas de otros de corte "estructura" en la prueba: el de la izquierda reglas de construir la estructura de la hipótesis de pequeñas fórmulas, y que las normas de derecho de construir la estructura en la conclusión(s). Por lo tanto corte libre de pruebas tienen un tipo de estructura recursiva, y uno puede razonar acerca de la clase de corte libre de pruebas para probar cosas como la coherencia, la integridad, &c.

Sin embargo, el corte libre de las pruebas de no admitir todas las formas usuales tenemos razón en la lógica; modus ponens ser un ejemplo de que las necesidades de corte a ser modelados. Así que para pasar de la clase de inferencias que queremos trabajar dentro de la clase de inferencias en la que mejor podemos razón necesitamos el corte de la eliminación teorema. Si no podemos encontrar un corte de eliminación del teorema, que es una señal de que la "lógica" que está roto.

Answer 4

Otra razón es la prueba de búsqueda. Considere la posibilidad de que una regla como $\frac{\Gamma \vdash p \quad \Gamma \vdash q}{\Gamma \vdash p \wedge q}$ se puede leer como "para encontrar una prueba para $\Gamma \vdash p \wedge q$, es suficiente para encontrar pruebas para$\Gamma \vdash p$$\Gamma \vdash q$". Desde $p$ $q$ son subformulas de $p \wedge q$, la búsqueda de pruebas para ellos es más sencillo.

Para cortar la regla se obtiene "para encontrar una prueba para $\Gamma \vdash p$, es suficiente para encontrar pruebas para $\Gamma \vdash q$ $\Gamma, q \vdash p$ para algunos de fórmula $q$". El problema es, ¿cómo se puede elegir que $q$ a utilizar? No tiene que ser un subformula de $p$ o cualquier fórmula de $\Gamma$. Esto hace que la prueba de búsqueda de solución.