Preuve par l'absurde

Si $x > 0$, est ce que tu ne peux pas trouver un $\alpha$ tel que $0 < \alpha < x$ ?

@Dom: pour la quantification ça doit être ça: $\forall x, \left[\forall \alpha, 0<\alpha \rightarrow x<\alpha\right] \rightarrow x\leq 0$

Topoto: La relation est généralement fausse, sauf si tu considères que ta relation d'ordre est totale.

Je rappelle qu'on définie la relation d'ordre stricte $a<b$ comme un résumé de la formule $a\leq b\wedge \neg a=b$.
Dans le cadre d'une relation d'ordre totale tu as $(\neg a\leq b) \rightarrow b\leq a$.

Voici un résumé de démonstration par l'absurde de la formule dans le cadre de la relation d'ordre totale:

D'abord on suppose la formule qu'on voudrait fausse: $\neg \left( \forall x, \left[\forall \alpha, 0<\alpha \rightarrow x<\alpha\right] \rightarrow x\leq 0\right)$, on utilise la règle dérivée portant sur la négation de l'universalité pour montrer qu'elle implique: $\exists x \neg \left( \left[\forall \alpha, 0<\alpha \rightarrow x<\alpha\right] \rightarrow x\leq 0\right)$.
Là dessus sachant que si $A$ prouve $B$ alors $\exists x A$ prouve $\exists x B$ et que par ailleurs $\neg (A\rightarrow $ prouve $A\wedge \neg B$, on en déduit:
$\exists x \ \left( \neg x\leq 0 \wedge \left[\forall \alpha, 0<\alpha \rightarrow x<\alpha\right]\right)$

Là-dessus on explore les implications de cette dernière formule si on lui enlève le quantificateur existentiel $\exists x$:
-$\neg x\leq 0$ prouve par utilisation de la totalité de la relation d'ordre que $0\leq x$ et par utilisation de la réflexivité $x\neq 0$ et donc par conjonction des deux $0<x$.
- On utilise l'élimination de l'universalité (en remplaçant la variable liée $\alpha$ par le terme $x$) sur l'autre truc, ça donne: $0<x \rightarrow x< x$ (là, on commence à voir l'absurde venir).
- On utilise donc les deux dernière formules pour prouver $x<x$ cette formule implique notamment $x\neq x$.
On a une contradiction. La contradiction est une formule dans laquelle $x$ n'est pas libre, donc on l'a prouvée avec $\exists x \ \left( \neg x\leq 0 \wedge \left[\forall \alpha, 0<\alpha \rightarrow x<\alpha\right]\right)$ qui est donc fausse, or on avait déduit cette formule de la négation de celle qu'on cherche.