860 B
860 B
up, tags, aliases
| up | tags | aliases | ||
|---|---|---|---|---|
|
|
[!definition] Définition Une théorie
Test henkinienne si :
- elle est théorie logique#^coherence
- elle est théorie logique#^completude-syntaxique
- pour toute formule
f(x)en une variable librextelle queT \vdash \exists x f, il existe un terme clostdans le langage tel queT \vdash f(t)^definition
Propriétés
[!proposition]+ Soit
Run symbole de relation $n$-aire, Soientt_1, \dots, t_{n}etu_1, \dots, u_{n}des termes clos tels queT \vdash t_1 = u_1, \dots, T \vdash t_{n} = u_{n}alorsT \vdash R(t_1, \dots, t_{n}) \leftrightarrow R(u_{1}, \dots, u_{n})
[!proposition]+ Si
Test une théorie hentinienne, sa réalisation canonique en est un modèle