LES SYSTEMES FORMELS

1 - Qu'est-ce qu'un système formel ?

Un système formel est un quadruplet S = ( A, γ, Ax, R) où :

1 - A est un ensemble fini de symboles, appelé alphabet,
2 - γ est un procédé de construction de mots,
3 – Ax est un ensemble fini ou dénombrable de mots particuliers appelés axiomes,
4 – R est un ensemble fini de règles de déduction de la forme :
{ w 1, ..., w k } → { m 1, ..., m n } où pour tout i, w i et m i sont des mots.

Remarques :

1- On dit indifféremment règle de déduction, ou de dérivation, ou d'inférence.

2- Il y a deux types de règles d'inférence : les règles de production, qui produisent de nouveaux mots à partir des

mots initiaux, et les règles de réécriture, qui fournissent une nouvelle forme pour le même mot.

2 - Trois exemples.

Le système (G.P.), encore appelé "axiomatique de Peano" :

- alphabet : { x, y, * }
- mots : S1 * S2 où S1 et S2 sont des suites quelconques de symboles x ou y
- un unique axiome : x * x
- une seule règle, qui est une règle de production :
w 1 * w 2 → y w1 * y w2 où w 1, w 2 sont des mots

Le système (D.H.) dû à Douglas Hoffstadter :

- alphabet : { M, I, U }
- mots : toute suite de lettres de l'alphabet
- axiome : M I
- règles de déduction :
1- w I → w I U où w est un mot (production)
2- Mw → M ww où w est un mot (production)
3- III → U (réécriture)
4- UU → (réécriture)

Le (p q -) système :
- alphabet : { p, q, - }
- mots : suites finies de symboles de l'alphabet
- axiomes : les mots x p - q x - où x est formé uniquement de -
- une seule règle de déduction (production) :
si x, y et z sont des mots formés uniquement de -,
du mot x p y q z on peut déduire le mot x p y - q z -

Juin 2006 - Mme Kempf LOGIQUE FORMELLE 4 / 60

3 - Théorèmes

Définition 1 :Dans un système formel, une preuve (ou démonstration) est une suite finie de mots w 1 w2.... w k
où chaque w i : soit est un axiome,
soit se déduit des w j , j < i par l'une des règles d'inférence.
L'entier k est appelé la longueur de la preuve.

Définition 2 : Un théorème est un mot t tel qu'il existe une démonstration w 1 w2....w k avec t = w k
On note alors | t .

Exemples :
Dans (GP), yyx * yyx est un théorème dont la démonstration est :
x * x, yx * yx, yyx * yyx

Dans (DH), MIIUIIU est un théorème, de preuve :

MI, MII (par R2), MIIU (par R1), MIIUIIU (par R2).

Dans le (p q -) système, - - - p - - q - - - - - est un théorème de preuve :

---p-q---- , ---p--q-----

Remarque : Un axiome est un théorème; sa démonstration est de longueur 1.

