Système formel
Un système formel est une modélisation mathématique d'un langage en général spécialisé. Les éléments linguistiques, mots, phrases, discours, etc., sont représentés par des objets finis (entiers, suites, arbres ou graphes finis…). Le propre d'un système formel est que la correction au sens grammatical de ses éléments est vérifiable algorithmiquement, 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
[modifier | modifier le code]- 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 théorie des ensembles, système formel dont les axiomes définissent la notion d'ensemble.
- La nomenclature des molécules organiques est un système formel.
Systèmes formels en logique
[modifier | modifier le code]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.
Théories axiomatiques
[modifier | modifier le code]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
[modifier | modifier le code]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é 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
[modifier | modifier le code]Une théorie axiomatique est cohérente s'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
[modifier | modifier le code]Comme on a dit plus haut, les langages de programmation sont des systèmes formels : comme les systèmes 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 au moyen d'une analyse syntaxique 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 !) appelé compilateur ou interpréteur selon son mode de fonctionnement ; dans le cas du langage machine 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, ...
Systèmes formels en physique
[modifier | modifier le code]Le sixième problème de Hilbert posé en 1900 par le mathématicien allemand David Hilbert vise à axiomatiser la physique.
Dans une conférence donnée le à Zurich, David Hilbert énonce que les axiomes de toute théorie physique doivent respecter les critères d’indépendance et de non-contradiction de l'ensemble (de même qu’en mathématiques), à ceci s’ajoute pour le second point l’obligation de ne pas contredire ceux d’un autre domaine scientifique.
Voir aussi
[modifier | modifier le code]Bibliographie
[modifier | modifier le code]- Raymond Smullyan, (en) Theory of formal systems, 1961/1968.
- David Hilbert, « Axiomatisches Denken », Mathematische Annalen 78, pages 405-415, 1917, https://eudml.org/doc/158776. Traduction: « Pensée axiomatique », L’Enseignement Mathématique 20, pages 122-136, 1918, https://www.e-periodica.ch/digbib/view?pid=ens-001:1918:20::322.
