Élimination des quantificateurs

En logique mathématique, ou plus précisément en théorie des modèles, l'élimination des quantificateurs est l'action consistant à trouver une formule sans quantificateur équivalente à une formule donnée contenant éventuellement des quantificateurs dans la théorie considérée d'un certain langage.

Ainsi, si l'on considère la théorie des corps réels clos, le langage de cette théorie est L={+,•,<,0,1} où +,• sont deux symboles de fonction d'arité 2, < est un symbole de relation binaire, et 0,1 sont deux symboles de constante, la L-formule ∃x (ax² + bx + c = 0) est équivalente à la L-formule $(a=0\land b=0\land c=0)\lor (a=0\land b\not =0)\lor (a\not =0\land \lnot (b^{2}-4ac<0))$ dans la théorie, car dans cette théorie ax² + bx + c = 0 admet une racine si et seulement si a, b et c sont tous nuls, ou a est nul mais b est non nul, ou a non nul et $b^{2}-4ac$ est positif.

Définitions

Soient L un langage et T une L-théorie, on dit que T admet l'élimination des quantificateurs si pour toute L-formule F, il existe une L-formule G sans quantificateur telle que $T\models F\leftrightarrow G$. Autrement dit, une théorie T du langage L admet l'élimination des quantificateurs si toute formule du langage L est équivalente à une formule sans quantificateur dans cette théorie.

Intérêt d'élimination des quantificateurs

Les formules sans variables sont souvent plus faciles à décider ; l'algorithme d'élimination des quantificateurs peut donc servir de procédure de décision pour cette théorie. Dans une théorie décidable admettant l'élimination des quantificateurs, il existe un algorithme qui en acceptant une formule donne toujours une formule sans quantificateur. Le seul problème est l'efficacité de l'algorithme.

Elle nous permet aussi de mieux comprendre les ensembles définissables dans une théorie.

Quelques critères d'élimination des quantificateurs

Critère 1

Soit $T$ une L-theorie.

Supposons que pour toute L-formule $F({\bar {v}},w)$ sans quantificateur il existe une L-formule sans quantificateur $G({\bar {v}})$ telle que $T\models \exists wF({\bar {v}},w)\leftrightarrow G({\bar {v}})$.

Alors, T admet l'élimination des quantificateurs.

Preuve

Soit $F(x_{1},x_{2},...,x_{n})$ une L-formule. On montre par l'induction sur la complexité de $F$ qu'il existe une L-formule $G$ sans quantificateur telle que $T\models F\leftrightarrow G$.

Si $|F|=0$ alors posons $G=F$. Supposons que la propriété est vraie pour toutes les formules de complexité strictement plus petite que $n$. Si $|F|=n$, il y a trois cas : soit $F:=\lnot H_{1}$, alors par hypothèse d'induction il existe $H_{2}$ sans quantificateur telle que $H_{1}$ est équivalente à $H_{2}$, il suffit de poser $G:=\lnot H_{2}$; soit $F:=H_{1}\land H_{2}$, alors par hypothèse d'induction il existe $H_{3}$ et $H_{4}$ sans quantificateur telles que $T\models H_{1}\leftrightarrow H_{3}$ et $T\models H_{2}\leftrightarrow H_{4}$, et on pose $G:=H_{3}\land H_{4}$; soit $F:=\exists xH_{1}$, par hypothèse de l'induction il existe $H_{2}$ sans quantificateur telle que $T\models \exists xH_{1}\leftrightarrow \exists xH_{2}$, et par hypothèse, il existe $H_{3}$ sans quantificateur telle que $T\models \exists xH_{2}\leftrightarrow H_{3}$, on pose $G:=H_{3}$.

Exemple: DLO

On montre que $DLO$ (Dense Linear Ordering) admet l’élimination des quantificateurs en vérifiant la condition du critère 1. Autrement dit, soit $F(x_{1},\ldots ,x_{n},y)$ une formule sans quantificateur, cherchons une formule $G(x_{1},\ldots ,x_{n})$ sans quantificateur telle que $DLO\models F\leftrightarrow G$.