Nous avons donc : {axiomes} ⊂ {théorèmes} ⊂ {mots} ⊂ {chaînes de l'alphabet}

≠ ≠ ≠

4 - Décidabilité

Définition : On dira qu'un système formel est décidable lorsqu'il existe une procédure de décision unique qui permet
en un temps fini de décider si un mot quelconque du système est un théorème ou un non-théorème (mot dont on
peut prouver qu'il n'est pas un théorème)

Théorème
Procédure
Mot du de
S.F. décision Non théorème

Réponse
en temps

Un système formel qui n'est pas décidable peut être :

- semi-décidable : lorsqu'il existe une procédure qui, si une formule est démontrable, le dira en un temps fini,
mais qu'il n'existe pas de procédure capable de faire la même chose pour tous les non théorèmes.
- indécidable : dans les autres cas.

Juin 2006 - Mme Kempf LOGIQUE FORMELLE 5 / 60

5- Procédures de décision

Deux procédures de décision sont particulièrement simples :

1 - Si on peut construire l'ensemble de tous les théorèmes d'un système formel, les mots qui n'appartiennent pas à
cet ensemble sont des non-théorèmes et le système est décidable : pour tout mot, il suffit de vé rifier s'il appartient
ou non à l'ensemble des théorèmes.

Exemple 1 :
Tous les théorèmes de (GP) sont de la forme y ... y x * y ... y x
p fois p fois

Exemple 2 :
Une procédure dérivée : soit m un mot de longueur k d'un système formel S. Si on sait construire de manière
exhaustive tous les théorèmes de longueur inférieure ou égale à k, m est un théorème de S si et seulement
s'il est l'un d'entre eux. Sinon, il est un non-théorème; et le système est décidable.
C'est le cas du (p q -) système ; la procédure est dite "de bas en haut" (ou bottom - up):
Cherchons si - - p - - q - - - est un théorème. C'est un mot de longueur 9.
1. on prend l'axiome le plus simple, - p - q - -
On lui applique la règle d'inférence, on trouve - p - - q - - - qui est un mot de longueur 8.
On applique de nouveau la règle d'inférence, on trouve - p - - - q - - - - , mot de longueur >9.
2. on prend le 2ème plus simple axiome, - - p - q - - -
On lui applique la règle d'inférence, on trouve - - p - - q - - - - qui est un mot de longueur >9.
3. on prend le 3ème plus simple axiome, - - - p - q - - - - ; il est déjà de longueur >9.
Le mot - - p - - q - - - est donc un non-théorème.

Remarque : Tout système formel dont les règles allongent les mots est décidable.
La procédure de décision précédente le prouve.

2 - Procédure dite "de haut en bas" ou (top - down):

un mot étant donné, on regarde si c'est un axiome (donc un théorème); si non, on réduit sa longueur en utilisant une
règle d'inférence. On itère le procédé jusqu'à obtenir :
• soit un axiome : dans ce cas, le mot initial était un théorème
• soit un mot dont la longueur ne peut plus être réduite et qui n'est pas un axiome : le mot initial était un non -
théorème.

Quoique simples et fiables, ces procédures ne sont pas forcément rapides. Il se peut même qu'elles ne permettent
pas d'atteindre une réponse :

Exemple :
Le MU-Puzzle (Douglas Hofstadter)
En cherchant si le système (DH) est décidable, supposons que nous voulions tester si le mot MU es t un
théorème.
Comme deux des règles de (DH) raccourcissent les mots auxquels elles s'appliquent, on ne peut pas conclure
en appliquant la remarque précédente. Il reste la possibilité de construire l'arbre de dérivation du système, c'est-à-
dire de produire tous les théorèmes de (DH) en appliquant de toutes les manières possibles les règles
d'inférence à partir de l'axiome MI. Si l'on trouve MU, on dira alors qu'il est un théorème. Si on ne le trouve jamais,
ce ne sera pas un théorème.

Juin 2006 - Mme Kempf LOGIQUE FORMELLE 6 / 60

 Cette conclusion est insatisfaisante à deux titres : comment être sûr qu'on n'obtiendra jamais MU ? ne peut-on
pas toujours se dire qu'on l'obtiendra un peu plus tard? Et si MU n'est pas un théorème, ce n'est pas forcément un
non théorème. On ne peut donc pas conclure quant à la décidabilité de (DH) en l’état actuel de nos méthodes.

Deux notions peuvent conduire à des techniques plus efficaces, celles d'interprétation et de méta -raisonnement.

6 - Interprétation

Exemple :
Dans le (p q -) système, on peut observer qu'une chaîne de symboles est un théorème si et seulement si les 2
premiers groupes de - ont des cardinaux dont la somme est le nombre de - du 3ème groupe. On peut même faire
mieux qu'"observer" : on peut le démontrer par récurrence sur la longueur des théorèmes (exercice).
Ceci donne l'idée d'interpréter - - p - - - q - - - - - en : 2 plus 3 égale 5.
On remarquera qu'une interprétation est rarement unique : 2 égale 3 ôté de 5 est une autre idée.

Plus généralement :
Une interprétation d'un système formel S = ( A, γ, Ax, R) est le choix d'un univers U de domaine D (D est un
ensemble d'objets appartenant à U) et d'une application I : S → U
qui associe :
à chaque symbole de A un élément de D
au procédé de construction de mots γ un procédé de construction d'énoncés de U
à chaque axiome de Ax un énoncé vrai de U
à chaque règle d'inférence de R un mode de déduction dans U

Les théorèmes du système formel S deviennent des énoncés de U qu'on juge VRAIS ou FAUX dans l'interprétation
(ou privés de sens).

U
SF
x x

Procédé de Procédé de
Construction de construction
mots d'énoncés

axiome Enoncé vrai

Règle
Règle
d’inférence
d’inférence

théorèmes énoncés

Juin 2006 - Mme Kempf LOGIQUE FORMELLE 7 / 60

7 - Preuve et Vérité

Les concepts de Preuve et de Vérité appartiennent à des univers différents.

Les notions de vérité et de fausseté sont absentes des systèmes formels.

Dans un système formel, un mot peut être prouvé par une démons tration. C'est alors un théorème.

Lorsqu'on donne une interprétation du système formel, les mots deviennent des énoncés qui peuvent être vrais, ou
faux, ou privés de sens.

Quel lien y a-t-il entre preuve et vérité ?

Tout est possible !

Exemple 1 :
Dans le (p q -) système interprété dans l'ensemble des entiers positifs ou nuls où p représente + , q représente =
et où une suite de n – représente l'entier n, les axiomes deviennent effectivement des énoncés vrais, les règles
d'inférence se traduisent par des déductions correctes (par exemple : si 2 + 3 = 5 alors 2 + 4 = 6) et les
théorèmes sont exactement les énoncés vrais de la forme a + b = c.

Exemple 2 :
Dans (GP), nous avons vu que les théorèmes sont: | y ... y x * y ... y x
p fois p fois
On introduit ce qu'on appelle une métanotation | ypx * ypx (c'est-à-dire une notation issue d'un autre contexte
que celui du système formel dans lequel on travaille).
w1 * w 2 est donc un théorème SSI w 1 s'écrit ypx et w 2 aussi
Sinon, w 1 * w 2 est un non-théorème.

• Première interprétation de (GP) :

Domaine: N , x:0, *:= , y : successeur de .
L'axiome est 0 = 0 (vrai!)
Les théorèmes sont p = p pour tout p ∈ N (énoncés vrais).
De plus, les énoncés faux sont exactement les interprétations des non-théorèmes.

bonne interprétation, correspondance parfaite entre:

théorèmes et énoncés vrais
non-théorèmes et énoncés faux

• Deuxième interprétation de (GP)

Domaine : Langue française , x : "Socrate est mortel", * : identité de deux phrases , y : négation
L'axiome s'interprète comme un énoncé vrai, les théorèmes aussi.
Mais le non-théorème y y x * x s'interprète en un énoncé vrai.

La classe des non-théorèmes qui deviennent des énoncés vrais est non vide;
cependant, tout énoncé vrai est l'interprétation d'un théorème (mais aussi, en plus, de non théorèmes).

Juin 2006 - Mme Kempf LOGIQUE FORMELLE 8 / 60

 Exemple 3 :
"Pour tout entier n supérieur à 2, l'équation en nombres entiers xn + yn = zn n'a pas de solution"
( Fermat )
Ce résultat est :
• VRAI avec l'interprétation commune des symboles arithmétiques.
• INDEMONTRABLE dans l'axiomatisation de l'arithmétique ; mais ce n'est pas non plus un non théorème.

L'axiomatique de l'arithmétique est donc au mieux semi-décidable (puisqu'il existe des phrases
indémontrables)
et il existe des énoncés vrais qui ne sont pas issus de théorèmes. Cela ne rend pas pour autant
l'axiomatique sans intérêt ; cet intérêt a simplement ses limites.

Quelques définitions:

On appelle tautologie tout mot d'un sys tème formel qui se traduit par un énoncé vrai dans toutes les interprétations du
système formel.
Un système formel dans lequel tout théorème est une tautologie est dit correct.
Un système formel dans lequel toute tautologie est un théorème est dit complet.
Un système est dit consistant lorsqu'il existe une interprétation transformant tout théorème en énoncé vrai. Cette
interprétation est appelée modèle.

Remarque : un système correct est consistant.

8 – Méta-raisonnement

Jusqu'ici, pour voir si un mot du système formel S est un théorème ou non, on a cherché une démonstration dans S
ou une procédure que l'on déroule à l'intérieur du système S afin de conclure. On raisonne dans le système formel.
Effectuer un méta-raisonnement, c'est raisonner sur le sys tème formel afin d'en trouver les propriétés ou de gagner
en efficacité pour les démonstrations.

Exercice :
Le MU-Puzzle.
Nous avons vu que la construction de l'arbre de dérivation pouvait conduire à une recherche sans fin de la
réponse.
Quel méta-raisonnement envisager pour trouver la réponse avec certitude ?

Le préfixe "méta" (du grec µετα : au-dessus de)

• on a déjà introduit les méta -notations.
• on dit parfois que l'on travaille à un méta-niveau pour dire "à un niveau d'abstraction supérieur"; on aura des
exemples de cela dans la suite.
• il arrive que l'on définisse une méta -théorie, c'est-à-dire une théorie qui englobe la théorie actuelle et permette
d'élargir le champ des raisonnements.

Juin 2006 - Mme Kempf LOGIQUE FORMELLE 9 / 60

 • on parle enfin de méta -raisonnement lorsque l'on choisit de raisonner sur un système formel (et non dedans),
par exemple pour aboutir (plus rapidement) à une preuve, pour démontrer qu'un mot n'est pas démontrable, pour
étudier le système formel et établir certaines de ses propriétés.

Juin 2006 - Mme Kempf LOGIQUE FORMELLE 10 / 60