Accueil🇫🇷Chercher

Correction (logique)

En logique, la forme d'une argumentation déductive est correcte si et seulement si elle est valide et que toutes ses prémisses sont effectivement vraies[1].

En logique formelle, un système logique est correct si on peut lui associer une sémantique (on dit aussi un modèle) qui le justifie. La correction indique donc que les règles d’un tel système mettent en œuvre des raisonnements qui font du sens, puisqu'on peut les interpréter[2].

Étymologie

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].

Correction et cohérence

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.

Correction d'un argument ou d'une démonstration

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.
exemple d’argument correct :
  1. Tous les humains sont enclins à l’erreur.
  2. Nous sommes humains.

Donc nous sommes enclins à l’erreur.

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.


exemple d’argument à la correction incertaine :
  1. Tous les organismes avec des ailes peuvent voler.
  2. Les manchots ont des ailes.

Donc les manchots peuvent voler.

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.

Systèmes logiques

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. 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.

Correction (faible)

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é 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.

Correction forte

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.

Arithmétique de correction

Si une théorie T est une théorie dont les objets du discours peuvent être interprétés comme des nombres entiers, 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.

Relation avec la complétude

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.

Bibliographie

  • Hinman, P., Fundamentals of Mathematical Logic, A K Peters, (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).

Références

  1. (en) « Validity and Soundness », sur Internet Encyclopedia of Philosophy
    Traduction de « A deductive argument is sound if and only if it is both valid, and all of its premises are actually true. »
  2. Exemples d’usage du terme :
    • Bruno Marchal, CalculabilitĂ©, Physique et Cognition (lire en ligne), « ThĂ©ories et dĂ©monstrations »
    • Olivier Pirson, AbrĂ©gĂ© de Logiques Classiques (lire en ligne)
  3. Définition tirée du wiktionnaire
  4. Voir corrigo sur le Wiktionnaire.
  5. Exemple dans le mémoire Sémantiques formelles de Sandrine Blazy
  6. Exemple avec ce support de cours intitulé Preuve de correction.

Liens externes


Cet article est issu de wikipedia. Text licence: CC BY-SA 4.0, Des conditions supplémentaires peuvent s’appliquer aux fichiers multimédias.