Next Contents

1  Syntaxe

La syntaxe de la logique propositionnelle est fondée sur des variables de proposition ou atomes que nous notons avec des lettres majuscules prises au début de l'alphabet, A, B, C, etc., possiblement avec des indices ou des primes. Ces lettres sont censées représenter des propriétés de base, qui sont soit vraies soit fausses. Ces variables sont combinées au moyens de connecteurs logiques pour former des formules ou propositions, que nous notons par des lettres grecques majuscules comme F, Y.


Définition 1   Soit X un ensemble infini dit de variables de proposition. L'ensemble F des formules propositionnelles est le plus petit contenant toutes les variables, et tel que si F et F' sont des formules, alors FÙF', FÚF', FÞF' et ¬F sont des formules.


Ceci fait des formules des objets en forme d'arbre, où chaque noeud est appelé une sous-formule. Une sous-formule de F est dite stricte si elle n'est pas F elle-même. En forme textuelle, nous utilisons des parenthèses et des priorités pour éliminer les ambiguïtés: ¬ est plus prioritaire que Ù, qui l'est plus que Ú, qui l'est plus que Þ. Donc FÙF'ÚF'' est (FÙF')ÚF'', ¬FÚF' représente (¬F)ÚF', et FÙF'ÞF''ÚF''' (FÙF')Þ(F'ÚF'''), en particulier. De plus, Ù et Ú sont associatifs à gauche, i.e. FÙF'ÙF'' représente (FÙF')ÙF'' et FÚF'ÚF'' (FÚF')ÚF''. Et Þ est associatif à droite, i.e. FÞF'ÞF'' représente FÞ(F'ÞF'').

Nous définissons aussi des abréviations pour d'autres opérations. Par exemple, l'équivalence logique Û est définie par: FÛF' égale (FÞF')Ù(F'ÞF).

Nous aurions pu aussi définir moins de connecteurs et faire de ceux qui restent des abréviations. Par exemple, nous aurions pu définir uniquement ¬ et Ú, et poser FÙF' égal à ¬((¬F)Ú(¬F')), et FÞF' égal à ¬FÚF'. Ceci n'aurait rien changé pour ce qui est de la logique classique, que nous développons ici. Mais cela aurait changé beaucoup de choses en logique intuitionniste, par exemple.


Définition 2  L'ensemble des variables libres fv(F) d'une formule F est défini par récurrence structurelle par :
En somme, une variable est libre dans F si et seulement si elle apparaît à une feuille de F.

Une autre notion utile est :


Définition 3  Une substitution s est une application des variables propositionnelles vers les formules, telle que s(A)=A pour tout A sauf un nombre fini.

Le domaine de s, dom s, est l'ensemble (fini) de variables A telles que s(A)¹ A. Nous notons [F1/A1, ..., Fn/An] la substitution de domaine {A1, ..., An} qui envoie chaque variable Ai vers Fi, 1£ i£ n, où les Ai sont supposées distinctes deux à deux. En particulier, [] est la substitution vide.

Toute substitution s s'étend de façon unique à toutes les formules par : Nous notons Fs l'image de F par s définie ci-dessus, et nous l'appelons l'application de s à F.


En somme, on peut voir s comme un ensemble fini d'opérations de remplacement Fi/Ai, remplaçant Ai par Fi. Fs est la formule F où toutes les variables Ai sont remplacées par Fi. Ce remplacement doit être effectué en parallèle: par exemple, le fait d'appliquer [B/A,C/B] à A donne B, pas C, comme ce serait le cas si nous avions appliqué B/A puis C/B.


Théorème 4   Soit s = [F1/A1, ..., Fn/An] et s' = [F'1/A'1, ..., F'n'/A'n'].

Il existe une substitution s'' unique telle que Fs'' = (Fs)s' pour toute formule F.
Preuve : Par définition, si s'' existe, elle doit envoyer chaque variable A vers (As)s', c'est-à-dire vers s(A)s'. Donc s'' est unique. Maintenant, soit s'' la substitution que nous venons de définir, alors Fs'' égale (Fs)s' par une récurrence structurelle facile sur F. ¤

On écrit ce s'' ss', ou s'°s. Le théorème nous permet de définir :
Définition 5  La composition de substitutions est l'opération ° définie par F(s'°s) = (Fs)s' pour tout F. Nous écrivons aussi ss' au lieu de s'°s, de sorte que F(ss')=(Fs)s'.


La composition de substitutions n'est pas la composition de fonctions ! En effet, l'image de la variable A est s(A)s', pas s'(s(A)). En fait, ce dernier n'a aucun sens si s(A) n'est pas une variable.


Théorème 6  La composition de substitutions est associative, et admet la substitution vide comme élément neutre.
Preuve : Exercice. ¤



Next Contents