Un sistema formal es una estructura abstracta y formalización de un sistema axiomático utilizado para deducir , mediante reglas de inferencia , 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 determinado de notación , por ejemplo, la notación bra-ket 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 conjuntos semidecidibles , respectivamente.
Un lenguaje formal es un lenguaje que se define mediante un sistema formal. Al igual que los lenguajes en lingüística , los lenguajes formales generalmente tienen dos aspectos:
Por lo general, solo 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 las gramáticas generativas , que son conjuntos de reglas sobre cómo se pueden escribir las cadenas en un lenguaje, y las gramáticas analíticas (o gramática reductiva [6] [7] ), que son conjuntos de reglas sobre cómo se puede analizar una cadena para determinar si es un miembro del lenguaje.
Un sistema deductivo , también llamado aparato deductivo , [8] consiste en los axiomas (o esquemas axiomáticos ) 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. Por lo general, la cualidad que nos interesa es la verdad en oposición a la falsedad. Sin embargo, otras modalidades , como la justificación o la creencia, pueden conservarse en su lugar.
Para mantener su integridad deductiva, un aparato deductivo debe ser definible sin referencia a ninguna interpretación intencionada del lenguaje. El objetivo es asegurar 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 interfiera con la naturaleza deductiva del sistema.
La consecuencia lógica (o implicación) del sistema por su fundamento lógico es lo que distingue a 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 ) coherente con el uso en las matemáticas modernas, como la teoría de modelos . [ Aclaración necesaria ]
Un ejemplo de un sistema deductivo serían las reglas de inferencia y los axiomas sobre 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 demostraciones formales son secuencias de fórmulas bien formadas (o WFF, por sus siglas en inglés) que pueden ser un axioma o ser el producto de aplicar una regla de inferencia sobre las WFF anteriores en la secuencia de demostraciones. La última WFF en la secuencia se reconoce como un teorema .
Una vez que se da un sistema formal, se puede definir el conjunto de teoremas que se pueden demostrar dentro del sistema formal. Este conjunto consta de todas las FBF para las que existe una demostración. Por lo tanto, todos los axiomas se consideran teoremas. A diferencia de la gramática para las FBF, no hay garantía de que exista un procedimiento de decisión para decidir si una FBF dada es un teorema o no.
El punto de vista de que la generación de pruebas formales es todo lo que hay en matemáticas se suele llamar formalismo . David Hilbert fundó la metamatemática como disciplina para discutir sistemas formales. Cualquier lenguaje que se utilice para hablar sobre 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 formalizado por completo que el componente de lenguaje formal del sistema formal en examen, que entonces se llama lenguaje objeto , es decir, el objeto de la discusión en cuestión. La noción de teorema que se acaba de definir no debe confundirse con los teoremas sobre el sistema formal , que, para evitar confusiones, suelen llamarse 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 describan si una estructura dada (la aplicación de fórmulas a 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 un sistema lógico es la aritmética de Peano . El modelo estándar de la aritmética establece que el dominio del discurso sean los números enteros no negativos y otorga a los símbolos su significado habitual. [10] También existen modelos no estándar de aritmética .
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, entre los contribuyentes se incluyen 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 el programa de Hilbert como una solución propuesta a la crisis fundacional de las matemáticas , que finalmente fue atenuada por los teoremas de incompletitud de Gödel . [2] El manifiesto QED representó un esfuerzo posterior, aún infructuoso, de formalización de las matemáticas conocidas.
Medios relacionados con Sistemas formales en Wikimedia Commons
