Este artículo necesita la atención de un experto en matemáticas . Consulte la página de discusión para obtener más detalles. WikiProject Mathematics puede ayudar a reclutar a un experto. ( Marzo de 2011 )
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 de cambio de contexto. Por lo tanto, si uno está interesado solo en la derivabilidad de tautologías , no en juicios hipotéticos, entonces uno puede formalizar el sistema de Hilbert de tal manera que sus reglas de inferencia contengan solo juicios de una forma bastante simple. No se puede hacer lo mismo con los otros dos sistemas de deducciones: [ cita requerida ] como el contexto cambia en algunas de sus reglas de inferencia, no se pueden formalizar para evitar juicios hipotéticos, ni siquiera si queremos usarlos solo para probar la derivabilidad de tautologías.
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 están destinadas a 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 solo axiomas lógicos y elementos de . Por lo tanto, informalmente, significa que es demostrable asumiendo todas las fórmulas en .
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 que se obtienen al sustituir todas las fórmulas de alguna forma en un patrón específico. El conjunto de axiomas lógicos incluye no solo los axiomas generados a partir de este patrón, sino también cualquier generalización de uno de esos axiomas. Se obtiene una generalización de una fórmula prefijando cero o más cuantificadores universales en la fórmula; por ejemplo, es una generalización de .
Axiomas lógicos
Hay varias axiomatizaciones variantes de la lógica de predicados, ya que para cualquier lógica hay libertad para elegir axiomas y reglas que caracterizan esa lógica. 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 utilizan sólo los conectivos y ya 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.
Los primeros cuatro esquemas de axiomas lógicos permiten (junto con modus ponens) la manipulación de conectivos lógicos.
P1.
P2.
P3.
P4.
El axioma P1 es redundante, como se desprende 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 agregando en su lugar el axioma P4m o definiendo como .
P4m.
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.
P5i.
Tenga en cuenta que estos son esquemas de axiomas, que representan un número infinito de 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 ésta que se extiende sobre las fórmulas se denomina 'variable esquemática'.
Con una segunda regla de sustitución uniforme (EE. UU.), Podemos cambiar cada uno de estos esquemas de axioma 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 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 sustitutiva usa variables proposicionales que hacen el mismo trabajo al expresar la idea de una variable que va sobre fórmulas con una regla que usa sustitución.
NOSOTROS. Sea una fórmula con una o más instancias de la variable proposicional y sea otra fórmula. Luego de , inferir . [ dudoso - discutir ]
Los siguientes tres esquemas de axiomas lógicos proporcionan formas de agregar, manipular y eliminar cuantificadores universales.
Q5. donde t puede ser sustituido por x en
Q6.
Q7. donde x no está libre en .
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 usando una regla adicional de generalización (ver la sección sobre Metateoremas), en cuyo caso las reglas Q6 y Q7 son redundantes. [ dudoso - discutir ]
Se requiere que los esquemas de axiomas finales trabajen con fórmulas que involucren el símbolo de igualdad.
I8. para cada variable x .
I9.
Extensiones conservadoras
Es común incluir en un sistema de deducción al estilo de Hilbert solo axiomas para la implicación y la 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 denominan conservativas porque si una fórmula φ que involucra nuevas conectivas 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 al estilo de Hilbert se parecerá más a un sistema de deducción natural .
Cuantificación existencial
Introducción
Eliminación
donde no es una variable libre de .
Conjunción y disyunción
Introducción y eliminación de conjunciones
Introducción:
eliminación izquierda:
derecho de eliminación:
Introducción y eliminación de disyunciones
introducción a la izquierda:
introducción a la derecha:
eliminación:
Metateoremas
Debido a que los sistemas al estilo 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 usa las nuevas reglas de deducción se puede convertir en una deducción usando solo la deducción original. reglas.
Algunos metateoremas comunes de esta forma son:
El teorema de la deducción : si y solo si .
si y solo si y .
Contraposición: Si entonces .
Generalización : Si y x no ocurre libre en cualquier fórmula de continuación .
Algunos teoremas útiles y sus demostraciones
A continuación se presentan varios teoremas en lógica proposicional, junto con sus demostraciones (o enlaces a estas demostraciones en otros artículos). Tenga en cuenta que dado que (P1) en sí mismo 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 .
(L1) - prueba:
(1) (instancia de (P3))
(2) (instancia de (P1))
(3) (de (2) y (1) por modus ponens )
(4) (instancia de (HS1))
(5) (de (3) y (4) por modus ponens)
(6) (instancia de (P2))
(7) (de (6) y (5) por modus ponens)
Los dos teoremas siguientes se conocen juntos como doble negación :
(DN1)
(DN2)
Ver pruebas .
(L2) - para esta prueba usamos el método del metateorema del silogismo hipotético como una forma abreviada de varios pasos de prueba:
(1) (instancia de (P3))
(2) (instancia de (HS1))
(3) (de (1) y (2) usando el metateorema del silogismo hipotético)
(4) (instancia de (P3))
(5) (de (3) y (4) usando modus ponens)
(6) (instancia de (P2))
(7) (instancia de (P2))
(8) (de (6) y (7) usando modus ponens)
(9) (de (8) y (5) usando modus ponens)
(HS2) - una forma alternativa del silogismo hipotético . prueba:
(1) (instancia de (HS1))
(2) (instancia de (L2))
(3) (de (1) y (2) por modus ponens)
(TR1) - Transposición, ver prueba (la otra dirección de transposición es (P4)).
(TR2) - otra forma de transposición; prueba:
(1) (instancia de (TR1))
(2) (instancia de (DN1))
(3) (instancia de (HS1))
(4) (de (2) y (3) por modus ponens)
(5) (de (1) y (4) usando el metateorema del silogismo hipotético)
(L3) - prueba:
(1) (instancia de (P2))
(2) (instancia de (P4))
(3) (de (1) y (2) usando el metateorema del silogismo hipotético)
(4) (instancia de (P3))
(5) (de (3) y (4) usando modos ponens)
(6) (instancia de (P4))
(7) (de (5) y (6) usando el metateorema del silogismo hipotético)
(8) (instancia de (P1))
(9) (instancia de (L1))
(10) (de (8) y (9) usando modos ponens)
(11) (de (7) y (10) utilizando el metateorema del silogismo hipotético)
Axiomatizaciones alternativas
Más información: Lista de sistemas lógicos
El axioma 3 anterior se le atribuye a Łukasiewicz . [2] El sistema original de Frege tenía axiomas P2 y P3 pero otros cuatro axiomas en lugar del axioma P4 (ver 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 base lógica combinatoria I , K y S con el operador de aplicación. Las demostraciones en el sistema de Hilbert corresponden a los términos combinatorios en lógica combinatoria. Véase también la correspondencia de Curry-Howard .
Ver también
Lista de sistemas Hilbert
Deducción natural
Notas
↑ a b Máté y Ruzsa 1997: 129
^ A. Tarski, Lógica, semántica, metamatemáticas, Oxford, 1956
Referencias
Curry, Haskell B .; Robert Feys (1958). Lógica combinatoria Vol. Yo . 1 . Amsterdam: 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.CS1 maint: posdata ( enlace )
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: telecabina.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). From Frege to Gödel: A Source Book in Mathematical Logic, 1879-1931 (tercera edición, 1976 ed.). Cambridge MA: Harvard University Press. ISBN 0-674-32449-8.
Hilbert de 1927, basado 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 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 del 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 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 corrección de 1971 ed.). Amsterdam NY: North Holland Publishing Company. ISBN 0-7204-2103-9.
Ver en particular el Capítulo IV Sistema formal (págs. 69-85) donde Kleene presenta 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 éstos 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 de tipo Hilbert para la lógica de las oraciones, la integridad y la 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 ).
vtmiTemas principales en Fundamentos de las matemáticas
Lógica matemática
Axiomas de Peano
Inducción matemática
Sistema formal
Sistema axiomático
Sistema de Hilbert
Deducción natural
Prueba matemática
Teoría de modelos
Constructivismo matemático
Lógica modal
Lista de temas de lógica matemática
Teoría de conjuntos
Colocar
Teoría de conjuntos ingenua
Teoría de conjuntos axiomáticos
Teoría de conjuntos de Zermelo
Teoría de conjuntos de Zermelo-Fraenkel
Teoría de conjuntos constructiva
Teoría descriptiva de conjuntos
Determinación
La paradoja de Russell
Lista de temas de teoría de conjuntos
Teoría de tipos
Axioma de reducibilidad
Teoría de tipos simples
Teoría de tipos dependientes
Teoría de tipos intuicionistas
Teoría del tipo de homotopía
Fundaciones univalentes
La paradoja de Girard
Teoría de categorías
Categoría
Teoría Topos
Categoría de conjuntos
Teoría de categorías superiores
∞-grupoide
Teoría ∞-topos
Estructuralismo matemático
Glosario de teoría de categorías
Lista de temas de teoría de categorías
Categorías :
Teoría de la prueba
Cálculos lógicos
Demostración automatizada de teoremas
Categorías ocultas:
Artículos que necesitan la atención de un experto desde marzo de 2011
Todos los artículos que necesitan la atención de un experto
Artículos de matemáticas que necesitan la atención de un experto
Artículos que carecen de citas en el texto de octubre de 2019
Todos los artículos que carecen de citas en el texto.
Artículos con múltiples problemas de mantenimiento
Todos los artículos con declaraciones sin fuente
Artículos con declaraciones sin fuente de marzo de 2014
Todas las disputas de precisión
Artículos con declaraciones controvertidas de diciembre de 2018