Système formel
Source: Wikipédia sous licence CC-BY-SA 3.0.
La liste des auteurs de cet article est disponible ici.

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 (La chimie organique est une branche de la chimie concernant la description et l'étude d'une grande classe de molécules à base de carbone : les composés organiques.) est un 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...).
  • Une théorie (Le mot théorie vient du mot grec theorein, qui signifie « contempler, observer, examiner ». Dans le langage courant, une théorie est une idée ou une connaissance spéculative, souvent basée sur...) est un ensemble (En théorie des ensembles, un ensemble désigne intuitivement une collection d’objets (les éléments de l'ensemble), « une multitude qui peut être comprise comme...) 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 (Graphie) de vue (La vue est le sens qui permet d'observer et d'analyser l'environnement par la réception et l'interprétation des rayonnements lumineux.) 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 (Le mot monde peut désigner :) 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 (La logique (du grec logikê, dérivé de logos (λόγος), terme inventé par Xénocrate signifiant à la fois raison, langage, et raisonnement) est dans...) usuelle. Par exemple, la théorie axiomatique des ensembles (Il existe plusieurs versions formelles de la théorie des ensembles, mais quand on parle de « la » théorie axiomatique des ensembles, on désigne habituellement sous ce nom la théorie ZFC. Au XXIe...) est un système formel. Rappelons d'abord qu'un axiome (Un axiome (du grec ancien αξιωμα/axioma, « considéré comme digne, convenable, évident en soi ») désigne une vérité...) 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 (La géométrie euclidienne commence avec les Éléments d'Euclide, qui est à la fois une somme des connaissances géométriques de l'époque et une tentative de formalisation mathématique de ces...) ). Un théorème (Un théorème est une proposition qui peut être mathématiquement démontrée, c'est-à-dire une assertion qui peut être établie comme vraie au travers d'un raisonnement logique...) est une proposition déduite à partir des axiomes, en un nombre (La notion de nombre en linguistique est traitée à l’article « Nombre grammatical ».) 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 (L'Univers est l'ensemble de tout ce qui existe et les lois qui le régissent.) 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 (Dans le langage courant, la mécanique est le domaine des machines, moteurs, véhicules, organes (engrenages, poulies, courroies, vilebrequins, arbres...) 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 (En logique mathématique, le terme décidabilité recouvre deux concepts liés : la décidabilité logique et la décidabilité algorithmique.), 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 (Un ordinateur est une machine dotée d'une unité de traitement lui permettant d'exécuter des programmes enregistrés. C'est un ensemble de circuits...) 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 (Le temps est un concept développé par l'être humain pour appréhender le changement dans le monde.), 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 (Une contradiction existe lorsque deux affirmations, idées, ou actions s'excluent mutuellement.) (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 (Le tout compris comme ensemble de ce qui existe est souvent interprété comme le monde ou l'univers.) et son contraire ne prouve rien du tout.

Kurt Gödel a montré au début du siècle (Un siècle est maintenant une période de cent années. Le mot vient du latin saeculum, i, qui signifiait race, génération. Il a ensuite indiqué la durée d'une génération humaine...) 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 (On parle de complétude en mathématiques dans des sens très différents. On dit d'un objet mathématiques qu'il est complet pour exprimer que rien ne peut lui être ajouté, en un...) de Gödel).

Page générée en 0.165 seconde(s) - site hébergé chez Amen
Ce site fait l'objet d'une déclaration à la CNIL sous le numéro de dossier 1037632
Ce site est édité par Techno-Science.net - A propos - Informations légales
Partenaire: HD-Numérique