Sistema formal

Un sistema formal o sistema lógico es un sistema abstracto compuesto por un lenguaje formal, axiomas, reglas de inferencia y a veces una semántica formal, que se utiliza para deducir o demostrar teoremas y dar una definición rigurosa del concepto de demostración. Un sistema formal es una formalización rigurosa y completa del concepto de sistema axiomático, los cuales se pueden expresar en lenguaje formal o en lenguaje natural formalizado. Al crear un sistema formal se pretende capturar y abstraer la esencia de determinadas características del mundo real, en un modelo conceptual expresado en un determinado lenguaje formal. Algunos de los sistemas formales más conocidos son la lógica proposicional, la lógica de primer orden y la lógica modal.

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.

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 , 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.

Los sistemas formales también han encontrado aplicación dentro de la informática, la teoría de la información y la estadística.

Componentes 
Un sistema formal está compuesto por:

 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.

Tipos de sistemas formales 

Existe un debate sobre si es correcto hablar de una lógica, o de varias lógicas, pero en el  se han desarrollado no uno, sino varios sistemas formales diferentes, que capturan y formalizan distintas partes del lenguaje natural.

Lógicas clásicas

Lógicas no clásicas

Lógicas modales

Metalógica

Véase también 

 Lógica matemática
 Lenguaje formalizado
 Noción primitiva
 Teoría (lógica)

Referencias

Bibliografía 

 Raymond M. Smullyan, 1961. Theory of Formal Systems: Annals of Mathematics Studies, Princeton University Press (April 1, 1961) 156 pag. ISBN 069108047X
 S. C. Kleene, 1967. Mathematical Logic Reprinted by Dover, 2002. ISBN 0486425339
Douglas Hofstadter, 1979. Gödel, Escher, Bach: An Eternal Golden Braid. 777 pag. ISBN 978-0465026562.

Enlaces externos 

 Formal system, definición en la Enciclopedia Británica, 2007.
 Christer Blomqvist, an introduction to formal systems, página web 1997.
 What is a Formal System?: Algunas citas de `Artificial Intelligence: The Very Idea' (1985) de John Haugeland, pp. 48–64.
 Heinrich Herre Formal Language and systems, 1997.
 Peter Suber, Formal Systems and Machines: An Isomorphism , 1997.

Lógica matemática
Filosofía de la matemática
Métodos formales
Sistema formal
Sintaxis (lógica)
Lenguajes formales
India en el siglo IV a. C.