Sistema de Hilbert

En lógica , más específicamente en teoría de la demostración , un sistema de Hilbert , a veces llamado cálculo de Hilbert , sistema de estilo Hilbert , sistema de demostración de estilo Hilbert , sistema deductivo de estilo Hilbert o sistema de Hilbert - Ackermann , es un tipo de sistema de demostración formal atribuido a Gottlob Frege ^{[ 1 ]} y David Hilbert . ^{[ 2 ]} 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.

Se define como un sistema deductivo que genera teoremas a partir de axiomas y reglas de inferencia, ^{[ 3 ] [ 4 ] [ 5 ]} especialmente si la única regla de inferencia postulada es el modus ponens . ^{[ 6 ] [ 7 ]} Todo sistema de Hilbert es un sistema axiomático , que muchos autores utilizan como un término menos específico para declarar sus sistemas de Hilbert, ^{[ 8 ] [ 9 ] [ 10 ]} sin mencionar ningún término más específico. En este contexto, los "sistemas de Hilbert" se contraponen a los sistemas de deducción natural , ^{[ 3 ]} en los que no se utilizan axiomas, solo reglas de inferencia.

Si bien todas las fuentes que se refieren a un sistema de prueba lógica "axiomático" lo caracterizan simplemente como un sistema de prueba lógica con axiomas, las fuentes que utilizan variantes del término "sistema de Hilbert" a veces lo definen de maneras diferentes, que no se utilizarán en este artículo. Por ejemplo, Troelstra define un "sistema de Hilbert" como un sistema con axiomas y con${\displaystyle {\rightarrow }E}$y${\displaystyle {\forall }I}$como las únicas reglas de inferencia. ^{[ 11 ]} Un conjunto específico de axiomas también se denomina a veces "el sistema de Hilbert", ^{[ 12 ]} o "el cálculo de estilo Hilbert". ^{[ 13 ]} A veces, "estilo Hilbert" se utiliza para transmitir el tipo de sistema axiomático cuyos axiomas se dan en forma esquemática , ^{[ 2 ]} como en la §  Forma esquemática de P2 a continuación, pero otras fuentes utilizan el término "estilo Hilbert" para abarcar tanto sistemas con axiomas esquemáticos como sistemas con una regla de sustitución, ^{[ 14 ]} como lo hace este artículo. El uso de "estilo Hilbert" y términos similares para describir sistemas de prueba axiomáticos en lógica se debe a la influencia de los Principios de lógica matemática (1928) de Hilbert y Ackermann . ^{[ 2 ]}

La mayoría de las variantes de los sistemas de Hilbert adoptan un enfoque característico en la forma en que equilibran una compensación entre axiomas lógicos y reglas de inferencia . ^{[ 1 ] [ 6 ] [ 15 ] [ 11 ]} 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 enfoque opuesto, incluyendo muchas reglas de deducción pero muy pocos o ningún esquema de axiomas. ^{[ 3 ]} Los sistemas de Hilbert más comúnmente estudiados tienen solo una regla de inferencia – modus ponens , para lógicas proposicionales – o dos – con generalización , para manejar también lógicas 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 adicionalmente 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 axiomáticos, en cuyo caso se requiere la regla de sustitución uniforme . ^{[ 14 ]}    

Una característica distintiva de las numerosas variantes de los sistemas de Hilbert es que el contexto no se modifica en ninguna de sus reglas de inferencia, mientras que tanto la deducción natural como el cálculo de secuentes contienen algunas reglas que sí modifican el contexto. ^{[ 16 ]} Por lo tanto, si solo interesa la derivabilidad de las tautologías , sin juicios hipotéticos, se puede formalizar el sistema de Hilbert de manera que sus reglas de inferencia contengan únicamente juicios de una forma bastante simple. Lo mismo no se puede hacer con los otros dos sistemas de deducción: dado que el contexto se modifica en algunas de sus reglas de inferencia, no se pueden formalizar de forma que se eviten los juicios hipotéticos , ni siquiera si se pretende utilizarlos únicamente para demostrar la derivabilidad de las tautologías. 

En un sistema de Hilbert, una deducción formal (o prueba ) es una secuencia finita de fórmulas en la que cada fórmula es un axioma o se obtiene a partir de fórmulas anteriores mediante una regla de inferencia. ^{[ 17 ]} Estas deducciones formales pretenden reflejar las pruebas en lenguaje natural, aunque son mucho más detalladas. ^{[ 18 ]}

Suponer${\displaystyle \Gamma }$es un conjunto de fórmulas, consideradas como hipótesis . Por ejemplo,${\displaystyle \Gamma }$podría ser un conjunto de axiomas para la teoría de grupos o la teoría de conjuntos . La notación${\displaystyle \Gamma \vdash \phi }$significa que hay una deducción que termina con${\displaystyle \phi }$utilizando como axiomas únicamente axiomas lógicos y elementos de${\displaystyle \Gamma }$. ^{[ 19 ]} Así, informalmente,${\displaystyle \Gamma \vdash \phi }$significa que${\displaystyle \phi }$es demostrable asumiendo todas las fórmulas en${\displaystyle \Gamma }$.

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

A continuación se presentan algunos sistemas de Hilbert que se han utilizado en lógica proposicional . Uno de ellos, la forma esquemática  de P2 , también se considera un sistema de Frege .

