Henkinův model

Henkinův model je model teorie vyššího řádu v obecné sémantice, přičemž platí, že každá bezesporná teorie má model (se spočetnými doménami). Definici předložil Leon Henkin ve svém příspěvku k úplnosti v teorii typů.

V Henkinově modelu probíhá kvantifikace vyššího řádu přes pevně dané domény, díky čemuž jsou takové modely hojnější a silnější, než modely ve standardní sémantice. Speciálně platí, že reifikovaná teorie prvního řádu věrně reflektuje validní formule vyššího řádu. Tyto modely se používají například ve formální sémantice při zpracování přirozených jazyků.

Vytvoření kanonického modelu

Je-li $T$ bezesporná teorie, můžeme sestrojit její kanonický model indukcí podle typu formulí. Doména pro typ $o$ je $\{\mathrm{\top },\mathrm{\perp }\}$ a pro $\iota$ množina tříd ekvivalence formulí tohoto typu. Pro typy $\alpha$ a $\beta$ s doménami $D_{\alpha }$ a $D_{\beta }$ můžeme sestrojit příslušnou doménu $D_{\alpha \beta }$ jakožto množinu tříd ekvivalence hodnot valuační funkce $\mathrm{\Phi }$. Speciálně pro $\mathrm{\Phi }([A_{\alpha \beta }])$ je funkce, jejíž hodnota pro $\mathrm{\Phi }([B_{\beta }])$ je $\mathrm{\Phi }([A_{\alpha \beta }{B}_{\beta }])$. $D_{\alpha \beta }$ je množina hodnot této funkce pro všechny uzavřené formule $A_{\alpha \beta }$. V takto sestrojeném modelu je pro libovovolný typ jeho doména spočetná.