Sistema de Hilbert

Sistema de deducción formal en lógica

En lógica , más específicamente en teoría de pruebas , un sistema de Hilbert , a veces llamado cálculo de Hilbert , sistema de estilo Hilbert , sistema de prueba de estilo Hilbert , sistema deductivo de estilo Hilbert o sistema de Hilbert-Ackermann , es un tipo de sistema de prueba 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 es el modus ponens . ^{[6] [7]} Todo sistema de Hilbert es un sistema axiomático , que es utilizado por muchos autores como único 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 contrastan con los sistemas de deducción natural , ^[3] en los que no se utilizan axiomas, solo reglas de inferencia.

Aunque todas las fuentes que hacen referencia 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 formas 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 y como únicas reglas de inferencia. ^[11] A un conjunto específico de axiomas también se le denomina a veces "el sistema de Hilbert", ^[12] o "el cálculo al estilo de Hilbert". ^[13] A veces, se utiliza "al estilo de Hilbert" para transmitir el tipo de sistema axiomático que tiene sus axiomas dados en forma esquemática , ^[2] como en el § Forma esquemática de P2 a continuación, pero otras fuentes utilizan el término "al estilo de Hilbert" para abarcar tanto los sistemas con axiomas esquemáticos como los sistemas con una regla de sustitución, ^[14] como lo hace este artículo. El uso del "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 de Hilbert y Ackermann (1928). ^[2] ${\displaystyle {\rightarrow }E}$ ${\displaystyle {\forall }I}$

La mayoría de las variantes de los sistemas de Hilbert adoptan un enfoque característico en la forma en que equilibran un equilibrio entre axiomas lógicos y reglas de inferencia . ^{[1] [15] [16] [17]} Los sistemas de Hilbert se pueden caracterizar 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 estudiados tienen solo una regla de inferencia ( modus ponens , para lógicas proposicionales  ) o dos (con generalización , para manejar lógicas de predicados también) 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 a través de esquemas de axiomas, en cuyo caso se requiere la regla de sustitución uniforme. ^[18]

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 consecuente contienen algunas reglas que cambian el contexto. ^[19] Por lo tanto, si uno está interesado solo en la derivabilidad de las tautologías , no en los juicios hipotéticos, entonces puede formalizar el sistema de Hilbert de tal manera que sus reglas de inferencia contengan solo juicios de una forma bastante simple. Lo mismo no se puede hacer con los otros dos sistemas de deducción: ^{[ cita requerida ]} como el contexto cambia en algunas de sus reglas de inferencia, no se pueden formalizar de modo que se puedan evitar los juicios hipotéticos, ni siquiera si queremos usarlos solo para probar la derivabilidad de las tautologías.

Deducciones formales

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

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. Estas deducciones formales tienen como objetivo reflejar las pruebas del 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 con el uso como axiomas solo de axiomas lógicos y elementos de . Por lo tanto, informalmente, significa que es demostrable suponiendo 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 Hilbert se caracterizan por el uso de numerosos esquemas de axiomas lógicos . Un esquema de axiomas es un conjunto infinito de axiomas obtenidos al sustituir todas las fórmulas de alguna forma en un patrón específico. 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. 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}$

Lógica proposicional

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 .

De FregeEscritura de constitución

Las demostraciones axiomáticas se han utilizado en matemáticas desde el famoso libro de texto griego antiguo Elementos de geometría de Euclides , alrededor del año 300 a. C. Pero el primer sistema de demostración totalmente formalizado conocido que, por lo tanto, califica como un sistema de Hilbert se remonta a la Begriffsschrift de Gottlob Frege de 1879. ^{[9] [20]} El sistema de Frege usaba solo la implicación y la negación como conectivos, ^[21] y tenía seis axiomas, ^[20] que eran los siguientes: ^{[22] [23]}

• Proposición 1: ${\displaystyle a\supset (b\supset a)}$
• Proposición 2: ${\displaystyle (c\supset (b\supset a))\supset ((c\supset b)\supset (c\supset a))}$
• Proposición 8: ${\displaystyle (d\supset (b\supset a))\supset (b\supset (d\supset a))}$
• Proposición 28: ${\displaystyle (b\supset a)\supset (\neg a\supset \neg b)}$
• Proposición 31: ${\displaystyle \neg \neg a\supset a}$
• Proposición 41: ${\displaystyle a\supset \neg \neg a}$

Frege los utilizó junto con el modus ponens y una regla de sustitución (que se utilizó pero nunca se enunció con precisión) para producir una axiomatización completa y consistente de la lógica proposicional funcional de la verdad clásica. ^[22]

