Systeme formel

Système formel

Un système formel est un ensemble de formules, ou expressions formelles, que l’on peut interpréter comme des noms, des phrases, ou de toute autre façon. Ils sont des ensembles fondamentaux pour la logique et les mathématiques.

Exemples

• Les ensembles de nombres, entiers, rationnels, algébriques, peuvent être définis comme des systèmes formels, mais pas les ensembles qui contiennent tous les nombres transcendants, réels ou complexes.

• La nomenclature de la chimie organique est un système formel.

• Une théorie est un ensemble de phrases, ou de propositions, et est donc un système formel.

Problèmes généraux

Les théories générales des systèmes formels ont été conçues par des logiciens surtout pour étudier les théories. De ce point de vue on peut les considérer comme des métathéories générales, des théories de toutes les théories.

Les trois problèmes fondamentaux pour les théories des systèmes formels sont : - Comment définit-on des ensembles de formules ? - Comment interprète-t-on les formules qui parlent des formules et des ensembles de formules ? - Comment prouve-t-on des vérités à propos des ensembles de formules ?

Le point de vue formel introduit une limitation. On se soucie peu de la signification des mots ou des symboles. Les théories n’y sont pas considérées comme des fenêtres sur le monde réel. Elles sont opaques. Elles ne contiennent que des assemblages de mots et on se soucie d’abord de leurs formes, pas de leurs significations. D’où le nom de point de vue formaliste.

Les théories axiomatiques

Un système formel est souvent construit en se donnant un ensemble d'axiomes et en raisonnant à partir de ces axiomes à l'aide de la logique usuelle. Par exemple, la théorie axiomatique des ensembles est un système formel. Rappelons d'abord qu'un axiome est 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 ). Un théorème est une proposition déduite à partir des axiomes, en un nombre fini d’étapes, avec les règles de la logique. Si les règles de déduction sont valides, un théorème est vrai pourvu que les axiomes soient vrais.

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

Les systèmes formels de base sont des ensembles énumérables. Intuitivement, ce sont tous les ensembles pour lesquels on peut donner un procédé mécanique d’énumération de tous leurs éléments.

Une théorie axiomatique est toujours énumérable, pour les raisons suivantes.

• La liste, finie ou infinie, de ses axiomes, est toujours décidable, parce qu’on veut savoir précisément ce qui est et ce qui n’est pas un axiome.

• Les méthodes formelles imposent que les règles de déduction aient un caractère mécanique, qu’elles puissent être appliquées aveuglémént par une machine. L’ensemble des preuves formelles est donc toujours décidable. Si on présente une preuve formalisée à un ordinateur convenablement programmé, il répond si oui ou non la preuve est correcte, si oui ou non elle commence par des axiomes et respecte les règles de déduction.

La théorie, c’est-à-dire l’ensemble des théorèmes, ou formules prouvables à partir des axiomes, est énumérable, parce qu’on peut définir un ordre sur l’ensemble de toutes les listes finies de formules. Soit une formule F dont on veut savoir si elle est un théorème. L’ordinateur examine chaque liste finie de formules une par une et décide si oui ou non elle est une preuve formelle. Si oui, alors la dernière formule de la liste est un théorème. Si cette formule est F alors l’ordinateur s’arrête et répond que F est un théorème. Dans les autres cas, l’ordinateur examine la liste finie suivante.

Si F est vraiment un théorème, un ordinateur ainsi programmé trouvera toujours la réponse, parce qu’il examine toutes les preuves formelles possibles. Mais il mettra beaucoup de temps, beaucoup trop pour que cette méthode soit réellement efficace pour nous simples mortels.

Si F n’est pas un théorème, l’ordinateur ne s’arrête jamais, il examine sans arrêt de nouvelles listes, il trouve de nouvelles preuves, mais il ne trouvera jamais de preuve de F, puisque F n’est pas un théorème. Une théorie axiomatique est donc toujours énumérable mais il n’est pas sûr a priori qu’elle soit décidable.

Un « bon » système formel S doit être cohérent.

S est cohérent s'il ne permet pas de démontrer une contradiction (formellement : s'il n'existe pas de proposition A telle que S démontre A et non A)

S'il n'est pas cohérent et le principe du raisonnement par l'absurde est accepté parmi les règles de déduction logique alors toutes les formules sont prouvables. Un système qui prouve tout et son contraire ne prouve rien du tout.

Kurt Gödel a montré au début du siècle que tout système formel un tant soit peu complexe contenait des propositions vraies mais non démontrables (voir Théorème d'incomplétude de Gödel).

Voir également

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

Sources

• Raymond Smullyan, (en) Theory of formal systems

Ce document provient de « Syst%C3%A8me formel ».