$F$ est sans quantificateur, donc $F$ est équivalente à une formule sous forme disjonctive $\bigvee _{i}\bigwedge _{j}A_{i,j}(x_{1},...,x_{n},y)$ où les $A_{i,j}$ sont des formules atomiques (ou leur négation) du langage de $DLO$. Comme $DLO\models \bigvee _{i}\bigwedge _{j}A_{i,j}(x_{1},...,x_{n},y)$ si et seulement si $DLO\models \bigwedge _{j}A_{i,j}(x_{1},...,x_{n},y)$ pour un certain $i$, $F$ est équivalente à une formule de la forme $\bigwedge _{i}A_{i}(x_{1},...,x_{n},y)$ où les $A_{i}$ sont des formules atomiques (ou leur négation) du langage de $DLO$.

Comme $DLO\models \lnot (x<y)\leftrightarrow (y<x\lor x=y)$, $DLO\models \lnot (x=y)\leftrightarrow (x<y\lor y<x)$, $DLO\models x=x\leftrightarrow \top$, $DLO\models x<x\leftrightarrow \bot$ et $DLO\models H\land \top \leftrightarrow H$, on peut supposer que les $A_{i}$ sont de la forme : $y=x_{i},x_{i}=x_{j},y<x_{i},x_{i}<y,x_{i}<x_{j}$, ou $\bot .$

S'il existe $i$ tel que $A_{i}=\bot$ alors $DLO\models \bigwedge _{i}A_{i}(x_{1},...,x_{n},y)\leftrightarrow \bot$, donc $G:=\bot$ convient. Supposons que $A_{i}\not =\bot$ pour tout $i$.

S'il existe $i$ tel que $y=x_{i}$ alors $G:=F[x_{i}/y]$ convient. Donc on peut supposer que $A_{i}$ n'est pas de la forme $y=x_{i}$ pour tout $i$.

Donc les $A_{i}$ sont de la forme : $x_{i}=x_{j},y<x_{i},x_{i}<y$, ou $x_{i}<x_{j}$.

Ainsi $\bigwedge _{i}A_{i}(x_{1},...,x_{n},y):=\bigwedge _{i\in I}A_{i}\land \bigwedge _{j\in J}A_{j}$ où les $A_{i}$ sont de la forme $x_{i}=x_{j}$ ou $x_{i}<x_{j}$, et les $A_{j}$ sont de la forme $y<x_{i}$ ou $x_{i}<y$.

On a que $\bigwedge _{j\in J}A_{j}:=\bigwedge _{j\in S}x_{j}<y\land \bigwedge _{j\in T}y<x_{j}$. Donc on a deux cas :

• Si $S\cap T\not =\emptyset$, alors $G:=\bot$ convient.

• Sinon si $S=\emptyset$ ou $T=\emptyset$, alors $G:=\top$ convient car l'ordre est sans extrémités.

• Sinon $DLO\models \bigwedge _{j\in J}A_{j}\leftrightarrow \bigwedge _{i\in S,j\in T}x_{i}<x_{j}$ car l'ordre est dense, donc $G:=\bigwedge _{i\in I}A_{i}\land \bigwedge _{i\in S,j\in T}x_{i}<x_{j}$ convient.

Critère 2

Soit $T$ une L−théorie.

Supposons que pour toute L-formule sans quantificateur $F(x_{1},x_{2},...,x_{n},y)$, si $M$ et $N$ sont deux modèles de $T$, $A$ est une sous-structure commune de $M$ et $N$, $a_{1},a_{2},...,a_{n}$ des éléments de l’ensemble de base de $A$, et il existe $b\in M$ tel que $M\models F(a_{1},a_{2},...a_{n},b)$, alors il existe $c$ dans le domaine de $N$ tel que $N\models F(a_{1},a_{2},...,a_{n},c)$.

Alors, $T$ admet l’élimination des quantificateurs.

Preuve

