sistema de fregue

En la complejidad de la prueba , un sistema de Frege es un sistema de prueba proposicional cuyas pruebas son secuencias de fórmulas derivadas utilizando un conjunto finito de reglas de inferencia sólidas e implicativamente completas . Los sistemas de Frege (más conocidos como sistemas de Hilbert en la teoría de la prueba general ) llevan el nombre de Gottlob Frege .

Definicion formal

Sea K un conjunto finito funcionalmente completo de conectivos booleanos y considere fórmulas proposicionales construidas a partir de variables p ₀ , p ₁ , p ₂ , ... usando K -conectivos. Una regla de Frege es una regla de inferencia de la forma

${\displaystyle r={\frac {B_{1},\dots ,B_{n}}{B}},}$

donde B ₁ , ..., B _n , B son fórmulas. Si R es un conjunto finito de reglas de Frege, entonces F = ( K , R ) define un sistema de derivación de la siguiente manera. Si X es un conjunto de fórmulas y A es una fórmula, entonces una derivación F de A a partir _de los axiomas X es una secuencia de fórmulas A ₁ , ..., Am tal que _Am =  A  , y cada A _k es un miembro de X , o se deriva de algunas de las fórmulas Ai _, i  <  k , mediante una instancia de sustitución de una regla de R. Una prueba F de una fórmula A es una derivación F de A a partir del conjunto vacío de axiomas (X=∅). F se llama sistema de Frege si

• F es sólida: toda fórmula demostrable por F es una tautología.
• F es implícitamente completo: para cada fórmula A y un conjunto de fórmulas X , si X implica A , entonces hay una F -derivación de A a partir de X.

La longitud (número de líneas) en una prueba A ₁ , ..., Am es _m . El tamaño de la prueba es el número total de símbolos.

Un sistema de derivación F como el anterior es refutacionalmente completo, si para cada conjunto inconsistente de fórmulas X , hay una derivación F de una contradicción fija de X.

Ejemplos

• El cálculo proposicional de Frege es un sistema de Frege.
• Hay muchos ejemplos de reglas sólidas de Frege en la página de Cálculo proposicional .
• La resolución no es un sistema de Frege porque sólo opera sobre cláusulas , no sobre fórmulas construidas de manera arbitraria por un conjunto funcionalmente completo de conectivos. Además, no es implícitamente completo, es decir, no podemos concluir a partir de . Sin embargo, agregar la regla de debilitamiento : lo hace implícitamente completo ^{[ cita necesaria ]} . La resolución también es refutablemente completa. ${\displaystyle A\lor B}$ ${\displaystyle A}$ ${\displaystyle {\frac {A}{A\lor B}}}$

Propiedades

• El teorema de Reckhow (1979) establece que todos los sistemas de Frege son p-equivalentes .
• La deducción natural y el cálculo secuencial (sistema Gentzen con corte) también son p-equivalentes a los sistemas de Frege.
• Hay pruebas de Frege de tamaño polinomial del principio del casillero (Buss 1987).
• Los sistemas de Frege se consideran sistemas bastante fuertes. A diferencia de, digamos, la resolución, no se conocen límites inferiores superlineales para el número de líneas en las pruebas de Frege, y los límites inferiores más conocidos para el tamaño de las pruebas son cuadráticos.
• El número mínimo de rondas en el juego probador-adversario necesario para demostrar una tautología es proporcional al logaritmo del número mínimo de pasos en una prueba de Frege de . ${\displaystyle \phi }$ ${\displaystyle \phi }$

• 
  Pruebas de fortalezas de diferentes sistemas.

Sistema Frege extendido

Una extensión importante de un sistema de Frege, el llamado Frege extendido , se define tomando un sistema de Frege F y agregando una regla de derivación adicional que permite derivar la fórmula , donde se abrevia su definición en el lenguaje del F particular y el átomo no. ocurren en fórmulas derivadas previamente, incluidos axiomas y en la fórmula . ${\displaystyle p\leftrightarrow D}$ ${\displaystyle \leftrightarrow }$ ${\displaystyle p}$ ${\displaystyle D}$

El objetivo de la nueva regla de derivación es introducir 'nombres' o atajos para fórmulas arbitrarias. Permite interpretar pruebas en Frege Extendido como pruebas de Frege operando con circuitos en lugar de fórmulas.

La correspondencia de Cook permite interpretar el Frege extendido como un equivalente no uniforme de la teoría PV de Cook y la teoría de Buss que formaliza el razonamiento factible (en tiempo polinómico). ${\displaystyle S_{2}^{1}}$

Referencias

• Krajíček, enero (1995). "Aritmética acotada, lógica proposicional y teoría de la complejidad", Cambridge University Press.
• Cocinero, Esteban ; Reckhow, Robert A. (1979). "La eficiencia relativa de los sistemas de prueba proposicional". Revista de Lógica Simbólica . 44 (1): 36–50. doi :10.2307/2273702. JSTOR  2273702.
• Buss, SR (1987). "Pruebas de tamaño polinomial del principio de casillero proposicional", Journal of Symbolic Logic 52, págs.
• Pudlák, P., Buss, SR (1995). "Cómo mentir sin ser (fácilmente) condenado y la duración de las pruebas en cálculo proposicional", en: Computer Science Logic'94 (Pacholski y Tiuryn ​​eds.), Springer LNCS 933, 1995, págs.