Élimination des quantificateurs

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)}$.

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