En la complejidad de la 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 . Los sistemas de Frege (más a menudo 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 las variables p 0 , p 1 , p 2 , ... usando K. conectivos. Una regla de Frege es una regla de inferencia de la forma
donde B 1 , ..., 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 axiomas X es una secuencia de fórmulas A 1 , ..., A m tal que A m = A , y cada A k es un miembro de X , o se deriva de algunas de las fórmulas a i , i < k , por una sustitución ejemplo de una regla de R . Una prueba F de una fórmula A es una derivación F de A del conjunto vacío de axiomas (X = ∅). F se llama sistema de Frege si
- F es sólida: toda fórmula demostrable de F es una tautología.
- F es implicationally completa: para cada fórmula A y un conjunto de fórmulas X , si X implica A , entonces hay un F -derivation de A de X .
La longitud (número de líneas) en una prueba A 1 , ..., 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 arriba es refutationally completa, si para cada conjunto inconsistente de las fórmulas X , existe un F -derivation de una contradicción fijo de X .
Ejemplos de
- El cálculo proposicional de Frege es un sistema de Frege.
- Hay muchos ejemplos de reglas sólidas de Frege en la página Cálculo proposicional .
- La resolución no es un sistema de Frege porque solo 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 de . Sin embargo, agregando la regla de debilitamiento :lo hace implicacionalmente completo. La resolución también es refutadamente completa.
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 de Gentzen con corte) también son p-equivalentes a los sistemas de Frege.
- Hay pruebas de Frege de tamaño polinómico del principio de casillero (Buss 1987).
- Los sistemas de Frege se consideran sistemas bastante fuertes. A diferencia de, digamos, la resolución, no hay límites inferiores superlineales conocidos en el número de líneas en las pruebas de Frege, y los límites inferiores más conocidos en el tamaño de las pruebas son cuadráticos.
- El número mínimo de rondas en el juego prover-adversario necesario para demostrar una tautología. es proporcional al logaritmo del número mínimo de pasos en una prueba de Frege de .
Prueba de fortalezas de diferentes sistemas.
Sistema Frege extendido
Una extensión importante de un sistema de Frege, el llamado Extended Frege , se define tomando un sistema de Frege F y agregando una regla de derivación adicional que permite derivar la fórmula, dónde abrevia su definición en el lenguaje de la F particular y el átomo no ocurre en fórmulas derivadas previamente, incluidos axiomas y en la fórmula .
El propósito de la nueva regla de derivación es introducir 'nombres' o atajos para fórmulas arbitrarias. Permite interpretar pruebas en Extended Frege como pruebas de Frege que operan con circuitos en lugar de fórmulas.
La correspondencia de Cook permite interpretar Extended Frege como un equivalente no uniforme de la teoría PV de Cook y la teoría de Buss formalizar el razonamiento factible (polinomio-tiempo).
Referencias
- Krajíček, Jan (1995). "Aritmética limitada, lógica proposicional y teoría de la complejidad", Cambridge University Press.
- Cook, Stephen ; Reckhow, Robert A. (1979). "La eficiencia relativa de los sistemas de prueba proposicionales". Revista de lógica simbólica . 44 (1): 36–50. doi : 10.2307 / 2273702 . JSTOR 2273702 .
- Buss, SR (1987). "Pruebas de tamaño polinómico del principio de casillero proposicional", Journal of Symbolic Logic 52, págs. 916–927.
- Pudlák, P., Buss, SR (1995). "Cómo mentir sin ser (fácilmente) condenado y la extensión de las pruebas en el cálculo proposicional", en: Computer Science Logic'94 (Pacholski y Tiuryn eds.), Springer LNCS 933, 1995, pp. 151-162.