Existe una cantidad ilimitada de axiomatizaciones de la lógica de predicados, ya que para cualquier lógica hay libertad en la elección de axiomas y reglas que la caracterizan. Aquí describimos 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. Nos ocupamos de un lenguaje mínimo para esta lógica, donde las fórmulas usan solo los conectores.${\displaystyle \lnot }$y${\displaystyle \to }$y solo el cuantificador${\displaystyle \forall }$. Más adelante mostramos cómo se puede extender el sistema para incluir conectores lógicos adicionales, como${\displaystyle \land }$y${\displaystyle \lor }$, sin ampliar la clase de fórmulas deducibles.

Los primeros cuatro esquemas de axiomas lógicos permiten (junto con el modus ponens) la manipulación de conectores 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, ya que se deduce de P3, P2 y modus ponens (véase la demostración ). Estos axiomas describen la lógica proposicional clásica ; sin el axioma P4 obtenemos la lógica implicacional positiva . La lógica mínima se logra añadiendo en su lugar el axioma P4m, o definiendo${\displaystyle \lnot \phi }$como${\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 añadiendo los axiomas P4i y P5i a la lógica implicacional positiva, o añadiendo 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 un número infinito de instancias específicas de axiomas. Por ejemplo, P1 podría representar la instancia particular del axioma.${\displaystyle p\to p}$o podría representar${\displaystyle \left(p\to q\right)\to \left(p\to q\right)}$: el${\displaystyle \phi }$Es un espacio donde se puede colocar cualquier fórmula. Una variable de este tipo que abarca varias fórmulas se denomina "variable esquemática".

Con una segunda regla de sustitución uniforme (SU), podemos transformar cada uno de estos esquemas axiomáticos en un único axioma, reemplazando cada variable esquemática por alguna variable proposicional que no se menciona en ningún axioma para obtener lo que llamamos axiomatización sustitucional. Ambas formalizaciones tienen variables, pero mientras que la axiomatización de una sola regla tiene variables esquemáticas que están fuera del lenguaje de la lógica, la axiomatización sustitucional utiliza variables proposicionales que realizan la misma función al expresar la idea de una variable que abarca fórmulas con una regla que utiliza la sustitución.

EE. UU. Dejemos${\displaystyle \phi (p)}$ser una fórmula con una o más instancias de la variable proposicional${\displaystyle p}$y dejar${\displaystyle \psi }$ser otra fórmula. Luego de${\displaystyle \phi (p)}$inferir${\displaystyle \phi (\psi )}$.

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

P5.${\displaystyle \forall x\left(\phi \right)\to \phi [x:=t]}$donde t puede sustituirse por x en${\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.${\displaystyle \phi \to \forall x\left(\phi \right)}$donde x no es libre en${\displaystyle \phi }$.

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

A menudo, la cuantificación universal se aproxima mediante una regla de generalización adicional que utiliza una regla adicional, en cuyo caso las reglas Q6 y Q7 resultan redundantes.

• Generalización : Si${\displaystyle \Gamma \vdash \phi }$y x no aparece libre en ninguna fórmula de${\displaystyle \Gamma }$entonces${\displaystyle \Gamma \vdash \forall x\phi }$.

Los esquemas axiomáticos finales son necesarios para trabajar con fórmulas que incluyan el símbolo de igualdad.

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

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

Es común incluir en un sistema de Hilbert únicamente los axiomas para los operadores lógicos de implicación y negación hacia la completitud funcional . Dados estos axiomas, es posible formar extensiones conservadoras del teorema de deducción que permiten el uso de conectores adicionales. Estas extensiones se denominan conservadoras porque si una fórmula φ que involucra nuevos conectores 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 se extiende completamente, un sistema de Hilbert se asemejará más a un sistema de deducción natural .

• Lista de sistemas de Hilbert
• Deducción natural
• Cálculo de secuencias

• Curry, Haskell B.; Robert Feys (1958). Lógica combinatoria Vol. I . Vol.  1. Ámsterdam: North Holland.
• Monk, 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.Se trata de una traducción al húngaro de una selección de artículos 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 referencia en lógica matemática, 1879-1931 ( 3.ª reimpresión,  ed. 1976). Cambridge, MA: Harvard University Press . ISBN 0-674-32449-8.
  • La obra de Hilbert de 1927, basada en una conferencia anterior de 1925 sobre "fundamentos" (págs.  367-392 ), presenta sus 17 axiomas: axiomas de implicación n.° 1-4, axiomas sobre & y V n.° 5-10, axiomas de negación n.° 11-12, su axioma lógico ε n.° 13, axiomas de igualdad n.° 14-15 y axiomas de número n.° 16-17, junto con los demás elementos necesarios de su "teoría de la demostración" formalista, por ejemplo, axiomas de inducción, axiomas de recursión, 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 la metamatemática (10.ª reimpresión con correcciones de 1971  ). Ámsterdam, Nueva York: North Holland Publishing Company. ISBN 0-7204-2103-9.{{cite book}}: Incompatibilidad de ISBN/Fecha ( ayuda )
  • 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 a partir de estos presenta 21 "postulados": 18 axiomas y 3 relaciones de "consecuencia inmediata" divididas de la siguiente manera: Postulados para el cálculo proposicional n.° 1-8, Postulados adicionales para el cálculo de predicados n.° 9-12 y Postulados adicionales para la teoría de números n.° 13-21.

• Gaifman, Haim. "Un sistema deductivo de tipo Hilbert para la lógica proposicional, la completitud y la compacidad" (PDF) .
• Farmer, WM "Lógica proposicional" (PDF) .Describe (entre otras cosas) un sistema de demostración específico al estilo de Hilbert (que se limita al cálculo proposicional ).