formalisation

Sur une feuille, la phrase « le carré d'un entier pair est pair » paraît claire. Un contrôle automatique ne peut pourtant pas deviner ce que signifient « entier », « pair » ou « carré », ni quelles transformations sont permises. Il faut choisir des symboles, définir chaque terme et écrire les règles utilisables.

Cette mise au net est une formalisation. Elle transforme un raisonnement exprimé en langue courante en une suite d'énoncés dont la forme est contrôlable. On peut alors distinguer les symboles que l'on manipule de leur interprétation mathématique.

La formalisation est le passage d'un raisonnement, d'une théorie ou d'une relation à un langage formel explicitement défini. Ce langage précise les symboles admis et les règles qui permettent de former des expressions : c'est sa syntaxe. Il fixe aussi la manière dont ces expressions reçoivent une interprétation dans un modèle : c'est sa sémantique. Un symbole n'est donc univoque qu'à l'intérieur du langage et de l'interprétation annoncés.

Formaliser une théorie demande d'énoncer ses axiomes, c'est-à-dire ses points de départ, puis ses règles d'inférence. Une règle d'inférence indique quelles conclusions sont autorisées à partir de quelles prémisses. Une démonstration formelle devient alors une suite finie d'expressions bien formées : chaque ligne est un axiome, une hypothèse admise ou le résultat d'une règle appliquée à des lignes antérieures. Cette structure rend la vérification mécanique possible.

La syntaxe et la sémantique jouent des rôles distincts. La première demande si une expression est correctement construite et si une déduction respecte les règles. La seconde demande ce que l'expression signifie dans un modèle donné et si elle y est vraie. Une même idée peut recevoir plusieurs formalisations selon le langage, les axiomes et le niveau de détail choisis ; la rigueur vient de l'explicitation de ces choix, non d'une notation unique.

On formalise l'énoncé « le carré d'un entier pair est pair ».
Données : la variable n désigne un entier ; dire qu'un entier est pair signifie qu'il existe un entier k dont il est le double ; les règles usuelles de l'égalité et du calcul sur les entiers sont admises.

La lettre k désigne l'entier qui atteste que n est pair. La lettre q désigne celui qui attestera que son carré est pair. L'énoncé visé s'écrit alors :

1. Supposer qu'il existe un entier k tel que $n=2kn=2k$.
2. Élever cette égalité au carré.
3. Réécrire le résultat sous la forme du double d'un entier : $n^2=(2k{)}^2=4k^2=2(2k^2)n^2=(2k)^2=4k^2=2(2k^2)$.
4. Poser l'entier q égal à $2k^{2}2k^2$, puis conclure que le carré de n est pair.

Le contrôle consiste à reprendre chaque ligne : elle doit provenir d'une donnée, d'une définition ou d'une règle annoncée. La chaîne illustrée rend cette dépendance visible. Avec n égal à 6, on peut aussi vérifier l'interprétation : k vaut 3, le carré de n vaut 36 et q vaut 18.

Pour relire une démonstration, la formalisation oblige à identifier les prémisses et la règle qui justifie chaque conclusion. Si une preuve ordinaire suffit à des lecteurs humains, elle reste plus souple ; si une vérification automatique est recherchée, chaque étape doit être encodée dans le système retenu.

Pour comparer des raisonnements, le langage formel révèle leur structure commune. On peut alors repérer qu'une conclusion ne suit pas des prémisses, indépendamment du sujet évoqué par les phrases. Une argumentation en langue courante reste préférable lorsque ses implicites sont partagés et qu'une traduction complète n'apporte aucun contrôle utile.

En informatique théorique et dans les assistants de preuve, les expressions et les règles sont données sous une forme manipulable par une machine. Le logiciel contrôle la conformité de la déduction ; le choix des axiomes, des définitions et de l'interprétation demeure une responsabilité mathématique.

Formalisation et simple notation symbolique. Remplacer « est pair » par un symbole ne suffit pas. Il y a formalisation lorsque la formation des expressions, le sens des symboles et les règles de déduction sont explicités. Écrire seulement « n pair » sous une forme abrégée reste une notation.

Formalisation et modélisation. Une modélisation choisit des objets mathématiques pour représenter une situation. Une formalisation fixe un langage et des règles pour exprimer et déduire rigoureusement. Décrire une population par une suite numérique construit un modèle ; encoder ses énoncés et ses déductions dans un système formel accomplit un autre travail.

Formalisation et démonstration. La formalisation prépare le cadre dans lequel une preuve peut être écrite et contrôlée ; elle ne prouve pas à elle seule chaque énoncé formulable. Dans l'exemple, définir la parité formalise le vocabulaire, tandis que déduire la parité du carré constitue la démonstration.

La vérification reste relative au système. Une machine peut confirmer qu'une ligne suit les règles encodées sans décider que les axiomes décrivent correctement l'objet étudié. Il faut contrôler séparément les choix de départ et l'interprétation.

Une expression bien formée n'est pas forcément vraie. Le respect de la syntaxe garantit seulement que l'expression appartient au langage. Sa vérité se juge dans un modèle, et elle peut varier d'un modèle à l'autre. Il faut donc annoncer le cadre sémantique avant de conclure.

Les conventions ne sont pas universelles. Une même lettre ou un même signe peut recevoir des significations différentes dans deux langages. Le symptôme est une preuve dont une étape change de sens au cours de la lecture. Un lexique stable et des règles explicites lèvent cette ambiguïté.

Un détail omis peut bloquer le contrôle mécanique. Dans une preuve ordinaire, une transformation algébrique peut être laissée implicite. Dans un système qui ne possède pas la règle correspondante, le vérificateur ne peut pas la franchir. Il faut alors décomposer l'étape ou ajouter un résultat déjà démontré.

Axiome. Cette notion précise le statut des énoncés pris comme points de départ dans une théorie formalisée.

Déduction naturelle. Ce formalisme organise les règles d'inférence pour construire des démonstrations ligne après ligne.