sistema Hilbert

Sistema de deducción formal en lógica.

En física matemática , sistema de Hilbert es un término poco utilizado para un sistema físico descrito mediante un álgebra C* .

En lógica , especialmente en lógica matemática , un sistema de Hilbert , a veces llamado cálculo de Hilbert , sistema deductivo estilo Hilbert o sistema de Hilbert-Ackermann , es un tipo de sistema de deducción formal atribuido a Gottlob Frege ^[1] y David Hilbert . Estos sistemas deductivos se estudian con mayor frecuencia para la lógica de primer orden , pero también son de interés para otras lógicas.

La mayoría de las variantes de los sistemas de Hilbert adoptan un rumbo característico en la forma en que equilibran el equilibrio entre axiomas lógicos y reglas de inferencia . ^[1] Los sistemas de Hilbert pueden caracterizarse por la elección de un gran número de esquemas de axiomas lógicos y un pequeño conjunto de reglas de inferencia . Los sistemas de deducción natural adoptan el rumbo opuesto, e incluyen muchas reglas de deducción pero muy pocos o ningún esquema de axiomas. Los sistemas de Hilbert más comúnmente estudiados tienen una sola regla de inferencia ( modus ponens , para lógica proposicional  ) o dos (con generalización , para manejar también lógica de predicados ) y varios esquemas de axiomas infinitos. Los sistemas de Hilbert para lógicas modales aléticas , a veces llamados sistemas de Hilbert-Lewis, requieren además la regla de necesidad. Algunos sistemas utilizan una lista finita de fórmulas concretas como axiomas en lugar de un conjunto infinito de fórmulas mediante esquemas de axiomas, en cuyo caso se requiere la regla de sustitución uniforme.

Un rasgo característico de las muchas variantes de los sistemas de Hilbert es que el contexto no cambia en ninguna de sus reglas de inferencia, mientras que tanto la deducción natural como el cálculo secuencial contienen algunas reglas que cambian el contexto. Así, si uno está interesado sólo en la derivabilidad de las tautologías , no en juicios hipotéticos, entonces puede formalizar el sistema de Hilbert de tal manera que sus reglas de inferencia contengan sólo juicios de una forma bastante simple. No se puede hacer lo mismo con los otros dos sistemas de deducciones: ^{[ cita necesaria ]} a medida que se cambia el contexto en algunas de sus reglas de inferencia, no se pueden formalizar de modo que se puedan evitar juicios hipotéticos, ni siquiera si queremos usarlos solo para demostrando la derivabilidad de tautologías.

Deducciones formales

Una representación gráfica del sistema de deducción.

En un sistema de deducción al estilo de Hilbert, una deducción formal es una secuencia finita de fórmulas en la que cada fórmula es un axioma o se obtiene de fórmulas anteriores mediante una regla de inferencia. Estas deducciones formales pretenden reflejar las pruebas en lenguaje natural, aunque son mucho más detalladas.

Supongamos que es un conjunto de fórmulas, consideradas como hipótesis . Por ejemplo, podría ser un conjunto de axiomas para la teoría de grupos o la teoría de conjuntos . La notación significa que hay una deducción que termina usando como axiomas sólo axiomas lógicos y elementos de . Por lo tanto, de manera informal, significa que es demostrable asumiendo todas las fórmulas en . ${\displaystyle \Gamma }$ ${\displaystyle \Gamma }$ ${\displaystyle \Gamma \vdash \phi }$ ${\displaystyle \phi }$ ${\displaystyle \Gamma }$ ${\displaystyle \Gamma \vdash \phi }$ ${\displaystyle \phi }$ ${\displaystyle \Gamma }$

