Cours 7 : Théories axiomatiques

Introduction

Problème de la conséquence logique mais où les symboles sont interprétés d’une manière fixée (ex: l’addition).

⟶ Les SAT Modulo Theory (SMT)

Exs :

Z3 de Microsoft

⟹ on veut iterpréter les symboles d’une manière fixée.

⟶ on axiomatise de manière suiffisamment riche (tout en gradant le cractère récursif) pour forcer l’interprétation de certains symboles.

Rien à voir : le programme de Hilbert ⟶ BUT : donner des fondements sûrs aux maths.

Part de choses dont est “sûrs” (ex: 1+1=2, 1< 3, etc…), et on reconstruit les mathématiques à partir de ça.

Puis : on rajoute des choses (qui n’introduisent pas d’incohérence) pour étendre l’arithmétique.

Théories axiomatiques

Théorie :: un ensemble de formules $T$ sans variables libres clos par conséquence logique (i.e : si $T ⊨ 𝜑$ , alors $𝜑 \in T$ )

Si $S$ est une $F, P$ -structure :
$T h (S) ≝ {𝜑 ∣ S ⊨ 𝜑}$
Si $A$ est un ens. de formules sans var libres ( $A$ est supposé récursif) :
$T h (A) ≝ {𝜑 ∣ A ⊨ 𝜑}$
NB: on suppose $A$ récursif car ce qui nous intéresse, ce sont les problèmes de décision

$T$ est complète :: ssi pour tout $𝜑$ sans variables libres,
$T ⊨ 𝜑 ou T ⊨ \neg 𝜑$
$T$ est cohérente :: ssi $T ⊭ 𝜑 ou T ⊭ \neg 𝜑$

$T h (S)$ est complète et cohérente
- comme elle est complète, elle est co-réc. én., donc (par symétrie), elle est aussi réc. én., donc réc.
$T h (A)$ est
- incomplète si $A = \emptyset$ , car alors $T h (A)$ est l’ensemble des tautologies, et la formule $p$ n’en est pas conséquence logique ni sa négation
- si $p$ et $\neg p$ appartiennent à $A$ , c’est incohérent
- MAIS CE QU’ON SAIT : c’est que $T h (A)$ est réc. én., car l’ensemble des conséquences logiques d’un ens. de formules récursif est réc. én. (mais en général ce n’est pas récursif).

Théories :

Complète	Récursive pas complète	Pas récursive
Th. des ordres denses	Th. de l’égalité	Arithmétique élémentaire
Th. des ordres discrets		Arithmétique de Peano ⟶ Th. de Gödel
Arithmétique de Presburger ( $(ℕ, +, 0, 1, =)$ )
Th. des corps réels clos $(ℝ, \times, +, 0, 1, \geq)$ (nombres algébriques) ⟹ décidabilité de la géom. eucl. réelle

NB: Pour montrer la décidabilité de l’arithmétique de Presburger, on utilise des automates

Théories décidables

Méthode qu’on va utiliser : l’élimination des quantificateurs

Th : Soit $A$ un ens. d’axiomes récursif.

pour toute $𝜑$ sans quantificateurs, il existe $𝜓$ sans quantificateurs tq :

$A ⊨ (\exists x . 𝜑) ⟷ 𝜓$

pour toute formule close $𝜃$ , si $A ⊨ 𝜃$ est décidable (resp. $A ⊨ 𝜃$ ou $A ⊨ \neg 𝜃$ ) alors $T h (A)$ est récursive (resp. complète).

Théorie des ordres denses

2 prédicats : $\geq, =$ ( $>$ défini de manière usuelle)
pas de fonctions

Axiomes de l’égalité :