Montrons la réciproque (la preuve directe est plus délicate). Soit $F(x_{1},...,x_{n},y)$ une L-formule sans quantificateur. Soient $M$,$N$ deux modèles de $T$, $A$ une sous-structure commune de $M$ et $N$, et $a_{1},a_{2},...a_{n}$ des éléments de $A$. Supposons que $M\models \exists yF(a_{1},a_{2},...a_{n},y)$. Alors par élimination des quantificateurs, il existe une L-formule sans quantificateur $G(x_{1},...,x_{n})$ telle que $T\models \exists yF(x_{1},...,x_{n},y)\leftrightarrow G(x_{1},...,x_{n})$, et $M\models G(a_{1},...,a_{n})$. Or, comme $A$ est une sous-structure de $M$ et $G(x_{1},...,x_{n})$ est sans quantificateur, $M\models G(a_{1},...,a_{n})$ équivaut à $A\models G(a_{1},...,a_{n})$, équivalant, de même, à $N\models G(a_{1},...,a_{n})$, d'où enfin $N\models \exists yF(a_{1},a_{2},...a_{n},y)$.

Exemple: DAG

On montre que la théorie de groupe abélien divisible sans torsion ($DAG$) admet l’élimination des quantificateurs en montrant qu'elle vérifie la condition du critère 2.

Soit $F(x_{1},...,x_{n},y)$ une formule sans quantificateur. Soient $M$,$N$ deux groupes abélians divisibles sans torsion, $G$ un sous-groupe commun de $M$ et $N$, $(a_{1},...,a_{n})\in G^{n},h\in M$ tels que $M\models F(a_{1},...,a_{n},h)$. On montre d'abord qu'il existe un sous-groupe commun $H$ de $M$ et $N$ tel que $G$ est un sous-groupe de $H$, et puis on montre que $H\models \exists xF(a_{1},...,a_{n},x)$ avant de conclure.

Montrons qu'il existe un sous-groupe commun $H$ de $M$ et $N$ tel que $G$ est une sous-groupe de $H$: Posons $X:=\{(g,n):g\in G,n\in \mathbb {N} ^{*}\}$. On définit une relation d'équivalence $\sim$ sur $X$ par $(g,n)\sim (h,m)$ si et seulement si $mg=nh$. Posons $H=X/\sim$. Notons $((g,n))$ la $\sim ~$-classe de $(g,n)$. On définit $+:H^{2}\rightarrow H$ en posant $(((g,n)),((h,m)))=((mg+nh,mn))$.

$+$ est bien définie: Soient$(g',n')\in ((g,n))\ et\ (h',m')\in ((h,m)).$ On a que $((g',n'))+((h',m'))=((m'g'+n'h',m'n')).$ Comme $m'n'(mg+nh)=m'n'mg+m'n'nh=m'mn'g+n'nm'h=mnm'g'+mnn'h=mn(mg'+n'h),((m'g'+n'h',m'n'))=((mg+nh,mn))$

$(H,+)$ est un groupe: Soient $((g,n)),((h,m)),((k,l))\in H.$ On a $((0,1))+((g,n))=((g,n))$;

$((-g,n))+((g,n))=((0,nn))=((0,1))$;

$(((g,n))+((h,m)))+((c,l))=((g,n))+(((h,m))+((c,l)))$

$(H,+)$ est sans torsion: Soit $((g,n))\in H,m\in \mathbb {N} ^{*}\ tels\ que\ m((g,n))=((0,1)).$ On a donc $((mg,n))=((0,k)).$ Donc $kmg=(km)g=0$ Ainsi $g=0$ car $M$ est sans torsion.

$(H,+)$ est divisible: Soit $((g,n))\in H.\ On\ a\ m((g,mn))=((g,n)).$

$(H,+)$ est abélian: Soient $((g,m)),((h,n))\in H.\ On\ a\ ((g,m))+((h,n))=((ng+mh,mn))=((mh+ng,mn))=((h,n))+((g,m))$

Monstrons que $f:G\rightarrow H$ définie par $f(g)=((g,1))$ est une homomorphisme injectif: $f(0)=((0,1))$;

$\quad$ soient $g,h\in G,$ alors $f(g+h)=((g+h,1))=((g,1))+((h,1))=f(g)+f(h)$;

$\quad$ soient $g,h\in G,\ g=h$ si et seulement si $((x,1))=((y,1)).$

Montrons que $h:H\rightarrow M$ définie par $h((g,n))=g/n$ bien défini et est un homomorphisme injectif:

$h$ est bien défini: Soient $(k,m)\in ((g,n)),$ alors $mg=nk$. Donc $f(g,n)=g/n=(mg)/mn=(nk/mn)=k/m.$

$h$ est un homomorphisme injectif: $h(((0,1)))=0/1=0$;

