Une preuve formelle est une suite finie et ordonnée de formules bien formées dans un langage formel et un système de démonstration donnés, telle que chaque formule soit soit une prémisse, soit un axiome du système, soit obtenue à partir de formules antérieures par une règle d'inférence du système, et que la dernière formule soit la conclusion dérivée.

Principe

La dérivabilité dans un système formel fixé, selon ses axiomes et ses règles d'inférence, est le critère déterminant pour qu'un raisonnement soit une preuve formelle.

Démonstration

Scénario illustratif — Situation : Dans un langage propositionnel avec des axiomes A1 et A2 et Modus Ponens comme règle d'inférence, un démonstrateur énonce (1) A1, (2) A2, (3) A1 → B, (4) B (à partir de 1 et 3 par Modus Ponens). Reconnaissance : Chaque étape est soit un axiome soit suit la règle du système. Action : Le démonstrateur enregistre la séquence comme une dérivation. Conséquence : B est un théorème du système parce qu'il apparaît comme formule finale d'une dérivation finie valide.

Mauvaise application

Confondre un argument convaincant en langage naturel avec une preuve formelle sans fournir sa traduction dans le langage formel spécifié et la vérification que chaque étape respecte les règles d'inférence du système ; l'erreur est de confondre la force persuasive et la dérivabilité syntaxique.

Conséquence

Lorsqu'une assertion possède une preuve formelle dans un système sain, elle est dérivable syntaxiquement et ainsi justifiée au sein de ce système ; toutefois cette dérivabilité n'assure que ce que permettent les axiomes et règles choisis et dépend du langage et des axiomes retenus, non d'assertions empiriques externes.

Inversion

Si le système de preuve choisi est non sain par rapport à une sémantique visée, ou si l'interprétation des symboles diffère de l'interprétation formelle, alors une preuve formelle peut ne pas préserver la vérité sous cette interprétation externe ; inversement, certains faits sémantiques vrais peuvent ne pas admettre de preuve formelle dans un système incomplet.

Limite

Clairement inclus : une dérivation de type Hilbert ou déduction naturelle qui énumère chaque formule et justifie chaque étape par un axiome ou une règle. Cas limite : un schéma indiquant le motif d'inférence principal sans vérifier chaque application de règle. Clairement exclu : une explication informelle recourant à des métaphores ou à l'intuition sans règles syntaxiques explicites ni dérivation formule par formule.

Tension sémantique

Preuve formelle ↔ Explication mathématique informelle — la preuve formelle privilégie la vérifiabilité mécanique et la correction syntaxique, l'explication informelle privilégie l'intuition et la pédagogie ; leur traduction réciproque peut être complexe.

Synthèse

La preuve formelle transforme la validité argumentaire en une séquence vérifiable mécaniquement liée à un système choisi ; son sens dépend à la fois de l'adéquation de la formalisation et de la relation du système à la sémantique visée.