Los sistemas de deducción al estilo de Hilbert se caracterizan por el uso de numerosos esquemas de axiomas lógicos . Un esquema de axiomas es un conjunto infinito de axiomas obtenidos sustituyendo todas las fórmulas de alguna forma en un patrón específico. El conjunto de axiomas lógicos incluye no sólo aquellos axiomas generados a partir de este patrón, sino también cualquier generalización de uno de esos axiomas. Una generalización de una fórmula se obtiene anteponiendo cero o más cuantificadores universales a la fórmula; por ejemplo es una generalización de . ${\displaystyle \forall y(\forall xPxy\to Pty)}$ ${\displaystyle \forall xPxy\to Pty}$

Axiomas lógicos

Existen varias axiomatizaciones variantes de la lógica de predicados, ya que para cualquier lógica hay libertad para elegir axiomas y reglas que caractericen esa lógica. Describimos aquí un sistema de Hilbert con nueve axiomas y solo la regla modus ponens, que llamamos axiomatización de una regla y que describe la lógica ecuacional clásica. Se trata de un lenguaje mínimo para esta lógica, donde las fórmulas utilizan sólo los conectivos y sólo el cuantificador . Más adelante mostramos cómo se puede ampliar el sistema para incluir conectivos lógicos adicionales, como y , sin ampliar la clase de fórmulas deducibles. ${\displaystyle \lnot }$ ${\displaystyle \to }$ ${\displaystyle \forall }$ ${\displaystyle \land }$ ${\displaystyle \lor }$

Los primeros cuatro esquemas de axiomas lógicos permiten (junto con el modus ponens) la manipulación de conectivos lógicos.

P1. ${\displaystyle \phi \to \phi }$

P2. ${\displaystyle \phi \to \left(\psi \to \phi \right)}$

P3. ${\displaystyle \left(\phi \to \left(\psi \rightarrow \xi \right)\right)\to \left(\left(\phi \to \psi \right)\to \left(\phi \to \xi \right)\right)}$

P4. ${\displaystyle \left(\lnot \phi \to \lnot \psi \right)\to \left(\psi \to \phi \right)}$

El axioma P1 es redundante, como se desprende de P3, P2 y el modus ponens (ver prueba ). Estos axiomas describen la lógica proposicional clásica ; sin el axioma P4 obtenemos lógica implicacional positiva . La lógica mínima se logra agregando en su lugar el axioma P4m o definiendo como . ${\displaystyle \lnot \phi }$ ${\displaystyle \phi \to \bot }$

P4m. ${\displaystyle \left(\phi \to \psi \right)\to \left(\left(\phi \to \lnot \psi \right)\to \lnot \phi \right)}$

La lógica intuicionista se logra agregando los axiomas P4i y P5i a la lógica implicacional positiva, o agregando el axioma P5i a la lógica mínima. Tanto P4i como P5i son teoremas de la lógica proposicional clásica.

P4i. ${\displaystyle \left(\phi \to \lnot \phi \right)\to \lnot \phi }$

P5i. ${\displaystyle \lnot \phi \to \left(\phi \to \psi \right)}$

Tenga en cuenta que estos son esquemas de axiomas, que representan infinitos casos específicos de axiomas. Por ejemplo, P1 podría representar la instancia de axioma particular , o podría representar : es un lugar donde se puede colocar cualquier fórmula. Una variable como esta que abarca fórmulas se denomina "variable esquemática". ${\displaystyle p\to p}$ ${\displaystyle \left(p\to q\right)\to \left(p\to q\right)}$ ${\displaystyle \phi }$

Con una segunda regla de sustitución uniforme (US), podemos cambiar cada uno de estos esquemas de axiomas en un solo axioma, reemplazando cada variable esquemática por alguna variable proposicional que no se menciona en ningún axioma para obtener lo que llamamos la axiomatización sustitutiva. Ambas formalizaciones tienen variables, pero donde la axiomatización de una regla tiene variables esquemáticas que están fuera del lenguaje de la lógica, la axiomatización sustitutiva usa variables proposicionales que hacen el mismo trabajo al expresar la idea de una variable que abarca fórmulas con una regla que usa sustitución.

