Una realización de un tipo p(x) en un modelo M es un elemento o tupla a de M tal que cada fórmula en p(x) es verdadera para a en M; equivalentemente, a realiza p si M ⊨ φ(a) para toda φ(x) ∈ p.

Principio

La realización vincula la descripción sintáctica dada por un tipo con un objeto semántico concreto en un modelo; que un tipo sea realizado depende de las propiedades del modelo (tamaño, saturación) y del propio tipo.

Demostración

Un tipo de trascendencia sobre Q se realiza en cualquier extensión de Q que contenga un elemento trascendente; en un campo algebraicamente cerrado κ-saturado, todo tipo sobre un conjunto de parámetros de tamaño < κ es realizado por algún elemento del campo.

Aplicación incorrecta

Suponer que todo tipo consistente (o completo) se realiza en cualquier modelo: la realización puede fallar en modelos pequeños o no saturados, y la omisión de tipos es un fenómeno importante para construcciones.

Consecuencia

Cuando los tipos se realizan se obtienen testigos concretos para descripciones abstractas, lo que permite construir explícitamente elementos con comportamiento prescrito y vincular los tipos con cálculos de órbitas e independencia.

Inversión

El concepto inverso es la omisión: un modelo puede omitir un tipo (ningún elemento lo realiza), lo cual es central para el Teorema de Omisión de Tipos y para construir modelos con propiedades controladas.

Límite

La realización es relativa al modelo: el mismo tipo puede realizarse en algunos modelos y omitirse en otros; la realización trata la verdad de primer orden en una estructura dada y no aborda realizaciones de segundo orden o infinitarias.

Tensión semántica

La realización puede confundirse con la satisfactibilidad de una fórmula: la satisfactibilidad se refiere a la existencia de algún modelo y elemento que haga verdadera una fórmula, mientras que la realización fija tanto el tipo como el modelo ambiente donde cada fórmula del tipo se cumple.

Síntesis

Una realización es el testigo concreto en un modelo que hace verdaderas todas las fórmulas de un tipo dado; el patrón de cuáles tipos se realizan en qué modelos codifica información estructural profunda sobre la teoría y sus modelos.