Metalógica

La metalógica es la metateoría de la lógica . Mientras que la lógica estudia cómo se pueden utilizar los sistemas lógicos para construir argumentos válidos y sólidos , la metalógica estudia las propiedades de los sistemas lógicos. ^[1] La lógica se ocupa de las verdades que se pueden derivar utilizando un sistema lógico; la metalógica se ocupa de las verdades que se pueden derivar sobre los lenguajes y sistemas que se utilizan para expresar verdades. ^[2]

Los objetos básicos del estudio metalógico son los lenguajes formales, los sistemas formales y sus interpretaciones . El estudio de la interpretación de los sistemas formales es la rama de la lógica matemática que se conoce como teoría de modelos , y el estudio de los sistemas deductivos es la rama que se conoce como teoría de la prueba .

Un lenguaje formal es un conjunto organizado de símbolos , cuyos símbolos lo definen con precisión por su forma y lugar. Por lo tanto, un lenguaje de este tipo puede definirse sin referencia a los significados de sus expresiones; puede existir antes de que se le asigne interpretación alguna , es decir, antes de que tenga significado alguno. La lógica de primer orden se expresa en algún lenguaje formal. Una gramática formal determina qué símbolos y conjuntos de símbolos son fórmulas en un lenguaje formal.

Un lenguaje formal puede definirse formalmente como un conjunto A de cadenas (secuencias finitas) en un alfabeto fijo α. Algunos autores, incluido Rudolf Carnap , definen el lenguaje como el par ordenado <α, A >. ^[3] Carnap también requiere que cada elemento de α debe aparecer en al menos una cadena en A .

Las reglas de formación (también llamadas gramática formal ) son una descripción precisa de las fórmulas bien formadas de un lenguaje formal. Son sinónimos del conjunto de cadenas sobre el alfabeto del lenguaje formal que constituyen las fórmulas bien formadas. Sin embargo, no describe su semántica (es decir, lo que significan).

Un sistema formal (también llamado cálculo lógico o sistema lógico ) consiste en un lenguaje formal junto con un aparato deductivo (también llamado sistema deductivo ). El aparato deductivo puede consistir en un conjunto de reglas de transformación (también llamadas reglas de inferencia ) o un conjunto de axiomas , o tener ambos. Un sistema formal se utiliza para derivar una expresión a partir de una o más expresiones diferentes.

Un sistema formal puede definirse formalmente como una terna ordenada <α, , d>, donde d es la relación de derivabilidad directa. Esta relación se entiende en un sentido amplio , de modo que las oraciones primitivas del sistema formal se toman como directamente derivables del conjunto vacío de oraciones. La derivabilidad directa es una relación entre una oración y un conjunto finito, posiblemente vacío, de oraciones. Los axiomas se eligen de modo que cada miembro de primer lugar de d sea un miembro de y cada miembro de segundo lugar sea un subconjunto finito de . ${\displaystyle {\mathcal {I}}}$${\displaystyle {\mathcal {D}}}$${\displaystyle {\mathcal {D}}}$${\displaystyle {\mathcal {D}}}$${\displaystyle {\mathcal {I}}}$${\displaystyle {\mathcal {I}}}$

Un sistema formal también puede definirse únicamente con la relación d. Por lo tanto, se puede omitir α en las definiciones de lenguaje formal interpretado y sistema formal interpretado . Sin embargo, este método puede ser más difícil de entender y utilizar. ^[3]${\displaystyle {\mathcal {D}}}$${\displaystyle {\mathcal {I}}}$

Una demostración formal es una secuencia de fórmulas bien formadas de un lenguaje formal, la última de las cuales es un teorema de un sistema formal. El teorema es una consecuencia sintáctica de todas las fórmulas bien formadas que lo preceden en el sistema de demostración. Para que una fórmula bien formada sea considerada parte de una demostración, debe resultar de la aplicación de una regla del aparato deductivo de algún sistema formal a las fórmulas bien formadas anteriores en la secuencia de demostración.

La interpretación de un sistema formal es la asignación de significados a los símbolos y valores de verdad a las oraciones del sistema formal. El estudio de las interpretaciones se denomina semántica formal . Dar una interpretación es sinónimo de construir un modelo .

En metalógica, los lenguajes formales a veces se denominan lenguajes objeto . El lenguaje utilizado para hacer afirmaciones sobre un lenguaje objeto se denomina metalenguaje . Esta distinción es una diferencia clave entre la lógica y la metalógica. Mientras que la lógica se ocupa de las pruebas en un sistema formal , expresadas en algún lenguaje formal, la metalógica se ocupa de las pruebas sobre un sistema formal que se expresan en un metalenguaje sobre algún lenguaje objeto.

