Une méthode de construction d'un modèle pour une théorie du premier ordre consistante en étendant un ensemble de formules consistant en une théorie maximale consistante (théorie de Henkin) qui contient des constantes témoins explicites pour les formules existentielles, puis en formant le modèle canonique des termes (ou le quotient par l'égalité démontrable). Cette méthode soutient les preuves de complétude et d'existence de modèles.

Principe

Pour chaque formule ∃x φ(x) dans la théorie, ajouter un symbole de constante neuf c_φ et un axiome φ(c_φ) ; étendre le langage et la théorie pour que toute existentielle ait un témoin, puis étendre en un ensemble maximalement consistant (argument de Zorn ou de Lindenbaum) et interpréter les termes pour produire un modèle.

Démonstration

Commencer par une théorie consistante T dans un langage L. Énumérer les formules et chaque fois qu'apparaît ∃x φ(x), introduire une nouvelle constante c et ajouter φ(c) à la théorie en préservant la consistance ; répéter et prendre ensuite une théorie de Henkin T* maximalement consistante dans le langage étendu. L'ensemble des termes clos modulo l'égalité démontrable forme un modèle de T* dont le réduct satisfait T.

Mauvaise application

Ajouter des témoins sans vérifier la consistance, ou supposer que l'henkinisation fournit un modèle dans le langage original sans contrôler la conservativité. Une autre erreur consiste à traiter les constantes de Henkin comme signifiantes en dehors du modèle construit sans référence à l'identification preuve-théorique.

Conséquence

Fournit une voie constructive vers le théorème de complétude et vers la construction de modèles concrets à partir de théories consistantes ; donne des modèles de termes et montre que la consistance syntaxique implique satisfiabilité sémantique en logique du premier ordre.

Inversion

Supprimer les témoins de Henkin et prendre le réduct peut faire perdre les termes explicites réalisant les existentielles ; inversement, traiter la théorie henkinisée comme identique à l'original omet que de nouveaux symboles ont été introduits pour garantir des témoins.

Limite

S'applique en logique du premier ordre et aux théories où l'on peut ajouter systématiquement des témoins ; des considérations de cardinalité ou du choix peuvent affecter la taille du langage étendu mais n'empêchent pas la méthode sous les hypothèses usuelles. Ne produit pas en soi de modèles pour des propriétés d'ordre supérieur ou non axiomatisables.

Tension sémantique

Se situe face aux preuves d'existence de modèles fondées sur la compacité ou les ultraproduits : la construction de Henkin est syntaxique et explicite, tandis que les arguments par compacité ou ultraproduit sont plus sémantiques ; la tension apparaît selon la préférence pour des preuves syntaxiques ou sémantiques d'existence.

Synthèse

La construction de Henkin transforme la recherche d'un modèle en une extension syntaxique systématique : ajouter des constantes témoins pour chaque existentielle, étendre à la maximalité de consistance, puis interpréter les termes clos pour obtenir un modèle, reliant ainsi la consistance prouvable à l'existence de structures.