1 Définitions
1.1 Syntaxe
La syntaxe des logiques d'ordre un est à deux niveaux : un pour les
termes, qui représentent les objets étudiés, et un pour les
formules, autrement dit les propriétés de et entre ces objets.
Soit V un ensemble infini dénombrable de variables
d'individu x, y, ..., F un ensemble au plus
dénombrable de symboles de fonction f, g, ..., et
P un ensemble au plus dénombrable, et disjoint du
précédent, de symboles de prédiat P, Q, ...
Soit aussi m:FÈP®N une application dite
d'arité; l'arité de f est définie par m=m(f).
Définition 1 [Termes, Formules]
Nous appelons termes s, t, ... les éléments du
plus petit ensemble T tel que :
- toute variable est un terme;
- pour tout fÎF d'arité m, pour tous termes t1,
..., tm dans T, le (m+1)-uplet
(f,t1,...,tm) est aussi dans T.
Ce (m+1)-uplet, appelé l'application de f à t1,
..., tm, est écrit f(t1,...,tm) par
commodité.
Nous appelons formule atomique ou atome A, B,
... toute application P(t1,...,tm) d'un symbole de
prédicat P d'arité m à m termes.
Les formules F, Y, ... sont les formules
atomiques, les négations ¬ F de formules, les conjonctions
FÙ F', les disjonctions FÚ F', les
implications FÞ F', les quantifications
universelles " x· F et les quantifications
existentielles $ x· F.
Nous écrirons aussi " x1x2... xn· F
pour " x1· " x2·... " xn·
F, et $ x1x2... xn· F pour $
x1· $ x2·... $ xn· F.
Intuitivement, les termes représentent des valeurs dans un domaine
donné d'objets. Les constantes sont codées comme des symboles de
fonction d'arité 0, et les autres symboles de fonctions
représentent des opérations de base sur les valeurs (addition,
multiplication, par exemple). Les formules atomiques représentent
des propriétés de base des valeurs (par exemple, être
inférieur ou égal à, être impair, etc.), et sont combinées
entre elles à l'aide des connecteurs propositionnels usuels, ainsi
que des quantifications : " x· F (``pour tout x,
F'') signifie que, si l'on interprète F comme une fonction
x |® f(x) envoyant une valeur dénotée x vers la valeur de
vérité de F, alors f(v) est vraie de toutes les valeurs
v; de même, $ x· F (``il existe x tel que
F'') est vraie dès que f(v) est vraie pour au moins une
valeur v.
Définition 2 [Variables libres, liées] Si t est un terme ou une formule, nous définissons l'ensemble
fv(t) de ses variables libres et l'ensemble bv(t) de
ses variables liées par récurrence structurelle :
- fv(x)={x}, bv(x)=Ø pour tout xÎV;
- fv(f(t1, ..., tm))= fv(t1)È ... È
fv(tm), bv(f(t1, ..., tm))= Ø;
- fv(P(t1, ..., tm))= fv(t1)È ... È
fv(tm), bv(P(t1, ..., tm))= Ø;
- fv(¬ F)=fv(F), bv(¬ F)=bv(F);
- fv(FÚ F')= fv(FÙ F')= fv(FÞ
F')= fv(F)Èfv(F'), bv(FÚ F')=
bv(FÙ F')= bv(FÞ F')= bv(F)È
bv(F');
- fv(" x· F)=fv($ x·
F)=fv(F)\{x}, bv(" x·
F)=bv($ x· F)=bv(F)È{x}.
Un terme ou une formule est dit clos si l'ensemble de ses
variables libres est vide. Un énoncé est une formule
close.
Une théorie T est un ensemble d'énoncés.
Contrairement au cas propositionnel, une variable x peut
apparaître dans une formule sans y apparaître libre : par
exemple, " x· P(x) n'a pas de variable libre, et x
n'apparaît que liée (ici, par la quantification universelle).
Comme dans le cas propositionnel, nous pouvons définir des substitutions,
à ceci près que nous ne remplaçons pas des atomes mais
des variables d'individu. Les définitions sont les mêmes,
parce qu'en fait ce sont des définitions sur des éléments
d'algèbres libres arbitraires :
Définition 3 [Substitution] Une substitution s est une application de V vers
T telle que l'ensemble dom s={xÎV|
x¹s(x)}, appelé le domaine de s, est
fini.
L'image de s est par définition
rng s={s(x)| xÎdom s}, et on pose
yield s=È{fv(t)| tÎrng s}.
Nous écrivons aussi s sous la forme
[s(x1)/x1,...,s(xn)/xn], où
x1, ..., xn contiennent toutes les variables de
dom s et sont distinctes deux à deux.
En particulier, [] est la substitution vide (ou identité).
Comme dans le cas propositionnel, s s'étend en un morphisme
unique t|® ts de T vers T tel que :
- xs=s(x)
- f(t1, ..., tm)s= f(t1s, ...,
tms)
Définition 4 [Instances] Soit t un terme. Ses instances sont tous les termes de la forme
ts, où s est une substitution.
La composition ss' de deux substitutions est
définie par t(ss')=(ts)s'.
Une substitution s' est dite moins générale que
s, ce que nous notons s'£s, si et seulement
s'il existe une substitution s'' telle que
ss''=s'.
La composition de substitutions est bien définie (exercice). De
plus, elle est associative et a [] comme élément neutre, et
£ est un préordre. Intuitivement, s' est moins
générale que s si et seulement si toutes les instances de
ts' sont aussi des instances de ts, pour tout terme t;
en bref, une substitution est plus générale qu'une autre si elle a
au moins toutes les instances de l'autre.
Nous étendons ensuite la substitution aux formules par récurrence
structurelle :
- P(t1, ..., tm)s= P(t1s, ...,
tms)
- (¬ F)s=¬ (Fs)
- (FÅ F')s=FsÅ F's, où
ÅÎ{Ú,Ù,Þ}
- pour tout QÎ{",$}, (Q x· F)s=(Q
x'· F[x'/x]s), où x' est une variable hors de
yield sÈ(fv(F)\{x}).
Comme la dernière règle n'est pas déterministe, il y a plusieurs
instances d'une formule quantifiée par s. Cependant, toutes
ces formules seront équivalentes tant sémantiquement que
syntaxiquement. Le fait de transformer Q x· F en Q x'·
F[x'/x] avec x'Ïfv(F)\{x} sera bénin, et
est appelé a-renommage. (Exercice : vérifier que
les règles sémantiques de la section 2 et les
systèmes de preuve de la section 3 sont
effectivement invariants par a-renommage.)