Sistema Frege

En complejidad de prueba , un sistema de Frege es un sistema de prueba proposicional cuyas pruebas son secuencias de fórmulas derivadas usando un conjunto finito de reglas de inferencia sólidas e implicacionalmente completas . ^[1] Los sistemas de Frege (más conocidos como sistemas de Hilbert en la teoría de prueba general ) reciben su nombre de Gottlob Frege .

El nombre "sistema de Frege" fue definido por primera vez ^[2] por Stephen Cook y Robert Reckhow, ^{[3] [4]} y tenía como objetivo capturar las propiedades de los sistemas de prueba proposicional más comunes. ^[2]

Definición formal

Cook y Reckhow ^{[3] [4]} dieron la primera ^[2] definición formal de un sistema Frege, a la que es equivalente la siguiente, basada en Krajicek, ^{[1] .}

Sea K un conjunto finito funcionalmente completo de conectivos booleanos, y considere fórmulas proposicionales construidas a partir de las variables p ₀ , p ₁ , p ₂ , ... utilizando 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 F -derivación de A a partir de los axiomas X es una secuencia de fórmulas A ₁ , ..., A _m tales que A _m  =  A , y cada A _k es un miembro de X , o se deriva de alguna de las fórmulas A _i , i  <  k , por una instancia de sustitución de una regla de R . Una F -prueba de una fórmula A es una F -derivación de A a partir del conjunto vacío de axiomas (X=∅). F se llama un sistema de Frege si

• F es correcta: toda fórmula F -demostrable es una tautología.
• F es implicacionalmente completa: 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) de una prueba A ₁ , ..., A _m 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 refutativamente completo si para cada conjunto inconsistente de fórmulas X hay una F -derivación de una contradicción fija a partir de X.

Ejemplos

• El cálculo proposicional de Frege no es un sistema de Frege, ya que utiliza axiomas en lugar de esquemas axiomáticos, aunque puede modificarse para ser un sistema de Frege. ^[4]
• Hay muchos ejemplos de reglas de Frege válidas 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 implicacionalmente completa, es decir, no podemos concluir de . Sin embargo, agregar la regla de debilitamiento : la hace implicacionalmente completa ^{[ cita requerida ]} . La resolución también es refutacionalmente completa. ${\displaystyle A\lor B}$ ${\displaystyle A}$ ${\displaystyle {\frac {A}{A\lor B}}}$

Propiedades

• El teorema de Reckhow de 1979 ^[4] establece que todos los sistemas de Frege son p-equivalentes .
• La deducción natural y el cálculo secuencial (sistema de Gentzen con corte) también son p-equivalentes a los sistemas de Frege.
• Existen pruebas de Frege del principio del palomar en tamaño polinomial . ^[5]
• Los sistemas de Frege se consideran sistemas bastante sólidos. A diferencia de, por ejemplo, la resolución, no existen límites inferiores superlineales conocidos para el número de líneas en las demostraciones de Frege, y los límites inferiores más conocidos para el tamaño de las demostraciones son cuadráticos.
• El número mínimo de rondas en el juego demostrador-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 }$

• 
  Resistencia de prueba de diferentes sistemas.

Sistema Frege ampliado

Cook y Reckhow también definieron una extensión de un sistema de Frege, llamada Frege extendido , ^[4] que toma un sistema de Frege F y agrega una regla de derivación adicional que permite derivar una fórmula , donde abrevia su definición en el lenguaje del F particular y el átomo no aparece en fórmulas derivadas previamente incluyendo 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 las demostraciones en Frege extendido como demostraciones de Frege que operan con circuitos en lugar de fórmulas.

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

Referencias

1. Krajicek, Jan (24 de noviembre de 1995). Aritmética limitada, lógica proposicional y teoría de la complejidad. Cambridge University Press. pág. 42. ISBN 978-0-521-45205-2.
2. Pudlák, Pavel; Buss, Samuel R. (1995). Pacholski, Leszek; Tiuryn, Jerzy (eds.). "Cómo mentir sin ser (fácilmente) condenado y la longitud de las pruebas en el cálculo proposicional". Computer Science Logic . Berlín, Heidelberg: Springer: 151–162. doi :10.1007/BFb0022253. ISBN 978-3-540-49404-1.
3. Cook, Stephen; Reckhow, Robert (30 de abril de 1974). "Sobre la longitud de las pruebas en el cálculo proposicional (versión preliminar)". Actas del sexto simposio anual de la ACM sobre teoría de la computación . STOC '74. Nueva York, NY, EE. UU.: Association for Computing Machinery: 135–148. doi :10.1145/800119.803893. ISBN 978-1-4503-7423-1.
4. Cook, Stephen A.; 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. ISSN  0022-4812.
5. Buss, Samuel R. (1987). "Pruebas de tamaño polinomial del principio de palomar proposicional". The Journal of Symbolic Logic . 52 (4): 916–927. doi :10.2307/2273826. ISSN  0022-4812.