$\forall x . x = x$
$\forall x, y . x = y ⟶ y = x$
$\forall x, y, z . x = y \land y = z ⟶ x = z$
$\forall x, y, z . x = y \land y > z ⟶ x > z$
$\forall x, y, z . x = y \land z > y ⟶ z > x$
Totalité : $\forall x, y . x \leq y \lor y \leq x$
$\forall x . x \geq x$
$\forall x, y . x \geq y \land y \geq x ⟶ x = y$
$\forall x, y, z . x \geq y \land y \geq z ⟶ x \geq z$
Densité : $\forall x, y . x > y ⟶ \exists z . x > z \land z > y$

Remarquons que

A ⊨ \exists x . 𝜑 ⟷ 𝜓

si $𝜑$ est en forme normale disjonctive, on peut pousser le $\exists$ à l’intérieur
on remplace $u \geq v$ par $u = v \lor u > v$

Il suffit de faire la preuve quand $𝜑$ est une conjonction de formules atomiques.

𝜑 = 𝜑_{- x} \land 𝜑^{'}

où $𝜑_{- x}$ ne contient pas de $x$ , et toutes les formules atomiques de $𝜑^{'}$ contiennent $x$

si $𝜑^{'}$ contient $x = y$ ou $y = x$ , on prend, pour $𝜓$ , $𝜑$ où on a remplacé toutes les occurrences de $x$ par $y$
sinon :

𝜑^{'} = ⋂_{i \in I} x > x_{i} \land ⋂_{j \in J} x_{j} > x

On pose

𝜓 ≝ ⋂_{i \in I, j \in J} x_{j} > x_{i}

On veut mq

A ⊨ (\exists x . 𝜑^{'}) ⟷ 𝜓

en effet :

$⟶$ par transitivité
pour $⟵$ :

Soit $M$ un modèle de $A$ et $𝜎 : V a r (𝜑^{'}) ⟶ D_{M}$

M, 𝜎 ⊨ 𝜓

On note $a$ (resp. $b$ ) le max (resp. le min) des $x_{i} 𝜎$ (resp. $x_{j} 𝜎$ ) (ils existent par totalité).

Comme $M, 𝜎 ⊨ 𝜓$ , $b >_{M} a$ .

Comme $M ⊨ A$ , par densité, soit $c \in D_{M}$ tq

b >_{M} c >_{M} a

On étend $𝜎$ en associant $c$ à $x$ .

Alors

M, 𝜎 ⊨ 𝜑^{'}

(par transitivité) donc

M, 𝜎 ⊨ \exists x . 𝜑^{'}

Puis, on conclut en avec le fait que les seules formules sans var sont “Vrai” et “Faux” (donc le deuxième point est rempli).

Pourtant, le démonstration précédente est fausse : considérer

$\forall x, y . x = y$
$N o M a x ≝ \forall x . \exists y; y > x$

Or :

$[0, 1] ⊭ N o M a x$
$ℝ ⊨ N o M a x$

alors que $[0, 1] ⊨ A$ et $ℝ ⊨ A$

Idem pour

$N o M i n ≝ \forall x . \exists y; x > y$

D’où vient le problème ? : on a supposé, dans la démo, que $I$ et $J$ sont non vides.

Donc en rajoutant $N o M i n$ et $N o M a x$ , la théorie devient vraiment complète.

Problème : on n’a pas sous la main l’élément min, s’il existe.

On introduit un nouvel axiome (il existe un élément min) :

\forall u . (P (u) ⟷ \forall x . x \geq u)

⟶ on va avoir à plusieurs endroits le prédicat $P$ ⟹ le point deux devient moins trivial.

Théorie de l’égalité

$A$ : axiomes de l’égalité
un seul prédicat : $=$
pas de fonctions

Cette th. n’est pas complète.

Pour le montrer : on exhibe deux modèles $M_{1}, M_{2}$ de $A$ et une formule $𝜑$ tq $M_{1} ⊨ 𝜑$ mais $M_{2} ⊨ \neg 𝜑$

Contre-ex : $𝜑 = \forall x, y . x = y$ et $M_{1} = {a}, M_{2} = {a, b}$ où l’égalité est l’égalité syntaxique (les modèles de $𝜑$ sont les ens. à une seule classe d’éq.).

Soit $E_{n}$ une nouvelle var. prop. et :

𝛷_{n} ≝ E_{n} ⟷ \exists x_{1}, \dots, x_{n} . \underset{i \neq j}{⋀} x_{i} \neq x_{j}

Extension par définition :: on ajoute des var prop $E_{i}$ et les formules $𝛷_{n}$ correspondantes : on appelle $A^{+}$ cette nouvelle théorie

Lemme : $T h (A) = T h (A^{+}) \cap {𝜑 sans E_{i}}$ (extension conservative)

L’inclusion directe est immédiate.

Réciproquement : si $T h (A^{+}) ⊨ 𝜑$ et $𝜑$ sans $E_{i}$ , mq $𝜑 \in T h (A)$ .

On peut le faire en “inlinant” la définition des $E_{i}$ , ou en prenant un modèle de $T h (A)$ et en montrant que c’est un modèle de $T h (A^{+})$ , si on affecte les bonnes valeurs de vérité aux $E_{i}$ .

$A^{+} ⊨ (\exists x . 𝜑) ⟷ 𝜓$

Seul cas intéressant : $𝜑$ conjonction de formules atomiques contenant $x$ , $𝜑$ ne contient pas de formules $x = y$ .

𝜑 = \underset{i \in I}{⋀} x_{i} \neq x

Problème : on aimerait introduire les $E_{i}$ (qui ne contiennent pas $x$ ), mais on ne connaît la relation des $x_{i}$ entre eux (sont-ils égaux ? différents ?).

\underset{R \in E q (I)}{⋁} \underset{(i, j) \in R}{⋀} x_{i} = x_{j} \underset{(i, j) \notin R}{⋀} x_{i} \neq x_{j} \underset{i}{⋀} x_{i} \neq x

On note $I_{R}$ un ensemble d’indices de représentants modulo $R$ .

\underset{R \in E q (I)}{⋁} \underset{(i, j) \in R}{⋀} x_{i} = x_{j} [\underset{i \in I_{R}}{⋀} x_{i} \neq x \underset{i \neq j \in I_{R}}{⋀} x_{i} \neq x_{j}]

Or :

\exists x . [\underset{i \in I_{R}}{⋀} x_{i} \neq x \underset{i \neq j \in I_{R}}{⋀} x_{i} \neq x_{j}] ⟷ E_{| I_{R} |}

𝜓 = \underset{R \in E q (I)}{⋁} \underset{(i, j) \in R}{⋀} x_{i} = x_{j} \land E_{| I_{R} | + 1}

Formules sans variables de $T h (A^{+}) \subseteq F_{0} ({E_{0}, \dots, E_{n}, \dots})$

𝕰 ≝ {E_{i + 1} ⟶ E_{i} ∣ i \in ℕ}

A^{+} ⊨ 𝕰

Si $𝜑 \in F_{0} ({E_{0}, \dots, E_{n}, \dots})$

Lemme : $A^{+} ⊨ 𝜑 ⟺ 𝕰 ⊨ 𝜑$

Lemme 2 : $𝕰 ⊨ 𝜑$ ssi ${E_{i + 1} ⟶ E_{i} ∣ i \leq N} ⊨ 𝜑$

où $N$ est le + grand indice d’une var prop de $𝜑$

En quoi le problème $𝕰 ⊨ 𝜑$ est-il décidable ? :

Les modèles de $𝕰$ sont ${E_{0}, \dots, E_{k}}$ (pour $k \in ℕ$ ) et ${E_{i} ∣ i \in ℕ}$

⟶ Pour chaque modèle ${E_{0}, \dots, E_{k}}$ (pour $0 \leq k \leq N$ ), on teste si ${E_{0}, \dots, E_{k}} ⊨ 𝜑$

Share on

Twitter Facebook Google+ LinkedIn