Un teorema que da condiciones bajo las cuales una teoría consistente de primer orden y contable posee un modelo que omite una colección especificada de tipos no principales (no aislados); formulado clásicamente para lenguaje contable y familias contables de tales tipos.

Principio

Con lenguaje contable y teoría consistente, si los tipos a omitir son no principales y la familia es contable, es posible construir un modelo que evita la realización de cada tipo de la familia, mediante una construcción de Henkin o argumentos topológicos/de categoría de Baire en el espacio de tipos.

Demostración

Sea T una teoría contable y consistente y {p_n(x)} una sucesión contable de tipos 1 no principales. Añadiendo constantes de Henkin a T y organizando en etapas la no realización de cada p_n (o construyendo un conjunto comeagre de completaciones en el espacio de Stone que omiten todos los p_n), se obtiene un modelo contable de T que no realiza ninguno de los p_n.

Aplicación incorrecta

Afirmar que el teorema es válido en lenguajes no contables, para familias no contables de tipos o que garantiza la omisión de tipos principales; tales afirmaciones suelen fallar porque la compacidad y restricciones de cardinalidad pueden forzar la realización.

Consecuencia

Permite un control fino en la construcción de modelos: existencia de modelos con omisiones prescritas; se usa para producir modelos con propiedades algebraicas o combinatorias particulares y para distinguir clases de modelos según los tipos que realizan.

Inversión

La situación dual es que la compacidad puede imponer que ciertos tipos se realicen en todo modelo (por ejemplo, tipos principales determinados por diagramas finitos), de modo que en lugar de omisión se considera la inevitabilidad de la realización.

Límite

Se aplica principalmente a teorías de primer orden en lenguajes contables y a tipos no principales (a menudo contables). El teorema no se extiende en general a cardinalidades arbitrarias ni a familias de tipos cuya no realización contradiga la compacidad.

Tensión semántica

Existe tensión entre el teorema y la compacidad: la compacidad tiende a generar realizaciones a partir de consistencia local, mientras que las construcciones de omisión aprovechan un control global; también hay tensión con nociones más fuertes como la omisión de hiper‑imaginarios, donde el teorema clásico no asegura nada.

Síntesis

El Teorema de Omisión de Tipos proporciona un método dependiente de la contabilidad para construir modelos que eviten la realización de tipos no principales especificados, equilibrando las limitaciones de la compacidad con técnicas constructivas o topológicas para la omisión selectiva.