Élimination des quantificateurs

Modèle:Ébauche 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\wedge b=0\wedge c=0)\vee (a=0\wedge b=0)\vee (a=0\wedge \mathrm{\neg }(b^2-4ac<0))$ dans la théorie, car dans cette théorie ax² + bx + c = 0 admet une solution 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(\overline{v},w)$ sans quantificateur il existe une L-formule sans quantificateur $G(\overline{v})$ telle que $T\models \mathrm{\exists }wF(\overline{v},w)\leftrightarrow G(\overline{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:=\mathrm{\neg }{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:=\mathrm{\neg }{H}_2$; soit $F:=H_1\wedge 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\wedge H_4$; soit $F:=\mathrm{\exists }x{H}_1$, par hypothèse de l'induction il existe $H_2$ sans quantificateur telle que $T\models \mathrm{\exists }x{H}_1\leftrightarrow \mathrm{\exists }x{H}_2$, et par hypothèse, il existe $H_3$ sans quantificateur telle que $T\models \mathrm{\exists }x{H}_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,\dots ,x_n,y)$ une formule sans quantificateur, cherchons une formule $G(x_1,\dots ,x_n)$ sans quantificateur telle que $DLO\models F\leftrightarrow G$.

$F$ est sans quantificateur, donc $F$ est équivalente à une formule sous forme disjonctive $\underset{i}{\bigvee }\underset{j}{\bigwedge }{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 \underset{i}{\bigvee }\underset{j}{\bigwedge }{A}_{i,j}(x_1,...,x_n,y)$ si et seulement si $DLO\models \underset{j}{\bigwedge }{A}_{i,j}(x_1,...,x_n,y)$ pour un certain $i$, $F$ est équivalente à une formule de la forme $\underset{i}{\bigwedge }{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 \mathrm{\neg }(x<y)\leftrightarrow (y<x\vee x=y)$, $DLO\models \mathrm{\neg }(x=y)\leftrightarrow (x<y\vee y<x)$, $DLO\models x=x\leftrightarrow \mathrm{\top }$, $DLO\models x<x\leftrightarrow \mathrm{\perp }$ et $DLO\models H\wedge \mathrm{\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 $\mathrm{\perp }.$

S'il existe $i$ tel que $A_i=\mathrm{\perp }$ alors $DLO\models \underset{i}{\bigwedge }{A}_i(x_1,...,x_n,y)\leftrightarrow \mathrm{\perp }$, donc $G:=\mathrm{\perp }$ convient. Supposons que $A_i=\mathrm{\perp }$ 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 $\underset{i}{\bigwedge }{A}_i(x_1,...,x_n,y):=\underset{i\in I}{\bigwedge }{A}_i\wedge \underset{j\in J}{\bigwedge }{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 $\underset{j\in J}{\bigwedge }{A}_j:=\underset{j\in S}{\bigwedge }{x}_j<y\wedge \underset{j\in T}{\bigwedge }y<x_j$. Donc on a deux cas :

• Si $S\cap T=\mathrm{\varnothing }$, alors $G:=\mathrm{\perp }$ convient.

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

• Sinon $DLO\models \underset{j\in J}{\bigwedge }{A}_j\leftrightarrow \underset{i\in S,j\in T}{\bigwedge }{x}_i<x_j$ car l'ordre est dense, donc $G:=\underset{i\in I}{\bigwedge }{A}_i\wedge \underset{i\in S,j\in T}{\bigwedge }{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 de la réciproque

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 \mathrm{\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 \mathrm{\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 \mathrm{\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$ et $N$ deux groupes abéliens divisibles sans torsion, $G$ un sous-groupe commun de $M$ et $N$, $(a_1,...,a_n)\in G^n$ et $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$ à $M$ et $N$ tel que $G$ est un sous-groupe de $H$, puis on montre que $H\models \mathrm{\exists }xF(a_1,...,a_n,x)$ avant de conclure.

Montrons qu'il existe un sous-groupe commun $H$ à $M$ et $N$ tel que $G$ est un sous-groupe de $H$. Posons $X:=G\times 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 classe d'équivalence de $(g,n)$. On définit $+:H^2\to H$ en posant, pour tout $((g,n),(h,m))\in H^2$, $((g,n))+((h,m))=((mg+nh,mn))$.

• $+$ est bien définie : Soient $(g^{\prime },n^{\prime })\in ((g,n))$ et $(h^{\prime },m^{\prime })\in ((h,m))$. On a que $((g^{\prime },n^{\prime }))+((h^{\prime },m^{\prime }))=((m^{\prime }{g}^{\prime }+n^{\prime }{h}^{\prime },m^{\prime }{n}^{\prime })).$ Comme $m^{\prime }{n}^{\prime }(mg+nh)=m^{\prime }{n}^{\prime }mg+m^{\prime }{n}^{\prime }nh=m^{\prime }m{n}^{\prime }g+n^{\prime }n{m}^{\prime }h=mn{m}^{\prime }{g}^{\prime }+mn{n}^{\prime }h=mn(m{g}^{\prime }+n^{\prime }h)$, on a $((m^{\prime }{g}^{\prime }+n^{\prime }{h}^{\prime },m^{\prime }{n}^{\prime }))=((mg+nh,mn))$.

• $(H,+)$ est un groupe : Soit $(((g,n)),((h,m)),((k,l)))\in H^3$. On a :

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

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

$(((g,n))+((h,m)))+((k,l))=((g,n))+(((h,m))+((k,l)))$.

• $(H,+)$ est sans torsion : Soient $((g,n))\in H$ et $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élien : Soit$(((g,m)),((h,n)))\in H^2$. On a $((g,m))+((h,n))=((ng+mh,mn))=((mh+ng,mn))=((h,n))+((g,m))$.

Montrons que $f:G\to H,g\mapsto ((g,1))$ est un homomorphisme injectif. On a :

$f(0)=((0,1))$;

Pour tout $(g,h)\in G^2$, $f(g+h)=((g+h,1))=((g,1))+((h,1))=f(g)+f(h)$;

Pour tout $(g,h)\in G^2$, $g=h$ si et seulement si $((x,1))=((y,1)).$

Montrons que $h:H\to M,((g,n))\mapsto g/n$ est bien défini et est un homomorphisme injectif.

$h$ est bien défini : Soit $(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$;

Pour tout $(((g,m)),((k,n)))\in H^2$, $h(((g,m))+((k,n)))=h(((ng+mk,mn)))=(ng+mk)/(mn)=g/m+k/n=h(((g,m)))+h(((k,n)));$

Pour tout $(((g,m)),((k,n)))\in H^2$, 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 injectif de $H$ dans $N$. Ainsi on peut identifier $H$ avec un sous-groupe commun à $M$ et $N$ contenant $G$.

Montrons que $H\models \mathrm{\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 : $\underset{i}{\bigvee }\underset{j}{\bigwedge }{A}_{i,j}(x_1,...,x_n,y)$ où les $A_{i,j}$ sont des formules atomiques ou des négations de formules atomiques du langage. Quand $\underset{i}{\bigvee }\underset{j}{\bigwedge }{A}_{i,j}(x_1,...,x_n,y)$ est satisfait, il existe $i_0$ tel que $\underset{j}{\bigwedge }{A}_{i_0,j}(x_1,...,xn,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$ sont dans $\mathbb{N}$. Ainsi $\underset{j}{\bigwedge }{A}_{i_0,j}(x_1,...,x_n,y):=(\underset{j\in S}{\bigwedge }(\sum _{i=1}^n{m}_{i,j}{x}_i+m_{j}y=0)\wedge \underset{j\in T}{\bigwedge }(\sum _{i=1}^n{m}_{i,j}{x}_i+m_{j}y=0))$.

S'il existe $j\in S$ tel que $m_j=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 divisible. Donc $b\in H$.

Sinon, $\underset{j}{\bigwedge }{A}_{i_0,j}(x_1,...,x_n,y):=\underset{j\in T}{\bigwedge }(\sum _{i=1}^n{m}_{i,j}{x}_i+m_{j}y=0).$ Comme H est sans torsion, $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 $\underset{j\in T}{\bigwedge }(\sum _{i=1}^n{m}_{i,j}{a}_i+m_{j}y=0).$

Comment $H$ est un sous groupe de $N$, il existe un élément de $N$ qui satisfait $\underset{j\in T}{\bigwedge }(\sum _{i=1}^n{m}_{i,j}{a}_i+m_{j}y=0)$. Par conséquent, $N\models \mathrm{\exists }F(a_1,...,a_n,y)$.

Critère 3

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

1. Pour toute $A\models T_{\mathrm{\forall }}$, il existe une $K\models T$ et un monomorphisme$i:A\to K$ tels que pour tout $N\models T$ et monomorphisme $j:A\to N$, il existe $h:K\to 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,\dots ,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_{\mathrm{\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 \mathrm{\exists }xF(a_1,a_2,...,a_n,x)$. De même $N\models \mathrm{\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 \mathrm{\forall }x\mathrm{\forall }y((x=0\wedge y=0)\to (x.y=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 $\underset{i}{\bigvee }\underset{j}{\bigwedge }{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 \underset{j}{\bigwedge }{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 $\underset{i}{\bigwedge }{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)=\underset{i=1}{\overset{n}{\bigwedge }}{P}_i(X)=0\wedge \underset{j=1}{\overset{m}{\bigwedge }}{Q}_j(X)=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)=\underset{j=1}{\overset{m}{\bigwedge }}{Q}_j(X)=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 $\underset{j=1}{\overset{m}{\bigwedge }}{Q}_j(c)=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 (Modèle:Lien, algorithme de Modèle:Lien) ;
• 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 RackoffModèle:,, de Loos et Modèle:Lien) ;
• théorie linéaire des entiers, dite aussi arithmétique de Presburger.

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

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 Modèle:ISBN
• 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