Un sistema formal es una estructura abstracta y formalización de un sistema axiomático utilizado para inferir teoremas a partir de axiomas mediante un conjunto de reglas de inferencia . [1]
En 1921, David Hilbert propuso utilizar sistemas formales como base del conocimiento en matemáticas . [2]
El término formalismo es a veces un sinónimo aproximado de sistema formal , pero también se refiere a un estilo de notación determinado , por ejemplo, la notación bracket de Paul Dirac .
Un sistema formal tiene lo siguiente: [3] [4] [5]
Se dice que un sistema formal es recursivo (es decir, efectivo) o recursivamente enumerable si el conjunto de axiomas y el conjunto de reglas de inferencia son conjuntos decidibles o semidecidibles , respectivamente.
Un lenguaje formal es un lenguaje que está definido por un sistema formal. Al igual que las lenguas en lingüística , las lenguas formales generalmente tienen dos aspectos:
Por lo general, sólo se considera la sintaxis de un lenguaje formal a través de la noción de gramática formal . Las dos categorías principales de gramática formal son la de gramáticas generativas , que son conjuntos de reglas sobre cómo se pueden escribir cadenas en un idioma, y la de gramáticas analíticas (o gramática reductiva [6] [7] ), que son conjuntos de reglas. para saber cómo se puede analizar una cadena para determinar si es miembro del idioma.
Un sistema deductivo , también llamado aparato deductivo , [8] consta de axiomas (o esquemas de axiomas ) y reglas de inferencia que pueden usarse para derivar teoremas del sistema. [9]
Estos sistemas deductivos conservan cualidades deductivas en las fórmulas que se expresan en el sistema. Generalmente la cualidad que nos preocupa es la verdad y no la falsedad. Sin embargo, en su lugar pueden preservarse otras modalidades , como la justificación o la creencia .
Para mantener su integridad deductiva, un aparato deductivo debe poder definirse sin referencia a ninguna interpretación prevista del lenguaje. El objetivo es garantizar que cada línea de una derivación sea meramente una consecuencia lógica de las líneas que la preceden. No debe haber ningún elemento de interpretación del lenguaje que se involucre con la naturaleza deductiva del sistema.
La consecuencia lógica (o implicación) del sistema por su fundamento lógico es lo que distingue un sistema formal de otros que pueden tener alguna base en un modelo abstracto. A menudo, el sistema formal será la base o incluso se identificará con una teoría o campo más amplio (por ejemplo, la geometría euclidiana ) consistente con el uso en matemáticas modernas, como la teoría de modelos . [ se necesita aclaración ]
Un ejemplo de sistema deductivo serían las reglas de inferencia y los axiomas relativos a la igualdad utilizados en la lógica de primer orden .
Los dos tipos principales de sistemas deductivos son los sistemas de prueba y la semántica formal. [8]
Las pruebas formales son secuencias de fórmulas bien formadas (o WFF para abreviar) que pueden ser un axioma o el producto de aplicar una regla de inferencia sobre WFF anteriores en la secuencia de prueba. El último WFF de la secuencia se reconoce como un teorema .
Una vez dado un sistema formal, se puede definir el conjunto de teoremas que se pueden demostrar dentro del sistema formal. Este conjunto consta de todos los WFF para los que existe una prueba. Por tanto, todos los axiomas se consideran teoremas. A diferencia de la gramática de los WFF, no hay garantía de que exista un procedimiento de decisión para decidir si un WFF determinado es un teorema o no.
El punto de vista de que generar pruebas formales es todo lo que hay en las matemáticas a menudo se denomina formalismo . David Hilbert fundó las metamatemáticas como una disciplina para discutir sistemas formales. Cualquier lenguaje que se utilice para hablar de un sistema formal se llama metalenguaje . El metalenguaje puede ser un lenguaje natural, o puede estar parcialmente formalizado en sí mismo, pero generalmente está menos completamente formalizado que el componente de lenguaje formal del sistema formal bajo examen, que entonces se denomina lenguaje objeto , es decir, el objeto del lenguaje. discusión en cuestión. La noción de teorema recién definida no debe confundirse con los teoremas sobre el sistema formal , que, para evitar confusiones, suelen denominarse metateoremas .
Un sistema lógico es un sistema deductivo (más comúnmente lógica de primer orden ) junto con axiomas no lógicos adicionales . Según la teoría de modelos , a un sistema lógico se le pueden dar interpretaciones que describen si una estructura dada (la correspondencia de fórmulas con un significado particular) satisface una fórmula bien formada. Una estructura que satisface todos los axiomas del sistema formal se conoce como modelo del sistema lógico.
Un sistema lógico es:
Un ejemplo de sistema lógico es la aritmética de Peano . El modelo estándar de la aritmética establece que el dominio del discurso son los números enteros no negativos y da a los símbolos su significado habitual. [10] También existen modelos de aritmética no estándar .
Los primeros sistemas lógicos incluyen la lógica india de Pāṇini , la lógica silogística de Aristóteles, la lógica proposicional del estoicismo y la lógica china de Gongsun Long (c. 325-250 a. C.). En tiempos más recientes, los contribuyentes incluyen a George Boole , Augustus De Morgan y Gottlob Frege . La lógica matemática se desarrolló en la Europa del siglo XIX .
David Hilbert instigó un movimiento formalista llamado programa de Hilbert como una propuesta de solución a la crisis fundamental de las matemáticas , que finalmente fue atenuada por los teoremas de incompletitud de Gödel . [2] El manifiesto QED representó un esfuerzo posterior, hasta ahora infructuoso, de formalización de las matemáticas conocidas.
Medios relacionados con los sistemas formales en Wikimedia Commons
