eduroam-prg-sg-1-44-17.net.univ-paris-diderot.fr 2025-10-15:14:9:14
This commit is contained in:
@@ -8,6 +8,7 @@ aliases:
|
|||||||
|
|
||||||
> [!definition] Définition
|
> [!definition] Définition
|
||||||
> Une théorie $T$ est henkinienne si :
|
> Une théorie $T$ est henkinienne si :
|
||||||
|
> - elle est [[théorie logique#^coherence|cohérente]]
|
||||||
> - elle est [[théorie logique#^completude-syntaxique|syntaxiquement complète]]
|
> - elle est [[théorie logique#^completude-syntaxique|syntaxiquement complète]]
|
||||||
> - pour toute formule $f(x)$ en une variable libre $x$ telle que $T \vdash \exists x f$, il existe un terme clos $t$ dans le langage tel que $T \vdash f(t)$
|
> - pour toute formule $f(x)$ en une variable libre $x$ telle que $T \vdash \exists x f$, il existe un terme clos $t$ dans le langage tel que $T \vdash f(t)$
|
||||||
^definition
|
^definition
|
||||||
@@ -19,6 +20,9 @@ aliases:
|
|||||||
> Soient $t_1, \dots, t_{n}$ et $u_1, \dots, u_{n}$ des termes clos tels que $T \vdash t_1 = u_1, \dots, T \vdash t_{n} = u_{n}$
|
> Soient $t_1, \dots, t_{n}$ et $u_1, \dots, u_{n}$ des termes clos tels que $T \vdash t_1 = u_1, \dots, T \vdash t_{n} = u_{n}$
|
||||||
> alors $T \vdash R(t_1, \dots, t_{n}) \leftrightarrow R(u_{1}, \dots, u_{n})$
|
> alors $T \vdash R(t_1, \dots, t_{n}) \leftrightarrow R(u_{1}, \dots, u_{n})$
|
||||||
|
|
||||||
|
> [!proposition]+
|
||||||
|
> Si $T$ est une théorie hentinienne, sa réalisation canonique en est un modèle
|
||||||
|
|
||||||
# Exemples
|
# Exemples
|
||||||
|
|
||||||
|
|
||||||
|
|||||||
@@ -6,7 +6,6 @@
|
|||||||
|
|
||||||
# Propriétés
|
# Propriétés
|
||||||
|
|
||||||
## Cohérence
|
|
||||||
> [!proposition]+ Cohérence
|
> [!proposition]+ Cohérence
|
||||||
> une théorie est cohérente si $\top \not \vdash \bot$
|
> une théorie est cohérente si $\top \not \vdash \bot$
|
||||||
>
|
>
|
||||||
@@ -87,6 +86,32 @@
|
|||||||
> > > et donc $T \vdash f$ par [[modus ponens]]
|
> > > et donc $T \vdash f$ par [[modus ponens]]
|
||||||
> > >
|
> > >
|
||||||
|
|
||||||
|
> [!proposition]+ Théorème (Gödel)
|
||||||
|
> Toute théorie cohérente a un modèle
|
||||||
|
>
|
||||||
|
> > [!démonstration]- Démonstration
|
||||||
|
> > **Principe de la démonstration :**
|
||||||
|
> > $T$ une théorie cohérente dans un langage $L$
|
||||||
|
> > $T \subseteq T'$ une théorie maximale
|
||||||
|
> > $T_1$ théorie cohérente dans un nouveau langage $L_1$
|
||||||
|
> > - $L_1 = L \cup \{ c_{f} \}$ avec $c_{f}$ un symbole de constante
|
||||||
|
>
|
||||||
|
> >
|
||||||
|
> > [!corollaire]
|
||||||
|
> > Soit $f$ un énoncé.
|
||||||
|
> > Pour que $T \vdash f$ il faut et il suffit que pour tout modèle $A$ de $T$, on ait $A \models f$
|
||||||
|
> > > [!démonstration]- Démonstration
|
||||||
|
> > > - si $T \vdash f$ alors $A \models f$ pour tout modèle $A$ de $T$
|
||||||
|
> > > - réciproque :
|
||||||
|
> > > Soit $T' = T \cup \{ \neg f \}$
|
||||||
|
> > > Si $T'$ est [[théorie logique#^coherence|cohérente]], il existe un modèle $A$ de $T'$
|
||||||
|
> > > $A$ est un modèle de $T$ dans lequel $A \models \neg f$
|
||||||
|
> > > Donc $T'$ n'est pas cohérente.
|
||||||
|
> > > $T' \cup \{ \neg f \} \vdash \bot$
|
||||||
|
> > > par le théorème de déduction :
|
||||||
|
> > > $T \vdash (\neg f \to \bot)$
|
||||||
|
> > > donc $T \vdash f$ car $f \leftrightarrow (\neg f \to \bot)$ est une [[règles de démonstration . tautologies|tautologie]]
|
||||||
|
>
|
||||||
|
|
||||||
|
|
||||||
%%
|
%%
|
||||||
|
|||||||
Reference in New Issue
Block a user