P de Łukasiewicz2

Jan Łukasiewicz demostró que, en el sistema de Frege, "el tercer axioma es superfluo ya que puede derivarse de los dos axiomas anteriores, y que los tres últimos axiomas pueden reemplazarse por la oración única ". ^[23] Lo cual, sacado de la notación polaca de Łukasiewicz a la notación moderna, significa . Por lo tanto, a Łukasiewicz se le atribuye ^[20] este sistema de tres axiomas: ${\displaystyle CCNpNqCqp}$ ${\displaystyle (\neg p\rightarrow \neg q)\rightarrow (q\rightarrow p)}$

• ${\displaystyle p\to (q\to p)}$
• ${\displaystyle (p\to (q\to r))\to ((p\to q)\to (p\to r))}$
• ${\displaystyle (\neg p\to \neg q)\to (q\to p)}$

Al igual que el sistema de Frege, este sistema utiliza una regla de sustitución y utiliza el modus ponens como regla de inferencia. ^[20] El mismo sistema exacto fue dado (con una regla de sustitución explícita) por Alonzo Church , ^[24] quien se refirió a él como el sistema P _2, ^{[24] [25]} y ayudó a popularizarlo. ^[25]

Forma esquemática de P2

Se puede evitar el uso de la regla de sustitución dando los axiomas en forma esquemática, utilizándolos para generar un conjunto infinito de axiomas. Por lo tanto, utilizando letras griegas para representar esquemas (variables metalógicas que pueden representar cualquier fórmula bien formada ), los axiomas se dan como: ^{[9] [25]}

• ${\displaystyle \varphi \to (\psi \to \varphi )}$
• ${\displaystyle (\varphi \to (\psi \to \chi ))\to ((\varphi \to \psi )\to (\varphi \to \chi ))}$
• ${\displaystyle (\neg \varphi \to \neg \psi )\to (\psi \to \varphi )}$

La versión esquemática de P ₂ se atribuye a John von Neumann , ^[20] y se utiliza en la base de datos de pruebas formales "set.mm" de Metamath . ^[25] De hecho, la idea misma de utilizar esquemas axiomáticos para reemplazar la regla de sustitución se atribuye a von Neumann. ^[26] La versión esquemática de P ₂ también se ha atribuido a Hilbert , y se la nombró en este contexto. ^[27] ${\displaystyle {\mathcal {H}}}$

Los sistemas de lógica proposicional cuyas reglas de inferencia son esquemáticas también se denominan sistemas de Frege ; como señalan los autores que originalmente definieron el término "sistema de Frege" ^[28] , esto en realidad excluye el propio sistema de Frege, dado anteriormente, ya que tenía axiomas en lugar de esquemas de axiomas. ^[26]

Ejemplo de prueba en P₂

A modo de ejemplo, se ofrece a continuación una demostración de en P _2. Primero, se dan nombres a los axiomas: ${\displaystyle A\to A}$

(A1) ${\displaystyle (p\to (q\to p))}$

(A2) ${\displaystyle ((p\to (q\to r))\to ((p\to q)\to (p\to r)))}$

(A3) ${\displaystyle ((\neg p\to \neg q)\to (q\to p))}$

Y la prueba es la siguiente:

1. ${\displaystyle A\to ((B\to A)\to A)}$       (instancia de (A1))
2. ${\displaystyle (A\to ((B\to A)\to A))\to ((A\to (B\to A))\to (A\to A))}$       (instancia de (A2))
3. ${\displaystyle (A\to (B\to A))\to (A\to A)}$       (de (1) y (2) por modus ponens )
4. ${\displaystyle A\to (B\to A)}$       (instancia de (A1))
5. ${\displaystyle A\to A}$       (de (4) y (3) por modus ponens)

Lógica de predicados (sistema de ejemplo)

Existe una cantidad ilimitada de axiomatizaciones de la lógica de predicados, ya que para cualquier lógica hay libertad para elegir axiomas y reglas que caracterizan esa lógica. Describimos aquí un sistema de Hilbert con nueve axiomas y solo la regla modus ponens, que llamamos la axiomatización de una regla y que describe la lógica ecuacional clásica. Tratamos con un lenguaje mínimo para esta lógica, donde las fórmulas usan solo los conectivos y y solo el cuantificador . Más adelante mostramos cómo el sistema puede extenderse 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 axiomáticos 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, ya que se sigue de P3, P2 y 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 ya sea 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 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 axiomáticos que representan una cantidad infinita de instancias específicas de axiomas. Por ejemplo, P1 podría representar la instancia axiomática particular o podría representar : el 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 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 la axiomatización sustitucional. 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 sustitucional utiliza variables proposicionales que hacen el mismo trabajo al expresar la idea de una variable que se extiende a lo largo de fórmulas con una regla que utiliza la sustitución.

