Une technique de preuve qui établit une implication P ⇒ Q en prouvant sa contraposition ¬Q ⇒ ¬P à la place ; puisque l'implication est classiquement équivalente à sa contraposition, démontrer cette dernière suffit pour conclure la première.

Principe

Exploiter l'équivalence logique (classique) entre une implication et sa contraposition : prouver que ¬Q implique ¬P offre une voie alternative pour démontrer P implique Q, souvent en simplifiant l'argument.

Démonstration

Pour montrer : si n^2 est pair alors n est pair. Contraposition : si n est impair (c'est-à-dire ¬(n est pair)), alors n^2 est impair (¬(n^2 est pair)). Prouver la contraposition en écrivant n = 2k+1 et en développant n^2 donne l'implication initiale.

Mauvaise application

Tenter de justifier une implication dans des logiques où la contraposition n'est pas réciproquement dérivable (par ex. utiliser ¬Q ⇒ ¬P pour affirmer P ⇒ Q en logique intuitionniste sans justification supplémentaire), ou confondre contraposition et converse (Q ⇒ P).

Conséquence

Fournit une voie de preuve standard et souvent plus simple pour de nombreux théorèmes classiques ; peut transformer des preuves directes compliquées en preuves universelles plus simples et parfois donner des informations constructives sur les assertions niées.

Inversion

Une preuve directe de P ⇒ Q ou une preuve par contradiction (supposer P et ¬Q puis obtenir une contradiction) sont des stratégies alternatives ; la preuve par contraposition peut souvent se ramener à un bref argument par contradiction.

Limite

S'appuie sur le raisonnement propositionnel classique pour l'équivalence des formes ; bien que P ⇒ Q entraîne toujours ¬Q ⇒ ¬P en logique intuitionniste, obtenir P ⇒ Q à partir de ¬Q ⇒ ¬P nécessite en général des principes classiques (par ex. le tiers exclu). Elle présuppose aussi une négation classique et la bivalence pour les prédicats concernés.

Tension sémantique

On confond souvent contraposition et converse (Q ⇒ P). Il existe aussi une tension entre l'usage de la contraposition en contextes classiques et constructifs : équivalentes classiquement, elles ne le sont pas symétriquement constructivement.

Synthèse

La preuve par contraposition recompose une implication en une cible logiquement équivalente potentiellement plus simple à démontrer ; c'est une technique classique qui échange P ⇒ Q contre ¬Q ⇒ ¬P en gardant la précaution des conditions constructives et de la distinction avec la converse.