$\quad$ soient $((g,m)),((k,n))\in H$, $h(((g,m))+((k,n)))=h(((ng+mk,mn)))=(ng+mk)/(mn)=g/m+k/n=h(((g,m)))+h(((k,n)));$

$\quad$ soient $((g,m)),((k,n))\in H$, si $((g,m))=((k,n))$, alors $ng=mk$, donc $mn(g/m)=mn(k/n)$, donc $g/m=k/n$; si$g/m=k/n$, alors $ng=nm(g/m))=nm(k/n)=mk.$

De même, il existe aussi un homomorphisme injective de $H$ dans $N$. Ainsi on peut identifier $H$ avec un sous-groupe commun conenant $G$ de $M$ et $N$.

Montrons que $H\models \exists xF(a_{1},a_{2},...,a_{n},x)$:

$F(x_{1},...,x_{n},y)$ est une formule sans quantificateur, donc elle est équivalente à une formule sous forme disjonctive: $\bigvee _{i}\bigwedge _{j}A_{i,j}(x_{1},...,x_{n},y)$ où les $A_{i,j}$ sont des formules atomiques ou des négations de formules atomique du langage. Quand $\bigvee _{i}\bigwedge _{j}A_{i,j}(x_{1},...,x_{n},y)$ est satisfait, il existe $i_{0}$ tel que $\bigwedge _{j}A_{i_{0},j}(x_{1},...,x{n},y)$ est satisfait.

Comme dans le langage, le seul symbole de prédicat est le symbole $=$ et le seul symbole de fonction est $+$, une formule atomique dans ce langage est de la forme $\sum _{i=1}^{n}(m_{i,j}x_{i}+m_{j}y=0)$ où les $m_{i,j},m_{j}\in \mathbb {N}$. Ainsi $\bigwedge _{j}A_{i_{0},j}(x_{1},...,x_{n},y):=(\bigwedge _{j\in S}(\sum _{i=1}^{n}m_{i,j}x_{i}+m_{j}y=0)\land \bigwedge _{j\in T}(\sum _{i=1}^{n}m_{i,j}x_{i}+m_{j}y\not =0).)$

S'il existe $j\in S$ tel que $m_{j}\not =0$, alors comme $M\models F(a_{1},...,a_{n},b)$,$b={\frac {\sum _{i=1}^{n}m_{i,j}(-a_{i})}{m_{j}}}\in G$ car G est un groupe disivisble. Donc $b\in H$.

Sinon, $\bigwedge _{j}A_{i_{0},j}(x_{1},...,x_{n},y):=\bigwedge _{j\in T}(\sum _{i=1}^{n}m_{i,j}x_{i}+m_{j}y\not =0).$ Comme H est sans torsion, donc $H$ est infini, car sinon pour tout $x\in H,|H|x=0$. Comme pour tout $j\in T,\{w\in H|\sum _{i=1}^{n}m_{i,j}a_{i}+m_{j}y=0\}$ est fini, il existe un élément dans $H$ qui satisfait $\bigwedge _{j\in T}(\sum _{i=1}^{n}m_{i,j}a_{i}+m_{j}y\not =0).$

Comment $H$ est une sous groupe de $N$, il existe un élément de $N$ satisfait $\bigwedge _{j\in T}(\sum _{i=1}^{n}m_{i,j}a_{i}+m_{j}y\not =0)$, par conséquent, $N\models \exists F(a_{1},...,a_{n},y)$

Critère 3

Soit $T$ une L−théorie telle que

1. Pour toute $A\models T_{\forall }$, il existe une $K\models T$ et un monomorphisme$i:A\rightarrow K$ tels que pour tout $N\models T$ et monomorphisme $j:A\rightarrow N$, il existe $h:K\rightarrow N$ tel que $j=h\circ i$.

2. Si $M,N$ sont deux modèles de $T$ et $M$ est sous-structure de $N$ alors pour toute L-formule $F(x_{1},...,x_{n},w)$ et tout $a_{1},a_{2},\ldots ,a_{n}$ dans la domaine de $M$, s'il existe $b$ dans la domaine de $N$ tel que $F(a_{1},a_{2},...,a_{n},b)$ est satisfaite dans $N$, alors elle l'est aussi dans $M$.

