1.2 KiB
up, tags, aliases
up | tags | aliases | |
---|---|---|---|
|
[!definition] Définition Soit
V = \{ x_1, \dots, x_{n} \}
un ensemble (fini) de symboles de variables Un type en les variablesV
est un ensemble de formules dont les variables libres appartiennent àV
de la forme :\operatorname{tp}_{A}(a) = \{f \mid A \models f(a_1, \dots, a_{n}) \}
l'ensemble des formules satisfaites dansA
oùa = (a_1, \dots, a_{n})
et oùA
est une structure pour la signature donnéea_1, \dots, a_{n} \in A
[!info] Cas particulier important pour
n = 0
etV = \emptyset
on notera plutôt\operatorname{Th}(A) = \{ f \mid A \models f \}
l'ensemble des énoncés vrais dansA
, i.e la théorie deA
^definition
[!definition] Ensemble des types Soit
\mathcal{F}_{n}
l'ensemble des formules à variables libres dans\{ x_1, \dots, x_{n} \}
On note\mathscr{S}_{n} \in \mathcal{P}(\mathcal{P}(\mathcal{F}_{n}))
l'ensemble de tous les types en\{ x_1, \dots, x_{n} \}
- i
\mathscr{S}_{0}
est l'ensemble de toutes les théories[!info]- Topologie sur
\mathscr{S}_{n}
f \in \mathcal{F}_{n}
\{ t \in \mathscr{S}_{n} \mid f \in t \} =