A NOSOTROS. Sea una fórmula con una o más instancias de la variable proposicional y sea otra fórmula. Luego de , inferir . ^{[ dudoso ]} ${\displaystyle \phi (p)}$ ${\displaystyle p}$ ${\displaystyle \psi }$ ${\displaystyle \phi (p)}$ ${\displaystyle \phi (\psi )}$

Los siguientes tres esquemas de axiomas lógicos proporcionan formas de agregar, manipular y eliminar cuantificadores universales.

P5. donde t puede sustituirse por x en ${\displaystyle \forall x\left(\phi \right)\to \phi [x:=t]}$ ${\displaystyle \,\!\phi }$

P6. ${\displaystyle \forall x\left(\phi \to \psi \right)\to \left(\forall x\left(\phi \right)\to \forall x\left(\psi \right)\right)}$

P7. donde x no es libre en . ${\displaystyle \phi \to \forall x\left(\phi \right)}$ ${\displaystyle \phi }$

Estas tres reglas adicionales amplían el sistema proposicional para axiomatizar la lógica de predicados clásica . Asimismo, estas tres reglas extienden el sistema de la lógica proposicional intuicionista (con P1-3 y P4i y P5i) a la lógica de predicados intuicionista.

A la cuantificación universal a menudo se le da una axiomatización alternativa utilizando una regla de generalización adicional (ver la sección sobre Metateoremas), en cuyo caso las reglas Q6 y Q7 son redundantes. ^{[ dudoso ]}

Los esquemas de axiomas finales deben funcionar con fórmulas que involucran el símbolo de igualdad.

I8. para cada variable x . ${\displaystyle x=x}$

I9. ${\displaystyle \left(x=y\right)\to \left(\phi [z:=x]\to \phi [z:=y]\right)}$

Extensiones conservadoras

Es común incluir en un sistema de deducción al estilo de Hilbert sólo axiomas de implicación y negación. Dados estos axiomas, es posible formar extensiones conservadoras del teorema de deducción que permitan el uso de conectivos adicionales. Estas extensiones se llaman conservadoras porque si una fórmula φ que involucra nuevos conectivos se reescribe como una fórmula lógicamente equivalente θ que involucra solo negación, implicación y cuantificación universal, entonces φ es derivable en el sistema extendido si y solo si θ es derivable en el sistema original. . Cuando esté completamente extendido, un sistema de estilo Hilbert se parecerá más a un sistema de deducción natural .

Cuantificación existencial

• Introducción

${\displaystyle \forall x(\phi \to \exists y(\phi [x:=y]))}$

• Eliminación

${\displaystyle \forall x(\phi \to \psi )\to \exists x(\phi )\to \psi }$donde no es una variable libre de . ${\displaystyle x}$ ${\displaystyle \psi }$

Conjunción y disyunción

• Introducción y eliminación de conjunciones.

introducción: ${\displaystyle \alpha \to (\beta \to \alpha \land \beta )}$

eliminación restante: ${\displaystyle \alpha \wedge \beta \to \alpha }$

derecho de eliminación: ${\displaystyle \alpha \wedge \beta \to \beta }$

• Introducción y eliminación de disyunciones.

introducción a la izquierda: ${\displaystyle \alpha \to \alpha \vee \beta }$

introducción a la derecha: ${\displaystyle \beta \to \alpha \vee \beta }$

eliminación: ${\displaystyle (\alpha \to \gamma )\to ((\beta \to \gamma )\to \alpha \vee \beta \to \gamma )}$

Metateoremas

Debido a que los sistemas de estilo Hilbert tienen muy pocas reglas de deducción, es común demostrar metateoremas que muestran que reglas de deducción adicionales no añaden poder deductivo, en el sentido de que una deducción que usa las nuevas reglas de deducción se puede convertir en una deducción usando solo la deducción original. normas.

Algunos metateoremas comunes de esta forma son:

