Prueba enfocada

Según las reglas del cálculo de secuentes, las fórmulas se clasifican canónicamente en dos clases llamadas positivas y negativas , por ejemplo, en LK y LJ la fórmula${\displaystyle \phi \lor \psi }$es positivo. La única libertad reside en los átomos, a los que se les asigna una polaridad libremente. Para fórmulas negativas, la demostrabilidad es invariante bajo la aplicación de una regla de la derecha; y, de forma dual, para fórmulas positivas, la demostrabilidad es invariante bajo la aplicación de una regla de la izquierda. En ambos casos, se pueden aplicar reglas con seguridad en cualquier orden a subfórmulas hereditarias de la misma polaridad.

En el caso de una regla de la derecha aplicada a una fórmula positiva, o una regla de la izquierda aplicada a una fórmula negativa, se pueden obtener secuencias inválidas, por ejemplo, en LK y LJ no hay prueba de la secuencia.${\displaystyle B\lor A\vdash A\lor B}$Comenzando con una regla correcta. Un cálculo admite el principio de enfoque si, cuando un reducto original es demostrable, entonces los reductos hereditarios de la misma polaridad también lo son. Es decir, uno puede comprometerse a enfocarse en la descomposición de una fórmula y sus subfórmulas de la misma polaridad sin perder completitud.

A menudo se demuestra que un cálculo secuencial posee la propiedad de enfoque al trabajar con un cálculo relacionado donde la polaridad controla explícitamente qué reglas se aplican. Las demostraciones en tales sistemas se encuentran en fases enfocadas, no enfocadas o neutras, donde las dos primeras se caracterizan por la descomposición hereditaria; y la última por forzar la elección del enfoque. Uno de los comportamientos operacionales más importantes que puede experimentar un procedimiento es el retroceso , es decir, volver a una etapa anterior del cálculo donde se realizó una elección. En sistemas enfocados para la lógica clásica e intuicionista, el uso del retroceso puede simularse mediante la pseudocontracción.

Dejar${\displaystyle \uparrow }$y${\displaystyle \downarrow }$denotan cambio de polaridad, el primero hace que una fórmula sea negativa y el segundo positiva; y llama neutral a una fórmula con una flecha. Recuerda que${\displaystyle \lor }$es positivo, y considere la secuencia polarizada neutra${\displaystyle {\downarrow \uparrow \phi \lor \psi }\vdash {\uparrow \phi \lor \psi }}$, que se interpreta como la secuencia real${\displaystyle \phi \lor \psi \vdash \phi \lor \psi }$Para secuencias neutras como esta, el sistema enfocado obliga a elegir explícitamente en qué fórmula centrarse, denotada por${\displaystyle \langle \,\rangle }$Para realizar una búsqueda de pruebas, lo mejor es elegir la fórmula de la izquierda, ya que${\displaystyle \lor }$es positivo, de hecho (como se discutió anteriormente) en algunos casos no hay demostraciones donde el enfoque esté en la fórmula correcta. Para superar esto, algunos cálculos enfocados crean un punto de retroceso tal que enfocarse en la correcta produce${\displaystyle \downarrow \uparrow \phi \lor \psi \vdash \langle \phi \lor \psi \rangle ,\uparrow \phi \lor \psi }$, que sigue siendo como${\displaystyle \phi \lor \psi \vdash \phi \lor \psi }$. La segunda fórmula de la derecha solo se puede eliminar cuando la fase enfocada haya terminado, pero si la búsqueda de pruebas se bloquea antes de que esto suceda, el secuente puede eliminar el componente enfocado, volviendo así a la elección, por ejemplo,${\displaystyle \downarrow \uparrow B\lor A\vdash \langle A\rangle ,\uparrow A\lor B}$ debe ser llevado a${\displaystyle \downarrow \uparrow B\lor A\vdash {\uparrow A\lor B}}$ya que no se puede realizar ninguna otra inferencia reductiva. Se trata de una pseudocontracción, puesto que tiene la forma sintáctica de una contracción a la derecha, pero la fórmula real no existe; es decir, en la interpretación de la prueba en el sistema enfocado, el secuente tiene solo una fórmula a la derecha.