Correction (logique)

Le terme de correction peut ici être pris dans son sens de qualité de ce qui est correct^[3]. Correct venant de correctus participe passé de corrigo, (redresser, corriger) ; racine elle-même issue regō (diriger, guider, commander), et du préfixe augmentatif cor-, qui intensifie le sens du mot préfixé^[4].

On retrouve la même étymologie pour le terme allemand correspondant Korrektheit, où le suffixe heit sert à former des substantifs féminins à partir d’adjectifs, et indiquant la qualité décrite par ceux-ci.

Cependant, le terme de correction est parfois confondu avec la cohérence ou la validité, notamment dans des écrits qui les présentent comme la traduction du terme anglais soundness^[5]. Celui-ci dérive du germanique sund, qu’on retrouve dans l’allemand Gesund (sain), et Gesundheit, (santé). En anglais, le suffixe -ness joue le même rôle que heit en allemand, il est apposé à un adjectif pour former un nom indiquant une qualité, un état en relation avec l’adjectif. En ce sens il faudrait, suivant cette étymologie, traduire soundness par la santé d’un système formel.

En tout état de cause, le terme français idoine pour désigner cette notion est bien correction, comme l'atteste son proche homologue allemand, ou le terme preuve de correction largement employé dans le domaine informatique^[6].

La correction se distingue de la cohérence, qui est la propriété d'un système exempt de contradiction. Prenons l’exemple d’une logique dans laquelle on peut écrire les formules de l’arithmétique usuelle. Si la cohérence d’un système montre qu’on ne peut pas, dans ce système logique, montrer à la fois les formules ( x = 1 ) et ¬ ( x = 1 ) , soit dit en français une inconnue est à la fois égale au nombre 1, et en même temps qu'il est faux que cette inconnue est égale au nombre 1, la validité d'un système logique montre qu’on ne peut pas y démontrer des absurdités mathématiques comme (1 = 2) (le nombre un est égal au nombre deux).

La cohérence est une propriété syntaxique, elle ne nécessite pas de donner un sens aux formules, mais montre qu’on ne peut démontrer quelque chose et son contraire dans ce système. En revanche, souvent pour montrer la cohérence d'un système logique on exhibe un modèle. La validité repose sur le sens qu'on donne aux formules. Dans l'exemple de l'arithmétique le sens que l'on donne aux formules est le sens usuel.

En logique un argument ou une démonstration est correct si et seulement si :

1. il n'utilise que des inférences reconnues comme valides ;
2. toutes ses prémisses sont acceptées comme vraies.

Dans la mesure on l’on accepte de considérer vraies ses prémisses, cet argument sera considéré comme logiquement correct. En l’occurrence les prémisses relèvent d’expériences sensibles expérimentables par tout un chacun.

Dans un sens tout à fait général, bien que valide car basé sur un syllogisme, cet argument n’est pas correct. En effet, il existe par exemple des oiseaux inaptes au vol, comme le Manchot empereur, la première prémisse est donc fausse et le raisonnement incorrect. Il s’agit ici d’un problème au croisement de la définition, de la théorie des catégories et de la théorie du cygne noir : un individu qui n’aura connu que des organismes ailés capables de voler pourrait assimiler ces deux catégories comme interdépendantes et reléguer au rang de chimère un organisme ailé incapable de voler, par exemple en s’appuyant sur le principe du rasoir d'Ockham.

La correction fait partie des propriétés fondamentales de la logique mathématique. Un système formel conserve un statut incertain tant que sa correction n'a pas été démontrée. Ainsi le calcul des prédicats ou la logique intuitionniste ont été démontrés corrects.

Elle fournit l’attrait initial de la recherche d’un système logique possédant la propriété de correction.^{[réf. souhaitée]} En combinaison avec une autre propriété que peut avoir une logique, la complétude, qui assure que toute formule logique valide (vraie) est démontrable dans le système logique, elle implique que toutes et seulement toutes les formules valides sont démontrables dans ce système. Un système seulement complet pourrait être incohérent, c’est-à-dire permettre de démontrer toutes les formules valides mais aussi des formules invalides. De même un système seulement correct pourrait être incomplet, toutes les formules démontrables seraient valides, mais toutes les formules valides ne seraient pas forcément démontrables dans ce système.