• El teorema de la deducción : si y sólo si . ${\displaystyle \Gamma ;\phi \vdash \psi }$ ${\displaystyle \Gamma \vdash \phi \to \psi }$
• ${\displaystyle \Gamma \vdash \phi \leftrightarrow \psi }$si y sólo si y . ${\displaystyle \Gamma \vdash \phi \to \psi }$ ${\displaystyle \Gamma \vdash \psi \to \phi }$
• Contraposición: Si entonces . ${\displaystyle \Gamma ;\phi \vdash \psi }$ ${\displaystyle \Gamma ;\lnot \psi \vdash \lnot \phi }$
• Generalización : Si y x no aparecen libres en ninguna fórmula de entonces . ${\displaystyle \Gamma \vdash \phi }$ ${\displaystyle \Gamma }$ ${\displaystyle \Gamma \vdash \forall x\phi }$

Algunos teoremas útiles y sus demostraciones.

A continuación se presentan varios teoremas de lógica proposicional, junto con sus demostraciones (o enlaces a estas demostraciones en otros artículos). Tenga en cuenta que dado que (P1) se puede demostrar utilizando los otros axiomas, de hecho (P2), (P3) y (P4) son suficientes para demostrar todos estos teoremas.

(HS1) - Silogismo hipotético , ver prueba . ${\displaystyle (q\to r)\to ((p\to q)\to (p\to r))}$

(L1) - prueba: ${\displaystyle p\to ((p\to q)\to q)}$

(1)       (instancia de (P3)) ${\displaystyle ((p\to q)\to (p\to q))\to (((p\to q)\to p)\to ((p\to q)\to q))}$

(2)       (instancia de (P1)) ${\displaystyle (p\to q)\to (p\to q)}$

(3)       (de (2) y (1) por modus ponens ) ${\displaystyle ((p\to q)\to p)\to ((p\to q)\to q)}$

(4)       (instancia de (HS1)) ${\displaystyle (((p\to q)\to p)\to ((p\to q)\to q))\to ((p\to ((p\to q)\to p))\to (p\to ((p\to q)\to q)))}$

(5)       (de (3) y (4) por modus ponens) ${\displaystyle (p\to ((p\to q)\to p))\to (p\to ((p\to q)\to q))}$

(6)       (instancia de (P2)) ${\displaystyle p\to ((p\to q)\to p)}$

(7)       (de (6) y (5) por modus ponens) ${\displaystyle p\to ((p\to q)\to q)}$

Los dos teoremas siguientes se conocen juntos como doble negación :

(DN1) ${\displaystyle \neg \neg p\to p}$

(DN2) ${\displaystyle p\to \neg \neg p}$

Ver pruebas .

(L2) - para esta prueba utilizamos el método del metateorema del silogismo hipotético como abreviatura de varios pasos de la prueba: ${\displaystyle (p\to (q\to r))\to (q\to (p\to r))}$

(1)       (instancia de (P3)) ${\displaystyle (p\to (q\to r))\to ((p\to q)\to (p\to r))}$

(2)       (instancia de (HS1)) ${\displaystyle ((p\to q)\to (p\to r))\to ((q\to (p\to q))\to (q\to (p\to r)))}$

(3)       (de (1) y (2) utilizando el metateorema del silogismo hipotético) ${\displaystyle (p\to (q\to r))\to ((q\to (p\to q))\to (q\to (p\to r)))}$

(4)       (instancia de (P3)) ${\displaystyle ((p\to (q\to r))\to ((q\to (p\to q))\to (q\to (p\to r))))\to (((p\to (q\to r))\to (q\to (p\to q)))\to ((p\to (q\to r))\to (q\to (p\to r))))}$

(5)       (de (3) y (4) usando modus ponens) ${\displaystyle ((p\to (q\to r))\to (q\to (p\to q)))\to ((p\to (q\to r))\to (q\to (p\to r)))}$

