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. 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. Le terme de correction peut ici être pris dans son sens de qualité de ce qui est correct. 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é. 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. 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. 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.