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 \vDash 𝜑$, alors $𝜑∈T$)

  • Si $S$ est une $F,P$-structure :

    \[Th(S) ≝ \lbrace 𝜑 \mid S \vDash 𝜑 \rbrace\]

  • Si $A$ est un ens. de formules sans var libres ($A$ est supposé récursif) :

    \[Th(A) ≝ \lbrace 𝜑 \mid A \vDash 𝜑 \rbrace\]

    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 \vDash 𝜑 \text{ ou } T \vDash ¬𝜑\]
$T$ est cohérente :

ssi \(T \not\vDash 𝜑 \text{ ou } T \not\vDash ¬𝜑\)

  • $Th(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.

  • $Th(A)$ est

    • incomplète si $A=∅$, car alors $Th(A)$ est l’ensemble des tautologies, et la formule $p$ n’en est pas conséquence logique ni sa négation

    • si $p$ et $¬p$ appartiennent à $A$, c’est incohérent

    • MAIS CE QU’ON SAIT : c’est que $Th(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 $(ℝ, ×, +, 0, 1, ≥)$ (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.

  1. pour toute $𝜑$ sans quantificateurs, il existe $𝜓$ sans quantificateurs tq :
\[A \vDash (∃x. 𝜑) \longleftrightarrow 𝜓\]
  1. pour toute formule close $𝜃$, si $A \vDash 𝜃$ est décidable (resp. $A \vDash 𝜃$ ou $A \vDash ¬𝜃$) alors $Th(A)$ est récursive (resp. complète).

Théorie des ordres denses

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

Axiomes de l’égalité :

  • $∀x. x = x$
  • $∀x, y. x = y ⟶ y=x$
  • $∀x, y, z. x=y ∧ y=z ⟶ x=z$
  • $∀x, y, z. x=y ∧ y>z ⟶ x > z$
  • $∀x, y, z. x=y ∧ z>y ⟶ z > x$
  • Totalité : $∀x, y. x ≤y ∨ y ≤x$
  • $∀x. x≥x$
  • $∀x, y. x≥y ∧ y ≥ x ⟶ x=y$
  • $∀x, y, z. x≥y ∧ y ≥ z ⟶ x≥z$
  • Densité : $∀x, y. x>y ⟶ ∃ z. x > z ∧ z > y$

Remarquons que

\[A \vDash ∃x. 𝜑 \longleftrightarrow 𝜓\]

  • si $𝜑$ est en forme normale disjonctive, on peut pousser le $∃$ à l’intérieur

  • on remplace $u≥v$ par $u =v ∨ u>v$

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

\[𝜑 = 𝜑_{-x} ∧ 𝜑'\]

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 :

\[𝜑' = \bigcap_{i∈I} x> x_i ∧ \bigcap_{j∈J} x_j > x\]

On pose

\[𝜓 ≝ \bigcap_{i∈I, j∈J} x_j > x_i\]

On veut mq

\[A \vDash (∃x. 𝜑') \longleftrightarrow 𝜓\]

en effet :

  • $⟶$ par transitivité
  • pour $⟵$ :

Soit $M$ un modèle de $A$ et $𝜎 : Var(𝜑’) ⟶ D_M$

\[M, 𝜎 \vDash 𝜓\]

On note $a$ (resp. $b$) le max (resp. le min) des $x_i 𝜎$ (resp. $x_j 𝜎$) (ils existent par totalité).

Comme $M, 𝜎 \vDash 𝜓$, $b >_M a$.

Comme $M \vDash A$, par densité, soit $c∈D_M$ tq

\[b>_M c >_M a\]

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

Alors

\[M, 𝜎 \vDash 𝜑'\]

(par transitivité) donc

\[M, 𝜎 \vDash ∃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

  • $∀x, y. x=y$

  • $NoMax ≝ ∀x. ∃y; y >x$

Or :

  • $[0, 1] \not\vDash NoMax$
  • $ℝ \vDash NoMax$

alors que $[0,1] \vDash A$ et $ℝ \vDash A$

Idem pour

  • $NoMin ≝ ∀x. ∃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 $NoMin$ et $NoMax$, 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) :

\[∀u. \; (P(u) \longleftrightarrow ∀x. x≥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 \vDash 𝜑$ mais $M_2 \vDash ¬𝜑$

Contre-ex : $𝜑 = ∀x, y. x= y$ et $M_1 = \lbrace a \rbrace, M_2 = \lbrace a, b \rbrace$ 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 \longleftrightarrow ∃x_1, \ldots, x_n. \bigwedge_{i≠j} x_i ≠ 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 : \(Th(A) = Th(A^+) ∩ \lbrace 𝜑 \text{ sans } E_i \rbrace\) (extension conservative)

L’inclusion directe est immédiate.

Réciproquement : si $Th(A^+) \vDash 𝜑$ et $𝜑$ sans $E_i$, mq $𝜑∈Th(A)$.

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

Mq

\[A^+ \vDash (∃x. 𝜑) \longleftrightarrow 𝜓\]

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

\[𝜑 = \bigwedge_{i∈I} x_i ≠ 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 ?).

\[\bigvee_{R∈Eq(I)} \bigwedge_{(i,j)∈R} x_i = x_j \bigwedge_{(i,j)∉R} x_i ≠ x_j \bigwedge_{i}x_i ≠ x\]

On note $I_R$ un ensemble d’indices de représentants modulo $R$.

\[\bigvee_{R∈Eq(I)} \bigwedge_{(i,j)∈R} x_i = x_j \bigg[\bigwedge_{i∈I_R} x_i ≠ x \bigwedge_{i≠j∈I_R}x_i ≠ x_j \bigg]\]

Or :

\[∃x. \; \bigg[\bigwedge_{i∈I_R} x_i ≠ x \bigwedge_{i≠j∈I_R}x_i ≠ x_j \bigg] \longleftrightarrow E_{\vert I_R \vert}\]

et

\[𝜓 = \bigvee_{R∈Eq(I)} \bigwedge_{(i,j)∈R} x_i = x_j ∧ E_{\vert I_R \vert+1}\]

Formules sans variables de $Th(A^+) ⊆ F_0 (\lbrace E_0, ⋯, E_n, ⋯ \rbrace)$

\[𝕰 ≝ \lbrace E_{i+1} ⟶ E_i \mid i∈ℕ \rbrace\] \[A^+ \vDash 𝕰\]

Si $𝜑 ∈ F_0 (\lbrace E_0, ⋯, E_n, ⋯ \rbrace)$

Lemme : \(A^+ \vDash 𝜑 ⟺ 𝕰 \vDash 𝜑\)

Lemme 2 : $𝕰 \vDash 𝜑$ ssi $\lbrace E_{i+1} ⟶ E_i \mid i≤N \rbrace \vDash 𝜑$

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

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

Les modèles de $𝕰$ sont $\lbrace E_0, ⋯, E_k \rbrace$ (pour $k∈ℕ$) et $\lbrace E_i \mid i∈ℕ \rbrace$

⟶ Pour chaque modèle $\lbrace E_0, ⋯, E_k \rbrace$ (pour $0≤k≤N$), on teste si $\lbrace E_0, ⋯, E_k \rbrace \vDash 𝜑$

Leave a comment