Une méthode de démonstration qui établit la vérité d'une proposition P en supposant sa négation ¬P et en dérivant une contradiction ; à partir de cette contradiction on conclut que P doit être vraie (appelée reductio ad absurdum ou preuve par contradiction en logique classique).

Principe

Si supposer ¬P conjointement aux prémisses acceptées conduit à une contradiction explicite, alors P s'ensuit ; symboliquement, (prémisses ∪ {¬P}) ⊢ ⊥ implique prémisses ⊢ P, dans le raisonnement classique.

Démonstration

Pour montrer que √2 est irrationnel, on suppose le contraire que √2 = p/q sous forme irréductible et l'on déduit une contradiction arithmétique concernant la parité, concluant ainsi à l'irrationalité de √2 par preuve indirecte.

Mauvaise application

Employer la preuve indirecte dans des systèmes qui rejettent le principe du tiers exclu (par exemple des cadres constructivistes ou intuitionnistes) pour affirmer l'existence sans fournir de témoin ; ou confondre une inconsistance dérivée avec un simple événement improbable.

Conséquence

Permet de nombreuses démonstrations valides en logique classique lorsque la construction directe est difficile ou inconnue ; donne souvent des résultats décisifs mais peut être non constructif quant aux témoins ou algorithmes.

Inversion

L'inverse est la stratégie de preuve directe : déduire de façon constructive P à partir des prémisses sans passer par l'hypothèse ¬P et la contradiction.

Limite

Entièrement valide en logique classique ; restreint ou interprété différemment en logique constructive, intuitionniste ou minimale où ¬¬P ⇒ P n'est pas généralement admis et où les affirmations d'existence exigent des témoins.

Tension sémantique

Il existe une tension entre la reductio et les preuves constructives : la reductio admet des conclusions non constructives via la contradiction, tandis que le constructivisme exige des constructions explicites, rendant le même résultat acceptable dans un cadre et pas dans l'autre.

Synthèse

Principe De Preuve Indirecte : méthode classique qui prouve des propositions en montrant que leurs négations conduisent à une contradiction, puissante pour des conclusions non constructives mais dépendante de l'acceptation des schémas d'inférence classiques.