(6)       (instancia de (P2)) ${\displaystyle q\to (p\to q)}$

(7)       (instancia de (P2)) ${\displaystyle (q\to (p\to q))\to ((p\to (q\to r))\to (q\to (p\to q)))}$

(8)       (de (6) y (7) usando modus ponens) ${\displaystyle (p\to (q\to r))\to (q\to (p\to q))}$

(9)       (de (8) y (5) usando modus ponens) ${\displaystyle (p\to (q\to r))\to (q\to (p\to r))}$

(HS2) - una forma alternativa del silogismo hipotético . prueba: ${\displaystyle (p\to q)\to ((q\to r)\to (p\to r))}$

(1)       (instancia de (HS1)) ${\displaystyle (q\to r)\to ((p\to q)\to (p\to r))}$

(2)       (instancia de (L2)) ${\displaystyle ((q\to r)\to ((p\to q)\to (p\to r)))\to ((p\to q)\to ((q\to r)\to (p\to r)))}$

(3) (de (1) y (2) por modus ponens) ${\displaystyle (p\to q)\to ((q\to r)\to (p\to r))}$

(TR1) - Transposición, ver prueba (la otra dirección de transposición es (P4)). ${\displaystyle (p\to q)\to (\neg q\to \neg p)}$

(TR2) - otra forma de transposición; prueba: ${\displaystyle (\neg p\to q)\to (\neg q\to p)}$

(1)       (instancia de (TR1)) ${\displaystyle (\neg p\to q)\to (\neg q\to \neg \neg p)}$

(2)       (instancia de (DN1)) ${\displaystyle \neg \neg p\to p}$

(3)       (instancia de (HS1)) ${\displaystyle (\neg \neg p\to p)\to ((\neg q\to \neg \neg p)\to (\neg q\to p))}$

(4)       (de (2) y (3) por modus ponens) ${\displaystyle (\neg q\to \neg \neg p)\to (\neg q\to p)}$

(5)       (de (1) y (4) utilizando el metateorema del silogismo hipotético) ${\displaystyle (\neg p\to q)\to (\neg q\to p)}$

(L3) - prueba: ${\displaystyle (\neg p\to p)\to p}$

(1)       (instancia de (P2)) ${\displaystyle \neg p\to (\neg \neg (q\to q)\to \neg p)}$

(2)       (instancia de (P4)) ${\displaystyle (\neg \neg (q\to q)\to \neg p)\to (p\to \neg (q\to q))}$

(3)       (de (1) y (2) utilizando el metateorema del silogismo hipotético) ${\displaystyle \neg p\to (p\to \neg (q\to q))}$

(4)       (instancia de (P3)) ${\displaystyle (\neg p\to (p\to \neg (q\to q)))\to ((\neg p\to p)\to (\neg p\to \neg (q\to q)))}$

(5)       (de (3) y (4) usando modos ponens) ${\displaystyle (\neg p\to p)\to (\neg p\to \neg (q\to q))}$

(6)       (instancia de (P4)) ${\displaystyle (\neg p\to \neg (q\to q))\to ((q\to q)\to p)}$

(7)       (de (5) y (6) usando el metateorema del silogismo hipotético) ${\displaystyle (\neg p\to p)\to ((q\to q)\to p)}$

(8)       (instancia de (P1)) ${\displaystyle q\to q}$

(9)       (instancia de (L1)) ${\displaystyle (q\to q)\to (((q\to q)\to p)\to p)}$

(10)       (de (8) y (9) usando modos ponens) ${\displaystyle ((q\to q)\to p)\to p}$

(11)       (de (7) y (10) usando el metateorema del silogismo hipotético) ${\displaystyle (\neg p\to p)\to p}$

Axiomatizaciones alternativas

El axioma 3 anterior se atribuye a Łukasiewicz . ^[2] El sistema original de Frege tenía los axiomas P2 y P3 pero otros cuatro axiomas en lugar del axioma P4 (ver el cálculo proposicional de Frege ). Russell y Whitehead también sugirieron un sistema con cinco axiomas proposicionales.

