En la teoría de la demostración, las demostraciones formales se pueden expresar en el lenguaje de los sistemas formales, consistentes en axiomas y reglas de inferencia. Los teoremas pueden ser obtenidos por medio de demostraciones formales. Este punto de vista de las matemáticas ha sido denominado formalista; aunque en muchas ocasiones este término conlleva una acepción peyorativa. En ese sentido, David Hilbert creó la metamatemática para estudiar los sistemas formales, entendiendo que el lenguaje utilizado para ello, denominado metalenguaje era distinto del lenguaje del sistema formal que se pretendía estudiar, al que se llama lenguaje objeto.
Un sistema así es la reducción de un lenguaje formalizado a meros símbolos, lenguaje formalizado y simbolizado sin contenido material alguno; un lenguaje reducido a mera forma que se expresa mediante fórmulas que reflejan las relaciones sintácticas entre los símbolos y las reglas de formación y transformación que permiten construir las fórmulas del sistema y pasar de una fórmula a otra.[1]
Una teoría axiomática es un conjunto de fórmulas en un determinado lenguaje formal y todas las fórmulas deducibles de dichas expresiones mediante las reglas de inferencia posibles en dicho sistema formal. El objetivo de las teorías axiomáticas es construir sistemas formales que representen las características esenciales de ramas enteras de las matemáticas. Si se selecciona un conjunto más amplio o menos amplio de axiomas el conjunto de teoremas deducibles cambian. El interés de la teoría de modelos es que en un modelo en que satisfagan los axiomas de determinada teoría también se satisfacen los teoremas deducibles de dicha teoría. Es decir, si un teorema es deducible en una cierta teoría, entonces ese teorema es universalmente válido en todos los modelos que satisfacen los axiomas. Esto es interesante porque en principio la clase de modelos que satisface una cierta teoría es difícil de conocer, ya que las teorías matemáticas interesantes en general admiten toda clase infinita de modelos no isomorfos, por lo que su clasificación en general resulta difícilmente abordable si no existe un sistema formal y un conjunto de axiomas que caracterice los diferentes tipos de modelos.
En el siglo XX, Hilbert y otros sostuvieron que la matemática es un sistema formal. Pero en 1931, Kurt Gödel demostró que ningún sistema formal con suficiente poder expresivo para capturar la aritmética de Peano puede ser a la vez consistente y completo. El teorema de la incompletitud de Gödel, junto con la demostración de Alonzo Church de que la matemática tampoco es decidible, terminó con el programa de Hilbert. Sin embargo, a pesar de sus limitaciones, el enfoque sigue siendo ampliamente usado, básicamente porque no se ha encontrado ninguna alternativa mejor al enfoque formalista de Hilbert y la pretensión de trabajar en el seno de teorías matemáticas explícitamente axiomatizadas, aun con sus limitaciones.
Un conjunto de símbolos primitivos (el alfabeto o vocabulario).
Un conjunto de reglas de formación (la gramática) que nos dice cómo construir fórmulas bien formadas a partir de los símbolos primitivos. El lenguaje del sistema será el conjunto de todas esas fórmulas.
Un conjunto de axiomas o esquemas de axiomas. Cada axioma debe ser una fórmula bien formada.
Un sistema deductivo o conjunto de reglas de inferencia. Estas reglas determinan qué fórmulas se pueden inferir de qué fórmulas. Por ejemplo, una regla de inferencia clásica es el modus ponens, según el cual, dada una fórmula A, y otra fórmula A→B, la regla nos permite inferir B.
Estos cuatro elementos completan la parte sintáctica de los sistemas formales. Sin embargo, todavía no se ha dado ningún significado a los símbolos discutidos, y de hecho, un sistema formal se puede definir sin tener que hacerlo. Tal tarea corresponde al campo llamado semántica formal, que se ocupa de introducir un quinto elemento:
Una interpretación formal. En los lenguajes naturales, una misma palabra puede significar diversas cosas dependiendo de la interpretación que se le dé. Por ejemplo, en el idioma español, la palabra «banco» puede significar un edificio o un asiento, mientras que en otros idiomas puede significar algo completamente distinto o nada en absoluto, y dependiendo de la interpretación, variará también el valor de verdad de la oración «el banco está cerca». Las interpretaciones formales asignan significados inequívocos a los símbolos primitivos, y valores de verdad a las fórmulas.
Para entender mejor estos elementos, definimos un sistema formal minimalista llamado M.
El sistema M tiene un alfabeto con un único símbolo: a
Las fórmulas bien formadas de M son aquellas que se construyen con las siguientes reglas de formación:
a es una fórmula
Si φ es una fórmula, entonces φa también es una fórmula
Nada más es una fórmula
Por lo tanto, el lenguaje de M consta de las siguientes fórmulas: a, aa, aaa, aaaa, aaaaa, ...
M tiene un único axioma: a
M tiene una única regla de inferencia: de φ se puede inferir φa
Los teoremas son aquellas fórmulas que se deducen de los axiomas a través de las reglas de inferencia en un número finito de pasos. En este caso, los teoremas de M serán: aa, aaa, aaaa, aaaaa, ...
Es decir todas las fórmulas bien formadas, excepto a.
Existe un debate sobre si es correcto hablar de una lógica, o de varias lógicas, pero en el siglo XX se han desarrollado no uno, sino varios sistemas formales diferentes, que capturan y formalizan distintas partes del lenguaje natural.
Una lógica no clásica o lógica alternativa es un sistema formal que difiere de manera significativa de las lógicas clásicas. Hay varias formas de hacerlo, incluyendo a modo de extensiones, desviaciones, y variaciones, por ejemplo, rechazando uno o varios de los principios de la lógica clásica. El objetivo de estas desviaciones es para hacer posible construir distintos modelos de consecuencia lógica y verdad lógica.
La lógica filosófica, especialmente en la ciencia computacional teórica, se usa para abarcar y centrarse en las lógicas no clásicas, a pesar de que el término tiene otros significados también.[4]
Lógica no monotónica: Una lógica no monotónica es una lógica donde, al agregar una fórmula a una teoría cualquiera, es posible que el conjunto de consecuencias de esa teoría se reduzca.
Lógica intuicionista: Enfatiza las pruebas, en vez de la verdad, a lo largo de las transformaciones de las proposiciones.
Una lógica modal es un sistema formal que intenta capturar el comportamiento deductivo de algún grupo de operadores modales.[5] Los operadores modales son expresiones que califican la verdad de los juicios.[5] Por ejemplo, en el juicio «es necesario que 2 + 2 = 4», la expresión «es necesario que» es un operador modal que califica de necesaria a la verdad del juicio «2 + 2 = 4». De manera análoga, la expresión «siempre» califica a un juicio verdadero como verdadero en cualquier momento, es decir, siempre. No es lo mismo decir «está lloviendo» que decir «siempre está lloviendo».
En un sentido más restringido, sin embargo, una lógica modal es un sistema formal que intenta capturar el comportamiento deductivo de las expresiones «es necesario que» y «es posible que».[5] Este artículo trata exclusivamente sobre lógicas modales en este sentido restringido. Las lógicas modales pertenecen al grupo de las llamadas «extensiones de la lógica clásica» o «lógicas extendidas» entre las cuales se incluyen además la lógica deóntica, la lógica temporal, la lógica epistémica y la lógica doxástica.