L’établissement de la correction d'un système nécessite une preuve de correction. La plupart des preuves de correction sont triviales. Par exemple, dans un système axiomatique, prouver la correction revient à vérifier la validité des axiomes et que les règles d’inférence préservent la validité. La plupart des systèmes axiomatiques se limitent à la règle du modus ponens, avec parfois la substitution, il suffit donc de vérifier la validité des axiomes et une seule règle d’inférence.

Les propriétés de correction existent en deux variétés : correction faible et correction forte. La première est une version restreinte de la seconde.

La correction dite faible d’un système déductif (en) est la propriété qui garantit que toute phrase qui est prouvable dans ce système déductif est également vraie sur toutes les interprétations ou tous les modèles de la théorie sémantique pour le langage sur lequel est basée cette théorie.

Symboliquement, pour un système déductif S, un langage L accompagné de sa théorie sémantique, et une phrase P de L, on dit que « si S prouve P alors L modélise P » et on le note « si ⊢_S P, alors ⊨_L P ». Autrement dit, un système est correct si chacun de ses théorèmes, c'est-à-dire toute formule prouvable depuis l’ensemble vide, est valide dans chaque structure du langage.

La correction forte d’un système déductif S est la propriété qui assure que :

• étant donné un langage L sur lequel le système déductif est basé ;
• étant donné un ensemble de phrases du langage, ensemble usuellement noté à l’aide de la lettre grecque gamma : Γ ;
• toute phrase P du langage est une conséquence logique de l’ensemble Γ, au sens où tout modèle qui admettra chacun des membres de Γ comme vrai, admettra également P comme vraie.

On dit que « si gamma permet de prouver P avec S, alors gamma permet également de modéliser P avec L ». On note cela « Si Γ ⊢_S P, alors Γ ⊨_L P », ce qui de gauche à droite pourrait également se lire « si gamma prouve, par S, que P, alors gamma modélise, par L, que P ».

On remarquera qu’en affectant l’ensemble vide à Γ, de ces assertions de correction forte nous obtenons les assertions de correction faible.

Si une théorie T est une théorie dont les objets du discours peuvent être interprétés comme des nombres entiers^[pas clair], on dit que T est arithmétiquement correcte si tous les théorèmes de T sont effectivement vrais au regard des entiers des mathématiques standards^[pas clair].

La réciproque de la propriété de correction est la propriété de complétude sémantique. Un système déductif avec une théorie sémantique est fortement complet si toute phrase P qui est une conséquence sémantique (en) d’un ensemble de phrases Γ, peut être dérivée dans ce système déductif depuis cet ensemble. On note cela « si Γ ⊨P, alors Γ ⊢ P ».

La complétude de la logique du premier ordre a été pour la première fois établie explicitement dans le théorème de complétude de Gödel, bien que les principaux résultats étaient déjà contenus dans des travaux antérieurs de Skolem.

De façon informelle, un théorème de correction pour un système déductif exprime que toutes les phrases prouvables sont vraies. La complétude énonce que toutes les phrases vraies sont prouvables.

Le premier théorème d'incomplétude de Gödel montre que pour tout langage suffisant à l’expression d’une certaine portion de l’arithmétique, il ne peut exister de système déductif qui soit complet vis-à-vis de l’interprétation voulue du symbolisme de ce langage.

Ainsi, tous les systèmes déductifs corrects ne sont pas complets en ce sens de la complétude, pour lequel la classe des modèles (à un isomorphisme près) est restreinte à celle voulue. La preuve de correction originale s’applique à tous les modèles classiques, et non pas aux sous-classes propres spéciales de ceux voulus.

• Hinman, P., Fundamentals of Mathematical Logic, A K Peters, 2005 (ISBN 1-56881-262-0).
• Irving Copi. Symbolic Logic, 5th Ed, Macmillian Publishing Co., 1979.
• Boolos, Burgess, Jeffrey. Computability and Logic, 4th Ed, Cambridge, 2002.
• Paul Tomassi, Logic, (ISBN 0-415-16695-0) (hbk).

• (en) Cet article est partiellement ou en totalité issu de l’article de Wikipédia en anglais intitulé « Soundness » (voir la liste des auteurs).

• Validity and Soundness sur Internet Encyclopedia of Philosophy

•   Portail de la logique
•   Portail de la philosophie
•   Portail des mathématiques
•   Portail de la philosophie analytique