Metalógica

[1]​ Las propiedades más importantes que se pueden demostrar de los sistemas formales son la consistencia, decidibilidad y completitud.

La existencia de un modelo implica que una teoría lógica es consistente.

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

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.

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

[5]​ 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.

[6]​ 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.

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.

La palabra "demostrable" significa que existe una deducción formal de la fórmula.