Otras conexiones

Los axiomas P1, P2 y P3, con la regla de deducción modus ponens (que formaliza la lógica proposicional intuicionista), corresponden a los combinadores de bases de lógica combinatoria I , K y S con el operador de aplicación. Las pruebas en el sistema de Hilbert corresponden entonces a términos combinadores en lógica combinatoria. Véase también la correspondencia entre Curry y Howard .

Ver también

• Lista de sistemas Hilbert
• deducción natural

Notas

1. Máté y Ruzsa 1997:129
2. A. Tarski, Lógica, semántica, metamatemáticas, Oxford, 1956

Referencias

• Curry, Haskell B.; Robert Feys (1958). Lógica combinatoria vol. I . vol. 1. Ámsterdam: Holanda Septentrional.
• Monje, J. Donald (1976). Lógica Matemática . Textos de Posgrado en Matemáticas. Berlín, Nueva York: Springer-Verlag . ISBN 978-0-387-90170-1.
• Ruzsa, Imre; Máté, András (1997). Bevezetés a modern logikába (en húngaro). Budapest: Osiris Kiadó.
• Tarski, Alfred (1990). Bizonyítás és igazság (en húngaro). Budapest: góndola.Es una traducción al húngaro de los artículos seleccionados de Alfred Tarski sobre la teoría semántica de la verdad .
• David Hilbert (1927) "Los fundamentos de las matemáticas", traducido por Stephan Bauer-Menglerberg y Dagfinn Føllesdal (págs. 464–479). en:
  • van Heijenoort, Jean (1967). De Frege a Gödel: un libro de consulta sobre lógica matemática, 1879-1931 (tercera edición, edición de 1976). Cambridge MA: Harvard University Press. ISBN 0-674-32449-8.
  • Hilbert's 1927, basado en una conferencia anterior sobre "fundamentos" de 1925 (págs. 367-392), presenta sus 17 axiomas: axiomas de implicación #1-4, axiomas sobre & y V #5-10, axiomas de negación #11- 12, su ε-axioma lógico #13, axiomas de igualdad #14-15 y axiomas de números #16-17, junto con los otros elementos necesarios de su "teoría de la prueba" formalista, por ejemplo, axiomas de inducción, axiomas de recursividad, etc; también ofrece una enérgica defensa contra el intuicionismo de LEJ Brouwer. Véanse también los comentarios y la refutación de Hermann Weyl (1927) (págs. 480–484), el apéndice de Paul Bernay (1927) a la conferencia de Hilbert (págs. 485–489) y la respuesta de Luitzen Egbertus Jan Brouwer (1927) (págs. 490–495).
• Kleene, Stephen Cole (1952). Introducción a las metamatemáticas (décima impresión con correcciones de 1971, edición). Ámsterdam Nueva York: Compañía editorial de North Holland. ISBN 0-7204-2103-9.
  • Véase en particular el Capítulo IV Sistema formal (págs. 69–85), donde Kleene presenta los subcapítulos §16 Símbolos formales, §17 Reglas de formación, §18 Variables libres y ligadas (incluida la sustitución), §19 Reglas de transformación (por ejemplo, modus ponens). y de estos presenta 21 "postulados" - 18 axiomas y 3 relaciones de "consecuencia inmediata" divididas de la siguiente manera: Postulados para el cálculo proposicional #1-8, Postulados adicionales para el cálculo de predicados #9-12, y Postulados adicionales para Teoría de números #13-21.

enlaces externos

• Gaifman, Haim. "Un sistema deductivo tipo Hilbert para lógica oracional, completitud y compacidad" (PDF) .
• Farmer, WM "Lógica proposicional" (PDF) .Describe (entre otros) una parte del sistema de deducción al estilo de Hilbert (restringido al cálculo proposicional ).