En metalógica, la "sintaxis" se relaciona con los lenguajes formales o los sistemas formales sin tener en cuenta ninguna interpretación de los mismos, mientras que la "semántica" se relaciona con las interpretaciones de los lenguajes formales. El término "sintáctico" tiene un alcance ligeramente más amplio que el de "teórico de la demostración", ya que puede aplicarse a propiedades de los lenguajes formales sin ningún sistema deductivo, así como a los sistemas formales. "Semántico" es sinónimo de "teórico de modelos".

En metalógica, las palabras «uso» y «mención», tanto en su forma nominal como verbal, adquieren un sentido técnico para identificar una distinción importante. ^[2] La distinción entre uso y mención (a veces denominada distinción entre palabras como palabras ) es la distinción entre usar una palabra (o frase) y mencionarla . Por lo general, se indica que una expresión se menciona en lugar de usarse encerrándola entre comillas, imprimiéndola en cursiva o colocando la expresión sola en una línea. El encerramiento entre comillas de una expresión nos da el nombre de una expresión, por ejemplo:

'Metalogic' es el nombre de este artículo.

Este artículo trata sobre metalógica.

La distinción entre tipo y símbolo es una distinción en metalógica que separa un concepto abstracto de los objetos que son instancias particulares del concepto. Por ejemplo, la bicicleta particular que está en su garaje es un símbolo del tipo de cosa conocida como "la bicicleta". Mientras que la bicicleta que está en su garaje está en un lugar particular en un momento particular, eso no es cierto en el caso de "la bicicleta" como se usa en la oración: " La bicicleta se ha vuelto más popular recientemente". Esta distinción se usa para aclarar el significado de los símbolos de los lenguajes formales .

Las preguntas metalógicas se han planteado desde la época de Aristóteles . ^[4] Sin embargo, fue solo con el surgimiento de los lenguajes formales a fines del siglo XIX y principios del XX que las investigaciones sobre los fundamentos de la lógica comenzaron a florecer. En 1904, David Hilbert observó que al investigar los fundamentos de las matemáticas se presuponen nociones lógicas y, por lo tanto, se requería una explicación simultánea de los principios metalógicos y metamatemáticos . Hoy, metalógica y metamatemática son en gran medida sinónimos entre sí, y ambas han sido subsumidas sustancialmente por la lógica matemática en el ámbito académico. Un posible modelo alternativo, menos matemático, se puede encontrar en los escritos de Charles Sanders Peirce y otros semióticos .

Los resultados en metalógica consisten en cosas tales como pruebas formales que demuestran la consistencia , completitud y decidibilidad de sistemas formales particulares .

Los principales resultados en metalógica incluyen:

• Prueba de la incontabilidad del conjunto potencia de los números naturales ( Teorema de Cantor 1891)
• Teorema de Löwenheim-Skolem ( Leopold Löwenheim 1915 y Thoralf Skolem 1919)
• Prueba de la consistencia de la lógica proposicional veritativo-funcional ( Emil Post 1920)
• Prueba de la completitud semántica de la lógica proposicional veritativo-funcional ( Paul Bernays 1918), ^[5] (Emil Post 1920) ^[2]
• Prueba de la completitud sintáctica de la lógica proposicional veritativo-funcional (Emil Post 1920) ^[2]
• Prueba de la decidibilidad de la lógica proposicional veritativo-funcional (Emil Post 1920) ^[2]
• Prueba de la consistencia de la lógica de predicados monádicos de primer orden ( Leopold Löwenheim 1915)
• Prueba de la completitud semántica de la lógica de predicados monádicos de primer orden (Leopold Löwenheim 1915)
• Prueba de la decidibilidad de la lógica de predicados monádicos de primer orden (Leopold Löwenheim 1915)
• Prueba de la consistencia de la lógica de predicados de primer orden ( David Hilbert y Wilhelm Ackermann 1928)
• Prueba de la completitud semántica de la lógica de predicados de primer orden ( teorema de completitud de Gödel, 1930)
• Demostración del teorema de eliminación de cortes para el cálculo secuencial ( Gentzen 's Hauptsatz 1934)
• Prueba de la indecidibilidad de la lógica de predicados de primer orden ( teorema de Church de 1936)
• Primer teorema de incompletitud de Gödel 1931
• Segundo teorema de incompletitud de Gödel 1931
• Teorema de indefinibilidad de Tarski (Gödel y Tarski en la década de 1930)

• Programación metalógica
• Metamatemáticas

• Medios relacionados con Metalogic en Wikimedia Commons
• Dragalin, AG (2001) [1994], "Meta-lógica", Enciclopedia de Matemáticas , EMS Press