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. +more 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 \{\top,\bot\} a pro \iota množina tříd ekvivalence formulí tohoto typu. +more 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 \Phi. Speciálně pro \Phi([A_{\alpha\beta}]) je funkce, jejíž hodnota pro \Phi([B_{\beta}]) je \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á.

Kategorie:Matematická logika Kategorie:Sémantika