Next Contents

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 : 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 : 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 :


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 : 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.)



Next Contents