EE. UU. Sea una fórmula con una o más instancias de la variable proposicional , y sea otra fórmula. Luego, a partir de , infiera . ${\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.

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

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

Q7. donde x no es libre en . ${\displaystyle \phi \to \forall x\left(\phi \right)}$ ${\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 la cuantificación universal a menudo se le da una axiomatización alternativa utilizando una regla adicional de generalización (ver la sección sobre Metateoremas), en cuyo caso las reglas Q6 y Q7 son redundantes.

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

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

Yo9. ${\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 Hilbert solo axiomas para los operadores lógicos implicación y negación hacia la completitud funcional . Dados estos axiomas, es posible formar extensiones conservativas del teorema de deducción que permiten el uso de conectivos adicionales. Estas extensiones se denominan conservativas 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 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 a la izquierda: ${\displaystyle \alpha \wedge \beta \to \alpha }$

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

• Introducción y eliminación de la disyunción

Introducción izquierda: ${\displaystyle \alpha \to \alpha \vee \beta }$

Introducción 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 Hilbert tienen muy pocas reglas de deducción, es común probar metateoremas que muestran que las reglas de deducción adicionales no agregan poder deductivo, en el sentido de que una deducción que utiliza las nuevas reglas de deducción puede convertirse en una deducción que utiliza solo las reglas de deducción originales.

Véase también

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

Notas

1. Máté y Ruzsa 1997:129
2. Smith, Peter (21 de febrero de 2013). Introducción a los teoremas de Gödel. Cambridge University Press. pág. 10. ISBN 978-1-107-02284-3.
3. Restall, Greg (11 de septiembre de 2002). Introducción a la lógica subestructural. Routledge. pp. 73–74. ISBN 978-1-135-11131-1.
4. Gaifman, Haim (2002). "Un sistema deductivo de tipo Hilbert para lógica oracional, completitud y compacidad" (PDF) . Columbia . Consultado el 19 de agosto de 2024 .
5. Benthem, Johan van; Gupta, Amitabha; Parikh, Rohit (2 de abril de 2011). Prueba, computación y agencia: la lógica en la encrucijada. Springer Science & Business Media. pág. 41. ISBN 978-94-007-0080-2.
6. Bacon, Andrew (29 de septiembre de 2023). Introducción filosófica a la lógica de orden superior. Taylor & Francis. pág. 424. ISBN 978-1-000-92575-3.
7. Eijck, Jan van (26 de febrero de 1991). Lógica en IA: Taller europeo JELIA '90, Ámsterdam, Países Bajos, 10-14 de septiembre de 1990. Actas. Springer Science & Business Media. pág. 113. ISBN 978-3-540-53686-4.
8. Haack, Susan (27 de julio de 1978). Filosofía de la lógica. Cambridge University Press. pág. 19. ISBN 978-0-521-29329-7.
9. Bostock, David (1997). Lógica intermedia . Oxford: Nueva York: Clarendon Press; Oxford University Press. págs. 4-5, 8-13, 18-19, 22, 27, 29, 191, 194. ISBN 978-0-19-875141-0.
10. Lucas, JR (10 de octubre de 2018). Tratado sobre el tiempo y el espacio. Routledge. pág. 152. ISBN 978-0-429-68517-0.
11. Troelstra, AS; Schwichtenberg, H. (2000). Teoría básica de la prueba. Cambridge Tracts in Theoretical Computer Science (2.ª ed.). Cambridge: Cambridge University Press. pág. 51. doi :10.1017/cbo9781139168717. ISBN 978-0-521-77911-1.
12. "Introducción a la lógica - Capítulo 4". intrologic.stanford.edu . Consultado el 16 de agosto de 2024 .
13. Buss, SR (9 de julio de 1998). Manual de teoría de la prueba. Elsevier. págs. 552–553. ISBN . 978-0-08-053318-6.
14. Ono, Hiroakira (2 de agosto de 2019). Teoría de la demostración y álgebra en lógica. Springer. pág. 5. ISBN 978-981-13-7997-0.
15. Bacon, Andrew (29 de septiembre de 2023). Introducción filosófica a la lógica de orden superior. Taylor & Francis. pág. 424. ISBN 978-1-000-92575-3.
16. Eijck, Jan van (26 de febrero de 1991). Lógica en IA: Taller europeo JELIA '90, Ámsterdam, Países Bajos, 10-14 de septiembre de 1990. Actas. Springer Science & Business Media. pág. 113. ISBN 978-3-540-53686-4.
17. Troelstra, AS; Schwichtenberg, H. (2000). Teoría básica de la prueba. Cambridge Tracts in Theoretical Computer Science (2.ª ed.). Cambridge: Cambridge University Press. pág. 51. doi :10.1017/cbo9781139168717. ISBN 978-0-521-77911-1.
18. Ono, Hiroakira (2 de agosto de 2019). Teoría de la demostración y álgebra en lógica. Springer. pág. 5. ISBN 978-981-13-7997-0.
19. Gabbay, Dov M.; Guenthner, Franz (14 de marzo de 2013). Manual de lógica filosófica. Springer Science & Business Media. pág. 201. ISBN 978-94-017-0458-8.
20. Smullyan, Raymond M. (23 de julio de 2014). Guía para principiantes de lógica matemática. Courier Corporation. págs. 102-103. ISBN 978-0-486-49237-7.
21. Franks, Curtis (2023), "Propositional Logic", en Zalta, Edward N.; Nodelman, Uri (eds.), The Stanford Encyclopedia of Philosophy (edición de otoño de 2023), Metaphysics Research Lab, Stanford University , consultado el 22 de marzo de 2024
22. Mendelsohn, Richard L. (10 de enero de 2005). La filosofía de Gottlob Frege. Prensa de la Universidad de Cambridge. pag. 185.ISBN​ 978-1-139-44403-3.
23. Łukasiewicz, enero (1970). Jan Lukasiewicz: obras seleccionadas. Holanda del Norte. pag. 136.
24. Church, Alonzo (1996). Introducción a la lógica matemática. Princeton University Press. pág. 119. ISBN 978-0-691-02906-1.
25. "Proof Explorer - Página de inicio - Metamath". us.metamath.org . Consultado el 2 de julio de 2024 .
26. Cook, Stephen A.; Reckhow, Robert A. (1979). "La eficiencia relativa de los sistemas de prueba proposicional". The Journal of Symbolic Logic . 44 (1): 39. doi :10.2307/2273702. ISSN  0022-4812.
27. Walicki, Michał (2017). Introducción a la lógica matemática (edición ampliada). Nueva Jersey: World Scientific. pág. 126. ISBN 978-981-4719-95-7.
28. 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: 152. doi :10.1007/BFb0022253. ISBN 978-3-540-49404-1.

Referencias

• Curry, Haskell B.; Robert Feys (1958). Combinatory Logic Vol. I . Vol. 1. Ámsterdam: Holanda Septentrional.
• 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.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 (pp. 464–479). en:
  • van Heijenoort, Jean (1967). From Frege to Gödel: A Source Book in Mathematical Logic, 1879–1931 (3.ª edición, 1976). Cambridge, MA: Harvard University Press. ISBN 0-674-32449-8.
  • En 1927, Hilbert, basado en una conferencia anterior de "fundamentos" de 1925 (pp. 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 otros elementos necesarios de su "teoría de la prueba" 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éase también los comentarios y la refutación de Hermann Weyl (1927) (pp. 480-484), el apéndice de Paul Bernay (1927) a la conferencia de Hilbert (pp. 485-489) y la respuesta de Luitzen Egbertus Jan Brouwer (1927) (pp. 490-495).
• Kleene, Stephen Cole (1952). Introducción a las metamatemáticas (10.ª edición con correcciones de 1971). Ámsterdam, Nueva York: North Holland Publishing Company. ISBN 0-7204-2103-9.
  • Véase en particular el Capítulo IV Sistema Formal (pp. 69-85) donde Kleene presenta los subcapítulos §16 Símbolos formales, §17 Reglas de formación, §18 Variables libres y ligadas (incluyendo 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 proposcional #1-8, Postulados adicionales para el cálculo de predicados #9-12, y Postulados adicionales para la teoría de números #13-21.

Enlaces externos

• Gaifman, Haim. "Un sistema deductivo de tipo Hilbert para lógica oracional, completitud y compacidad" (PDF) .
• Agricultor, WM "Lógica proposicional" (PDF) .Describe (entre otras cosas) un sistema de prueba específico de estilo Hilbert (que está restringido al cálculo proposicional ).