Metateorema - Metatheorem
En lógica , un metateorema es una declaración sobre un sistema formal probado en un metalenguaje . A diferencia de los teoremas probados dentro de un sistema formal dado, un metateorema se prueba dentro de una metateoría y puede hacer referencia a conceptos que están presentes en la metateoría pero no en la teoría del objeto .
Un sistema formal está determinado por un lenguaje formal y un sistema deductivo ( axiomas y reglas de inferencia ). El sistema formal se puede utilizar para probar oraciones particulares del lenguaje formal con ese sistema. Los metateoremas, sin embargo, se prueban externamente al sistema en cuestión, en su metateoría. Las metateorías comunes utilizadas en lógica son la teoría de conjuntos (especialmente en la teoría de modelos ) y la aritmética recursiva primitiva (especialmente en la teoría de la prueba ). En lugar de demostrar que las oraciones particulares son probables, los metateoremas pueden mostrar que cada una de una amplia clase de oraciones puede ser probada, o mostrar que ciertas oraciones no pueden probarse.
Ejemplos
Ejemplos de metateoremas incluyen:
- El teorema de la deducción de la lógica de primer orden dice que una oración de la forma φ → ψ se puede deducir de un conjunto de axiomas A si y sólo si el ψ frase se puede deducir de sistema cuyos axiomas constará de φ y todos los axiomas de la Un .
- El teorema de existencia de clase de la teoría de conjuntos de von Neumann-Bernays-Gödel establece que para cada fórmula cuyos cuantificadores se extienden sólo entre conjuntos, hay una clase que consta de conjuntos que satisfacen la fórmula.
- Pruebas de consistencia de sistemas como la aritmética de Peano .
Ver también
Referencias
- Geoffrey Hunter (1969), Metalogic .
- Alasdair Urquhart (2002), "Metateoría", Un compañero de la lógica filosófica , Dale Jacquette (ed.), P. 307
enlaces externos
- Meta-teorema en la Enciclopedia de Matemáticas
- Barile, Margherita. "Metateorema" . MathWorld .