Alors, $T$ admet l'élimination des quantificateurs.

Preuve

Soit $F(x_{1},...,x_{n},y)$ une L-formule sans quantificateur. Supposons que $M,N$ soient deux modèles de $T$, $A$ une sous-structure commune de $M$ et $N$ , $a_{1},a_{2},...,a_{n}$ des éléments dans $A$ et $b$ un élément de $M$ tels que $M\models F(a_{1},a_{2},...,a_{n},b)$. Montrons qu'il existe $c$ dans $N$ tel que $N\models F(a_{1},a_{2},...,a_{n},c)$ et puis conclure par le critère 1:

Comme $M\models T$ et que $A$ est une sous-structure de $M$, on a que $A\models T_{\forall }$. Par hypothèse 1) il existe $K\models T$ telle que pour toute $Q\models T$ qui est extension de $A$, $K$ est une sous-structure de $Q$. Par conséquent, $K$ est sous-structure de $M$ et de $N$.

Comme $M\models F(a_{1},a_{2},...,a_{n},b),F$ est une formule sans quantificateur, $K$ est une sous-structure de $M$ et que les formules sans quantificateurs sont préservées par la sous-structure, on a que $K\models \exists xF(a_{1},a_{2},...,a_{n},x)$. De même $N\models \exists xF(a_{1},a_{2},...,a_{n},x)$.

Ainsi on conclut par le critère 2 que $T$ admet l'élimination des quantificateurs.

Exemple: Corps algébriquement clos

On note $ACF$ pour la théorie des corps algébriquement clos. Pour démontrer que $ACF$ admet l'élimination des quantificateurs, on montre d'abord l'ensemble $ACFU$ des conséquences universelles de la théorie des corps algébriquement clos est la théorie des anneaux intègres. Et puis, on montre que $ACF$ vérifie les conditions du critère 3 pour conclure.

Montrons que $ACFU$ est la théorie des anneaux intègres: Soit $A$ un anneau intègre. Soit $K$ corps-extension algébrique du corps de fraction de $A$. On a que $K$ est un modèle de $ACF$. Comme il existe un homomorphisme injectif de $A$ dans le corps de fraction de $A$, et qu'il existe un homomorphisme injective du corps de fraction de $A$ dans $K$, on déduit que $A$ est un sous-anneau de $K$. Donc $A\models ACFU$. Soit $B\models ACFU$. En particulier, $B\models \forall x\forall y((x\not =0\land y\not =0)\rightarrow (x.y\not =0))$. Comme de plus tous les axiomes de la théorie d'anneaux sont dans $ACFU$, $B$ est un anneau intègre.

Montrons que $ACF$ vérifie la première condition du critère 3: Soit $B$ un modèle de $ACFU$. $B$ est un anneau intègre. Soit $C$ le corps-extension algébrique du corps de fraction de $B$. Soit $D$ un modèle de $ACF$ tel que $B$ est un sous-anneau de $D$. Comme $D$ est un corps contenant $B$, donc $D$ contenant le corps de fraction de $B$. Et comme $D$ est algébriquement clos, $D$ contient, par définition, $C$ le corps-extension algébrique de $B$.

Montrons que $ACF$ vérifie la deuxième condition du critère 3: Soient $M,N\models ACF$ tels que $M$ est une sous-structure de $N$, $F(x_{1},...,x_{n},y)$ une L-formule sans quantificateur, $a_{1},...,a_{n}$ éléments de la domaine de $M$. Supposons qu'il existe $b$ élément de la domaine de $N$ tel que $N\models F(a_{1},a_{2},...,a_{n},b)$. Montrons qu'il existe $c$ élément de la domaine de $M$ tel que $M\models F(a_{1},...,a_{n},c)$. $F(x_{1},...,x_{n},y)$ est une formule sans quantificateur donc elle est équivalente à une formule sous forme disjonctive $\bigvee _{i}\bigwedge _{j}A_{ij}(x_{1},...,x_{n},y)$ où les $A_{ij}(x_{1},...,x_{n},y)$ sont des formules atomiques ou des négations de formules atomiques. $N\models F(x_{1},...,x_{n},y)$ si et seulement si $N\models \bigwedge _{j}A_{ij}(x_{1},...,x_{n},y)$ pour un certain $i$. On peut donc supposer, sans perte de généralité, que F est une formule de la forme $\bigwedge _{i}A_{i}(x_{1},...,x_{n},y)$ où les $Ai(x_{1},...,x_{n},y)$ sont des formules atomiques ou des négations de formules atomiques. Et le langage de ACF est le langage d'anneau, une formule atomique $A(x_{1},...,x_{n})$ est de la forme $P(x_{1},...,x_{n})=0$ où P est une polynôme de $\mathbb {Z} [X_{1},X_{2},...,X_{n}]$. $F(a_{1},...,a_{n},X)$ est un polynôme de $M[X]$. Donc il existe $P_{1},P_{2},...,P_{n},Q_{1},Q_{2},...,Q_{m}$ dans $M[X]$ tels que $F(a_{1},...,a_{n},X)=\bigwedge _{i=1}^{n}P_{i}(X)=0\wedge \bigwedge _{j=1}^{m}Q_{j}(X)\not =0$. On a deux cas:

