Un método para construir un modelo de una teoría de primer orden ampliando un conjunto consistentes de fórmulas a una teoría maximalmente consistente (teoría de Henkin) que contiene constantes testigo explícitas para las fórmulas existenciales, y formando después el modelo canónico de términos (o el cociente por la igualdad demostrable). Sustenta pruebas de completitud y existencia de modelos.

Principio

Para cada fórmula ∃x φ(x) en la teoría, añadir un símbolo de constante nuevo c_φ y un axioma φ(c_φ); ampliar el lenguaje y la teoría para que toda existencial tenga un testigo, luego extender a un conjunto maximalmente consistente (usando Zorn o argumentos de Lindenbaum) e interpretar términos para producir un modelo.

Demostración

Comenzar con una teoría consistente T en lenguaje L. Enumerar las fórmulas y cada vez que aparezca ∃x φ(x) introducir una nueva constante c y añadir φ(c) a la teoría preservando la consistencia; repetir y luego tomar una teoría de Henkin T* maximalmente consistente en el lenguaje ampliado. El conjunto de términos cerrados módulo la igualdad demostrable forma un modelo de T* cuyo reducto satisface T.

Aplicación incorrecta

Agregar testigos sin comprobar la consistencia, o asumir que la henquinización produce un modelo en el lenguaje original sin verificar la conservatividad. Otro abuso es tratar las constantes de Henkin como significativas fuera del modelo construido sin referencia a la identificación prueba-teoría.

Consecuencia

Proporciona una vía constructiva al teorema de completitud y a la construcción de modelos concretos a partir de teorías consistentes; produce modelos de términos y muestra que la consistencia sintáctica implica satisfacibilidad semántica en lógica de primer orden.

Inversión

Eliminar los testigos de Henkin y tomar el reducto puede hacer perder los términos explícitos que realizan las existenciales; a la inversa, tratar la teoría henquinizada como idéntica a la original pasa por alto que se introdujeron símbolos para garantizar testigos.

Límite

Se aplica en lógica de primer orden y a teorías donde se pueden añadir testigos sistemáticamente; consideraciones de cardinalidad o del axioma de elección pueden afectar el tamaño del lenguaje ampliado pero no invalidan el método bajo las hipótesis habituales. No produce por sí mismo modelos para propiedades esencialmente de segundo orden o no axiomatizables.

Tensión semántica

Contrasta con pruebas semánticas de existencia de modelos basadas en compacidad o ultraproductos: la construcción de Henkin es sintáctica y explícita, mientras que compacidad/ultraproductos son más semánticos; existe tensión según la preferencia por métodos sintácticos o semánticos.

Síntesis

La construcción de Henkin convierte la búsqueda de un modelo en una extensión sintáctica sistemática: añadir constantes testigo para cada existencial, extender a maximalidad de consistencia y luego interpretar términos cerrados para obtener un modelo, vinculando así consistencia demostrable con la existencia de estructuras.