É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 ${\displaystyle (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 ${\displaystyle b^{2}-4ac}$ est positif.

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 ${\displaystyle 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.

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.

Soit ${\displaystyle T}$ une L-theorie.

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

Alors, T admet l'élimination des quantificateurs.

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

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

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

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

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

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

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

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

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

On a que ${\displaystyle \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 ${\displaystyle S\cap T\not =\emptyset }$, alors ${\displaystyle G:=\bot }$ convient.

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

• Sinon ${\displaystyle 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 ${\displaystyle G:=\bigwedge _{i\in I}A_{i}\land \bigwedge _{i\in S,j\in T}x_{i}<x_{j}}$ convient.

Soit ${\displaystyle T}$ une L−théorie.

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

Alors, ${\displaystyle T}$ admet l’élimination des quantificateurs.

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

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

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

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

${\displaystyle +}$ est bien définie: Soient${\displaystyle (g',n')\in ((g,n))\ et\ (h',m')\in ((h,m)).}$ On a que ${\displaystyle ((g',n'))+((h',m'))=((m'g'+n'h',m'n')).}$ Comme ${\displaystyle 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))}$

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

${\displaystyle ((-g,n))+((g,n))=((0,nn))=((0,1))}$;

${\displaystyle (((g,n))+((h,m)))+((c,l))=((g,n))+(((h,m))+((c,l)))}$

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

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

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

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

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

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

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

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

${\displaystyle h}$ est un homomorphisme injectif: ${\displaystyle h(((0,1)))=0/1=0}$;

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

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

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

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

${\displaystyle F(x_{1},...,x_{n},y)}$ est une formule sans quantificateur, donc elle est équivalente à une formule sous forme disjonctive: ${\displaystyle \bigvee _{i}\bigwedge _{j}A_{i,j}(x_{1},...,x_{n},y)}$ où les ${\displaystyle A_{i,j}}$ sont des formules atomiques ou des négations de formules atomique du langage. Quand ${\displaystyle \bigvee _{i}\bigwedge _{j}A_{i,j}(x_{1},...,x_{n},y)}$ est satisfait, il existe ${\displaystyle i_{0}}$ tel que ${\displaystyle \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 ${\displaystyle =}$ et le seul symbole de fonction est ${\displaystyle +}$, une formule atomique dans ce langage est de la forme ${\displaystyle \sum _{i=1}^{n}(m_{i,j}x_{i}+m_{j}y=0)}$ où les ${\displaystyle m_{i,j},m_{j}\in \mathbb {N} }$. Ainsi ${\displaystyle \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 ${\displaystyle j\in S}$ tel que ${\displaystyle m_{j}\not =0}$, alors comme ${\displaystyle M\models F(a_{1},...,a_{n},b)}$,${\displaystyle b={\frac {\sum _{i=1}^{n}m_{i,j}(-a_{i})}{m_{j}}}\in G}$ car G est un groupe disivisble. Donc ${\displaystyle b\in H}$.

Sinon, ${\displaystyle \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 ${\displaystyle H}$ est infini, car sinon pour tout ${\displaystyle x\in H,|H|x=0}$. Comme pour tout ${\displaystyle 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 ${\displaystyle H}$ qui satisfait ${\displaystyle \bigwedge _{j\in T}(\sum _{i=1}^{n}m_{i,j}a_{i}+m_{j}y\not =0).}$

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

Soit ${\displaystyle T}$ une L−théorie telle que

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

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

Alors, ${\displaystyle T}$ admet l'élimination des quantificateurs.

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

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

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

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

On note ${\displaystyle ACF}$ pour la théorie des corps algébriquement clos. Pour démontrer que ${\displaystyle ACF}$ admet l'élimination des quantificateurs, on montre d'abord l'ensemble ${\displaystyle 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 ${\displaystyle ACF}$ vérifie les conditions du critère 3 pour conclure.

Montrons que ${\displaystyle ACFU}$ est la théorie des anneaux intègres: Soit ${\displaystyle A}$ un anneau intègre. Soit ${\displaystyle K}$ corps-extension algébrique du corps de fraction de ${\displaystyle A}$. On a que ${\displaystyle K}$ est un modèle de ${\displaystyle ACF}$. Comme il existe un homomorphisme injectif de ${\displaystyle A}$ dans le corps de fraction de ${\displaystyle A}$, et qu'il existe un homomorphisme injective du corps de fraction de ${\displaystyle A}$ dans ${\displaystyle K}$, on déduit que ${\displaystyle A}$ est un sous-anneau de ${\displaystyle K}$. Donc ${\displaystyle A\models ACFU}$. Soit ${\displaystyle B\models ACFU}$. En particulier, ${\displaystyle 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 ${\displaystyle ACFU}$, ${\displaystyle B}$ est un anneau intègre.

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

Montrons que ${\displaystyle ACF}$ vérifie la deuxième condition du critère 3: Soient ${\displaystyle M,N\models ACF}$ tels que ${\displaystyle M}$ est une sous-structure de ${\displaystyle N}$, ${\displaystyle F(x_{1},...,x_{n},y)}$ une L-formule sans quantificateur, ${\displaystyle a_{1},...,a_{n}}$ éléments de la domaine de ${\displaystyle M}$. Supposons qu'il existe ${\displaystyle b}$ élément de la domaine de ${\displaystyle N}$ tel que ${\displaystyle N\models F(a_{1},a_{2},...,a_{n},b)}$. Montrons qu'il existe ${\displaystyle c}$ élément de la domaine de ${\displaystyle M}$ tel que ${\displaystyle M\models F(a_{1},...,a_{n},c)}$. ${\displaystyle F(x_{1},...,x_{n},y)}$ est une formule sans quantificateur donc elle est équivalente à une formule sous forme disjonctive ${\displaystyle \bigvee _{i}\bigwedge _{j}A_{ij}(x_{1},...,x_{n},y)}$ où les ${\displaystyle A_{ij}(x_{1},...,x_{n},y)}$ sont des formules atomiques ou des négations de formules atomiques. ${\displaystyle N\models F(x_{1},...,x_{n},y)}$ si et seulement si ${\displaystyle N\models \bigwedge _{j}A_{ij}(x_{1},...,x_{n},y)}$ pour un certain ${\displaystyle i}$. On peut donc supposer, sans perte de généralité, que F est une formule de la forme ${\displaystyle \bigwedge _{i}A_{i}(x_{1},...,x_{n},y)}$ où les ${\displaystyle 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 ${\displaystyle A(x_{1},...,x_{n})}$ est de la forme ${\displaystyle P(x_{1},...,x_{n})=0}$ où P est une polynôme de ${\displaystyle \mathbb {Z} [X_{1},X_{2},...,X_{n}]}$. ${\displaystyle F(a_{1},...,a_{n},X)}$ est un polynôme de ${\displaystyle M[X]}$. Donc il existe ${\displaystyle P_{1},P_{2},...,P_{n},Q_{1},Q_{2},...,Q_{m}}$ dans ${\displaystyle M[X]}$ tels que ${\displaystyle 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 ${\displaystyle P_{k}}$ non nul, alors comme on a ${\displaystyle N\models P_{i}(b)=0}$ pour tout ${\displaystyle i}$, on a en particulier ${\displaystyle 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 ${\displaystyle F(a_{1},...,a_{n},X)=\bigwedge _{j=1}^{m}Q_{j}(X)\not =0}$. Soient ${\displaystyle S_{j}}$ l'ensemble de racines de ${\displaystyle Q_{j}(X)}$ pour tout ${\displaystyle j}$. On sait que ${\displaystyle S_{j}}$ est fini pour tout ${\displaystyle j}$ et que ${\displaystyle M}$ est infini donc il existe ${\displaystyle c}$ dans ${\displaystyle |M|-\bigcup _{j=1}^{m}S_{j}}$ tel que ${\displaystyle \bigwedge _{j=1}^{m}Q_{j}(c)\not =0}$. Donc il existe ${\displaystyle c}$ dans la domaine de M tel que ${\displaystyle M\models F(a_{1},...,a_{n},c)}$.

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^[1] (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^[2],[3], de Loos et Weispfenning (de)^[4]) ;
• théorie linéaire des entiers, dite aussi arithmétique de Presburger.

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

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

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

• 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

• Portail des mathématiques
• Portail de la logique