Système formel

Un système formel est une modélisation mathématique d'un langage en général spécialisé qui en représente les éléments, termes, formules, dérivations, ..., par des objets finis (entiers, suites, arbres ou graphes finis...). Le propre d'un système formel est que l'on peut vérifier algorithmiquement la correction (au sens grammatical) de ses éléments, c'est-à-dire que ceux-ci forment un ensemble récursif.

Les systèmes formels s'opposent aux langues naturelles pour lesquels les algorithmes de traitement sont extrêmement complexes et surtout doivent évoluer dans le temps pour s'adapter aux transformations du langage.

Les systèmes formels sont apparus en logique mathématique afin de représenter mathématiquement le langage et le raisonnement mathématique, mais peuvent se trouver également dans d'autres contextes : informatique, chimie...

Exemples

• Le calcul des prédicats, système logique modélisant le langage mathématique.

• Le lambda-calcul, langage de programmation théorique utilisé pour étudier les liens entre logique et informatique ; plus généralement tout langage de programmation est par définition un système formel.

• La nomenclature des molécules organiques est un système formel.

Systèmes formels en logique

Les systèmes formels ont été conçus par les logiciens afin de poser et étudier mathématiquement certains problèmes liés au langage mathématique. De ce point de vue on peut les considérer comme des métathéories générales, des théories sur les théories (mathématiques).

Les systèmes logiques visant à modéliser le langage mathématique résolvent trois problèmes :

• Comment formalise-t-on les énoncés mathématiques (théorèmes, lemmes, définitions, etc.), c'est-à-dire comment définit-on la notion de formule ?

• Réciproquement, comment interprète-t-on les objets formels que sont les formules de façon à les voir comme des énoncés mathématiques signifiants ?

• Comment prouve-t-on des formules, c'est-à-dire comment formalise-t-on les règles du raisonnement mathématique ?

Les systèmes formels ont permis l'émergence d'une épistémologie des mathématiques appelée point de vue formaliste au terme de laquelle les mathématiques apparaissent comme un jeu de manipulation de symboles suivant des règles rigoureuses mais a priori dépourvues de sens ; le sens des formules est reconstruit a posteriori par les interactions qu'elles entretiennent les unes avec les autres au travers des règles de raisonnement.

Les théories axiomatiques

Une théorie axiomatique est un système logique qui représente une théorie mathématique, c'est-à-dire un ensemble de résultats se rapportant tous à un même type d'objet. Une théorie axiomatique est fondée sur un ensemble d'axiomes qui sont des formules définissant les objets et relations de base de la théorie ; à partir de ces axiomes et en utilisant les règles de raisonnement on dérive les théorèmes de la théorie. Par exemple, la théorie des ensembles est un système formel dont les axiomes définissent la notion d'ensemble. Un axiome est donc une proposition non démontrée qui sert de point de départ à un raisonnement : par exemple « par deux points il passe une et une seule droite » est un axiome de la géométrie euclidienne.

La vérité des axiomes ou des formules est définie relativement à un modèle, un univers possible, dans lequel les formules sont interprétées.

L’énumérabilité des théories axiomatiques

Comme on a dit plus haut, les systèmes formels sont des ensembles récursifs, c'est-à-dire que l'on peut vérifier algorithmiquement si un élément (formule, terme, déduction) appartient au système. Une théorie axiomatique, vue comme l'ensemble de ses axiomes, n'échappe pas à cette règle, c'est-à-dire que la question de savoir si un axiome appartient ou pas à la théorie est décidable.

Si par contre on pense, comme c'est l'usage, une théorie axiomatique comme l'ensemble des conséquences de ses axiomes, c'est-à-dire l'ensemble de ses théorèmes, alors celui-ci n'est, sauf rares exceptions, pas récursif, mais seulement récursivement énumérable : on peut écrire un programme qui va énumérer toutes les conséquences des axiomes en appliquant mécaniquement et de toutes les façons possibles les règles logiques. Par contre il n'existe pas de programme qui étant donnée une formule F saura répondre si celle-ci est un théorème de la théorie ; ou plus exactement on ne peut faire mieux que d'énumérer tous les théorèmes de la théorie au moyen du programme précédent : si F est un théorème, alors elle apparaitra dans l'énumération au bout d'un temps fini, mais si elle n'est pas conséquence des axiomes, le programme ne termine jamais.

Cohérence

Une théorie axiomatique est cohérente si il existe des formules qui ne sont pas conséquence de ses axiomes. Par exemple l'arithmétique de Peano est cohérente car elle ne démontre pas la formule « 0 = 1 ». On peut équivalemment définir la cohérence comme le fait de ne pas démontrer de contradiction.

Kurt Gödel a montré que toute théorie axiomatique suffisamment puissante pour représenter l'arithmétique ne pouvait démontrer sa propre cohérence de manière formelle (voir Théorème d'incomplétude de Gödel).

Systèmes formels en informatique

Comme on a dit plus haut, les langages de programmation sont des systèmes formels : comme les système logiques servent à formaliser le langage mathématique (théorème, démonstrations), les langages de programmation formalisent les algorithmes. Les langages de programmation sont formés d'au moins deux constituants :

• les programmes qui sont représentés par des fichiers informatiques, c'est-à-dire des suites finies de nombres ; pour l'affichage les nombres sont en général interprétés comme des codes de caractères de façon à présenter le programme comme un texte. Mais ça n'est pas toujours le cas : un programme en langage machine est une suite de codes d'instructions du processeur. Bien entendu toute suite de nombres n'est pas un programme correct ; par contre on peut tester algorithmiquement si un fichier contient un programme qui satisfait les contraintes syntaxiques du langage dans lequel il est écrit.
• une sémantique opérationnelle qui détermine la façon dont un programme doit s'exécuter, c'est-à-dire la façon dont l'ordinateur doit interpréter le programme comme une séquence d'instructions. La sémantique opérationnelle d'un langage est en général réalisée par un programme (qui parfois est même écrit dans le même langage !), sauf dans le cas du langage machine où la sémantique opérationnelle est réalisée par le processeur lui-même.

Auxquels on ajoute parfois un troisième constituant :

• une sémantique dénotationnelle qui détermine abstraitement le comportement du programme, typiquement en l'interprétant comme une fonction : par exemple un programme de tri sera interprété par une fonction sur les listes d'entiers et à valeurs dans les listes d'entiers.

En dehors des langages de programmation, l'informatique définit plusieurs autres types de systèmes formels : les langages de spécification qui servent à définir le comportement désiré d'un programme de façon à pouvoir ensuite tester, vérifier ou démontrer qu'une implantation donnée satisfait la spécification ; les protocoles de communication qui définissent rigoureusement les échanges d'informations entre ordinateurs (ou téléphones mobiles) sur un réseau, ...

Voir également

• la définition de Smullyan des ensembles énumérables

Sources

• Raymond Smullyan, (en) Theory of formal systems