La metalógica es el estudio de la metateoría de la lógica . Mientras que la lógica estudia cómo se pueden usar 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 refiere a las verdades que pueden derivarse utilizando un sistema lógico; la metalógica se refiere a las verdades que pueden derivarse de los lenguajes y sistemas que se utilizan para expresar verdades. [2]
Los objetos básicos del estudio metalológico son los lenguajes formales, los sistemas formales y sus interpretaciones . El estudio de la interpretación de sistemas formales es la rama de la lógica matemática que se conoce como teoría de modelos , y el estudio de sistemas deductivos es la rama que se conoce como teoría de la prueba .
Descripción general
Lenguaje formal
Un lenguaje formal es un conjunto organizado de símbolos , cuyos símbolos lo definen con precisión por su forma y lugar. Por tanto, un lenguaje así puede definirse sin referencia a los significados de sus expresiones; puede existir antes de que se le asigne cualquier interpretación, es decir, antes de que tenga algún significado. 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 se puede definir 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 ocurrir en al menos una cadena en A .
Reglas de formación
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 fórmulas bien formadas. Sin embargo, no describe su semántica (es decir, lo que significan).
Sistemas formales
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. Se utiliza un sistema formal para derivar una expresión de una o más expresiones.
Un sistema formal se puede definir formalmente como un triple ordenado <α,,d>, donde d es la relación de derivabilidad directa. Esta relación se entiende en un sentido comprensivo , 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 de oraciones finito, posiblemente vacío. Los axiomas se eligen de tal manera que cada miembro de primer lugar ded es miembro de y cada miembro del segundo lugar es un subconjunto finito de .
Un sistema formal también se puede definir con solo la relaciónD. Por lo tanto se puede omitiry α en las definiciones de lenguaje formal interpretado y sistema formal interpretado . Sin embargo, este método puede resultar más difícil de comprender y utilizar. [3]
Pruebas formales
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 prueba. Para que una fórmula bien formada califique como parte de una demostración, debe resultar de aplicar una regla del aparato deductivo de algún sistema formal a las fórmulas bien formadas anteriores en la secuencia de la prueba.
Interpretaciones
Una 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 .
Distinciones importantes
Metalenguaje-lenguaje de objetos
En metalógica, los lenguajes formales a veces se denominan lenguajes objeto . El lenguaje utilizado para hacer declaraciones sobre un lenguaje objeto se llama 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.
Sintaxis-semántica
En metalógica, 'sintaxis' tiene que ver con lenguajes formales o sistemas formales sin tener en cuenta ninguna interpretación de ellos, mientras que, 'semántica' tiene que ver con interpretaciones de lenguajes formales. El término "sintáctico" tiene un alcance ligeramente más amplio que el de "teoría de la prueba", ya que puede aplicarse a las propiedades de los lenguajes formales sin ningún sistema deductivo, así como a los sistemas formales. "Semántico" es sinónimo de "modelo-teórico".
Usar – mencionar
En metalógica, las palabras 'usar' y 'mencionar', tanto en su forma nominal como verbal, adquieren un sentido técnico para identificar una distinción importante. [2] La distinción uso-mención (a veces denominada distinción de 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 usarla encerrándola entre comillas, imprimiéndola en cursiva o colocando la expresión por sí misma en una línea. El encerrar entre comillas 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 la metalógica.
Tipo – token
La distinción tipo-token es una distinción en la metalógica, que separa un concepto abstracto de los objetos que son instancias particulares del concepto. Por ejemplo, la bicicleta en particular en su garaje es un símbolo del tipo de cosa conocida como "La bicicleta". Considerando que, la bicicleta en su garaje está en un lugar particular en un momento particular, eso no es cierto para "la bicicleta" como se usa en la oración: " La bicicleta se ha vuelto más popular recientemente". Esta distinción se utiliza para aclarar el significado de los símbolos de los lenguajes formales .
Historia
Desde la época de Aristóteles se han planteado cuestiones metalogísticas . 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 las nociones lógicas y, por lo tanto, se requiere una explicación simultánea de los principios metalógicos y metamatemáticos . Hoy en día, la metalógica y la metamatemática son en gran medida sinónimos entre sí, y ambas han sido sustancialmente subsumidas por la lógica matemática en la academia. Un posible modelo alternativo menos matemático se puede encontrar en los escritos de Charles Sanders Peirce y otros semióticos .
Resultados
Los resultados en la metalógica consisten en cosas tales como pruebas formales que demuestran la consistencia , integridad y decidibilidad de sistemas formales particulares .
Los principales resultados en metalógica incluyen:
- Prueba de la incontabilidad del conjunto de potencias 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 funcional de la verdad ( Emil Post 1920)
- Prueba de la integridad semántica de la lógica proposicional funcional de la verdad ( Paul Bernays 1918), [4] (Emil Post 1920) [2]
- Prueba de la integridad sintáctica de la lógica proposicional funcional de la verdad (Emil Post 1920) [2]
- Prueba de la decidibilidad de la lógica proposicional funcional de la verdad (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)
- La prueba de la teorema de eliminación de corte 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 1936)
- Primer teorema de incompletitud de Gödel 1931
- Segundo teorema de incompletitud de Gödel 1931
- El teorema de indefinibilidad de Tarski (Gödel y Tarski en la década de 1930)
Ver también
- Programación metalógica
- Metamatemáticas
Referencias
- ^ Harry Gensler, Introducción a la lógica , Routledge, 2001, p. 336.
- ^ a b c d e Hunter, Geoffrey , Metalogic: An Introduction to the Metatheory of Standard-Order Logic , University of California Press, 1973
- ↑ a b Rudolf Carnap (1958) Introducción a la lógica simbólica y sus aplicaciones , p. 102.
- ^ Hao Wang, Reflexiones sobre Kurt Gödel
enlaces externos
- Medios relacionados con la Metalogic en Wikimedia Commons
- Dragalin, AG (2001) [1994], "Meta-lógica" , Enciclopedia de Matemáticas , EMS Press