S'il existe un polynôme $P_{k}$ non nul, alors comme on a $N\models P_{i}(b)=0$ pour tout $i$, on a en particulier $N\models P_{k}(b)=0$. Comme M est un sous-corps algébriquement clos de N et b est un élément de la domaine de N, on a que b est un élément de la domaine de M.

Sinon, alors $F(a_{1},...,a_{n},X)=\bigwedge _{j=1}^{m}Q_{j}(X)\not =0$. Soient $S_{j}$ l'ensemble de racines de $Q_{j}(X)$ pour tout $j$. On sait que $S_{j}$ est fini pour tout $j$ et que $M$ est infini donc il existe $c$ dans $|M|-\bigcup _{j=1}^{m}S_{j}$ tel que $\bigwedge _{j=1}^{m}Q_{j}(c)\not =0$. Donc il existe $c$ dans la domaine de M tel que $M\models F(a_{1},...,a_{n},c)$.

Exemples

Exemples de théories admettant l'élimination des quantificateurs :

• corps réels clos (théorème de Tarski-Seidenberg (en), algorithme de décomposition algébrique cylindrique (en)) ;
• corps algébriquement clos de caractéristique quelconque ou fixée (par exemple via les bases de Gröbner et le théorème d'extension) ;
• théorie linéaire des rationnels ou des réels (algorithmes de Ferrante et Rackoff, de Loos et Weispfenning (de)) ;
• théorie linéaire des entiers, dite aussi arithmétique de Presburger.

Toutes ces théories sont donc modèle-complètes (en).

Conséquence

Modèle-complétude

Soit $T$ une $L$-théorie admettant l'élimination des quantificateurs. Soient $M,N$ deux modèles de $T$ tels que $M$ est une sous-structure de $N$. Soit $F$ une $L$-formule et $s$ une assignation des variables dans $M$. Par l'élimination des quantificateurs, il existe une $L$-formule sans quantificateur $G$ qui est équivalente à $F$ dans $T$. On a que $M\models F[s]$ si et seulement si $M\models G[s]$ et que $N\models F[s]$ si et seulement si $N\models G[s]$. Comme l'injection canonique de $M$ dans $N$ est un homomorphisme injectif et que $G$ est une formule sans quantificateur, on a que $M\models G[s]$ si et seulement si $N\models G[s]$. On conclut que $M\models F[s]$ si et seulement si $N\models F[s]$. Donc $M$ est une sous-structure élémentaire de $N$. Ainsi $T$ est modèle-complète (par définition).

Voir aussi

Articles connexes

• Skolémisation
• Théorème de Herbrand

Bibliographie

• Jean-Louis Krivine et Georg Kreisel, Éléments de logique mathématique (théorie des modèles), Paris, Dunod, 1966, chap. 4, pdf
• Jean-François Pabion, Logique mathématique, chapitre VI « Élimination des quantificateurs » pp. 191-210, Hermann, Paris 1976 (ISBN 2-7056 5830-0)
• René David, Karim Nour, Christophe Raffalli, Introduction à la logique-theorie de la démonstration, 2e édition, Dunod
• David Marker, Model Theory: An introduction, Springer
• René Cori, Daniel Lascar, Logique mathématique 2, Dunod