# Metalógica

La metalógica es la rama de la lógica que estudia las propiedades y los componentes de los sistemas formales. Las propiedades más importantes que se pueden demostrar de los sistemas formales son la consistencia, decidibilidad y completitud. Ejemplos de teoremas metalógicos importantes son los teoremas de incompletitud de Gödel, el teorema de completitud de Gödel y el teorema de Löwenheim-Skolem. Otra propiedad es la compacidad.

## Propiedades metateóricas

Mientras la lógica matemática se encarga, entre otras cosas, de construir sistemas lógicos, la metalógica se ocupa de estudiar las propiedades de dichos sistemas. Las propiedades más importantes que se pueden demostrar de los sistemas lógicos son:

### Consistencia

En metalógica, la consistencia o consistencia lógica es la propiedad que tienen los sistemas formales cuando no es posible deducir una contradicción dentro del sistema. Es decir, dado un lenguaje formal y un aparato deductivo (axiomas y reglas de inferencia), no es posible deducir una fórmula y su negación. La existencia de un modelo implica que una teoría lógica es consistente.
${\mathcal {A}}\vdash p$
${\mathcal {A}}\vdash \neg p$

### Decidibilidad

En metalógica, la decidibilidad es una propiedad de los sistemas formales cuando, para cualquier fórmula en el lenguaje del sistema, existe un método efectivo para determinar si esa fórmula pertenece o no al conjunto de las verdades del sistema. Por ejemplo, la lógica proposicional es decidible, porque existe un algoritmo (la tabla de verdad) que en un número finito de pasos puede decidir si la fórmula es válida o no.

### Completitud

En metalógica, la completitud o completud semántica es la propiedad metateórica que tienen los sistemas formales cuando todas las fórmulas lógicamente válidas (todas las verdades lógicas) del sistema son además teoremas del sistema. Es decir, cuando el conjunto de las verdades lógicas del sistema es un subconjunto del conjunto de teoremas. En otras palabras, si A es una fórmula cualquiera del lenguaje y S es el sistema formal bajo consideración, entonces se cumple que:
    Si $\models _{\mathrm {S} }A$ entonces $\vdash _{\mathrm {S} }A$
Por otra parte, la completitud sintáctica es la propiedad que tienen los sistemas formales cuando, para toda fórmula cerrada del lenguaje del sistema, o bien es un teorema o bien su negación lo es. Esto es, existe una prueba para cada fórmula cerrada o para su negación.
La lógica proposicional y la lógica de primer orden son ambas semánticamente completas, pero no sintácticamente completas. Por ejemplo, en la lógica proposicional, la fórmula p no es un teorema, y tampoco lo es su negación, de modo que eso basta para mostrar que no es sintácticamente completa. No obstante, como ninguna de esas dos fórmulas es una verdad lógica, no afectan a la completitud semántica del sistema.
El segundo teorema de incompletitud de Gödel demuestra que ningún sistema (definido recursivamente) con cierto poder expresivo puede ser a la vez consistente y sintácticamente completo.
Otra propiedad metateórica distinta es la completitud semántica fuerte, que dice: si en un sistema formal S, A es una fórmula bien formada cualquiera que es una consecuencia semántica de un conjunto $\Gamma$ de fórmulas, entonces existe una derivación de A a partir de $\Gamma$. En símbolos:
    Si $\Gamma \models _{\mathrm {S} }A$ entonces $\Gamma \vdash _{\mathrm {S} }A$

### Compacidad

En lógica matemática, el teorema de compacidad establece que un conjunto (posiblemente infinito) de fórmulas bien formadas de la lógica de primer orden tiene un modelo si todos sus subconjuntos finitos tienen un modelo. Es decir, para todo conjunto de fórmulas $\Gamma$ de un lenguaje L, si todo subconjunto finito de $\Gamma$ es satisfacible, entonces $\Gamma$ es satisfacible.

## Resultados metalógicos importantes
### Teorema de Löwenheim-Skolem

En lógica matemática, el teorema de Löwenheim-Skolem o teorema de Löwenheim-Skolem-Tarski es un teorema que establece que si una teoría de primer orden es consistente, entonces tiene al menos un modelo con dominio finito o numerable. Más precisamente: sea T un subconjunto consistente de un lenguaje de primer orden ℒ (con identidad): si T es finito o numerable, entonces tiene al menos un modelo con dominio finito o numerable. Esto significa que las teorías de primer orden no pueden controlar la cardinalidad de sus modelos: ninguna teoría consistente puede tener sólo modelos isomórficos.
La primera versión del teorema se debe a Leopold Löwenheim en 1915, aunque su demostración tenía una pequeña laguna. Thoralf Skolem demostró una segunda versión del teorema en 1919. Desde entonces han aparecido otras versiones.
Skolem comprendió que este teorema se podría aplicar para las formalizaciones de primer orden de la teoría de conjuntos, siendo dicha formalización numerable, existiría un modelo numerable para dicha teoría aun cuando la teoría afirma que existen conjuntos no contables. Este resultado contraintuitivo es la conocida paradoja de Skolem.

### Teorema de completitud de Gödel

El teorema de completitud de Gödel es un importante teorema de la lógica matemática, que fue demostrado por primera vez por Kurt Gödel en 1929 y que en su forma más conocida establece lo siguiente:
* En una lógica de primer orden, toda fórmula que es válida en un sentido lógico es demostrable.
* Kurt Gödel
La palabra "demostrable" significa que existe una deducción formal de la fórmula. La deducción consiste en una lista finita de pasos en los que cada paso o bien invoca a un axioma o es obtenido a partir de pasos previos mediante una básica regla de inferencia. A partir de dicha deducción, es posible verificar si cada uno de los pasos es correcto mediante un algoritmo (por ejemplo, mediante una computadora o a mano).
Una fórmula es lógicamente válida si es verdadera en todo modelo para el lenguaje utilizado en la fórmula. Para expresar de manera formal el teorema de completitud de Gödel, se debe definir el significado de la palabra modelo en este contexto. Esta es una definición básica en la teoría de modelos.
El teorema de Gödel establece una correspondencia entre la verdad semántica y la probabilidad sintáctica en la lógica de primer orden. Crea un vínculo entre la teoría de modelos que se ocupa de lo que es cierto en diferentes modelos, y la teoría de la demostración que estudia lo que se puede probar formalmente en sistemas formales particulares. Gödel utilizó el teorema de completitud para probar el teorema de compacidad, demostrando la naturaleza finitaria del operador de consecuencia lógica. Estos resultados ayudaron a establecer la lógica de primer orden como el tipo de lógica dominante en las matemáticas actuales.

### Otros resultados

* Consistencia de la lógica proposicional veritativo-funcional (Emil Post 1920)
* Completitud semántica de la lógica proposicional veritativo-funcional (Paul Bernays 1918, Emil Post 1920)
* Decidibilidad de la lógica proposicional veritativo funcional (Emil Post 1920)
* Consistencia de la lógica de primer orden monádica (Leopold Löwenheim 1915)
* Completitud semántica de la lógica de primer orden monádica (Leopold Löwenheim 1915)
* Decidibilidad de la lógica de primer orden monádica (Leopold Löwenheim 1915)
* Consistencia de la lógica de primer orden (David Hilbert y Wilhelm Ackermann 1928)
* Indecibilidad de la lógica de primer orden (Entscheidungsproblem, Alonzo Church 1936 y Alan Turing 1936)