Démonstration par récurrence transfinie

ev : Lorsque $x=0$, $\forall y < x, P(y)$ est vraie (bah oui : trouve moi un $y<0$ et je te montrerai que $P(y)$ :-D ) donc si tu sais prouver $(\forall y < 0, P(y))\implies P(0)$, tu sais prouver $P(0)$, donc au fond tu as bien besoin de l'initialisation, tu peux juste la déguiser de cette manière.

pour Pierre, tu vas voir que c'est "la même chose" dite "langagièrement" différemment:

$$ \exists n: [P(n) \ et\ (\forall p<n: nonP(p))]$$

est la négation (logique classique) de :

$$ \forall n: [(\forall p<n: nonP(p))\to (nonP(n))]$$

et quand tu enlèves le "non" (P est quelconque), ça donne :

$$ \forall n: [(\forall p<n: P(p))\to P(n)]$$

@PC, je te traduis en français:

mon premier énoncé centré dit que $P$ a un plus petit élément
le deuxième qu'il n'en a pas
le troisième que nonP n'a pas de plus petit élément.

@PierreCap: On peut considérer en logique classique que $\forall x P(x)$ veut dire la même chose que $\neg (\exists x \neg P(x))$, que (si $E$ désigne un ensemble), $\forall x\in E, Q(x)$ abrège $\forall x \left(x \in E \Rightarrow Q(x)\right)$, et enfin que $A\Rightarrow B$ veut dire la même chose que $\neg (A \wedge \neg B )$.
Dans ce cas si $V$ est un ensemble et $F$ une propriété quelconque, l'énoncé
$$\left [\neg \exists y, y \in V \right ] \Rightarrow \left [ \forall x \in V, F(x)\right ]$$ devient une évidence grammaticale compte tenu de ce que (*) $\neg \neg C$ équivaut à $C$ pour tout énoncé $C$ puisque, une fois les abréviations dépliées et la règle (*) mise a contribution, on voit que cet énoncé dit la même chose que $$
\neg \left [\left ( \neg \exists y \left [ y \in V \right ] \right )\wedge \exists x \left ( x \in V \wedge \neg F(x) \right )\right ]
$$
En effet s'il n'y a aucun élément dans $V$, comment pourrait-il y avoir un élément dans $V$ qui de surcroît ne satisfait pas $F$?
Ensuite tu peux remplacer $V$ par $\emptyset$.

Bonjour PierreCap; j'ai rajouté une paire de crochet en plus. $\neg \exists y H$ est juste $\neg (\exists y H)$.

D'une manière générale:

1/ $[(\exists xR(x))\to P]$ veut dire la même chose que $[\forall x(R(x)\to P)]$ et ce dans TOUTES les logiques actuellement connues, y compris les plus faibles (bien plus faibles que l'intuitionniste). Tu peux même considérer que ce n'est pas une équivalence mais une égalité à ce point de rapprochement.

2/ En particulier, avec $P:=faux$, on note généralement $\perp$ pour dire "faux", et on abrège $A\to \perp$ par $(non(A))$, ça te donne:

$$[(\exists xR(x))\to \perp] \iff [\forall x(R(x)\to \perp)]$$

c'est à dire

$$[non(\exists x R(x))] \iff [\forall x(non(R(x)))]$$

que l'on devrait probablement plutôt écrire raisonnablement:

$$[non(\exists x R(x))] = [\forall x(non(R(x)))]$$

A cause de la présence très en amont de cette équivalence.

A mes précédents posts, je n'ai pas eu le temps d'écrire en entier l'axiome de récurrence qui t'intéressait, je me suis contenté d'insister (je varie en te le faisant avec le signe $\in$) sur le fait que pour tout $A$:

c'est la même chose de dire : $non(\exists x:[x\in A\ et\ (\forall y<x: y\notin A)])$

que de dire :$ [ \forall x:[ (\forall y<x: y\notin A) \to (x\notin A) ] $

en notant $\to$ pour l'implication.

Ceci afin de te signaler que c'est un grand mot que de dire que c'est un théorème que l'axiome de récurrence (ou la définition de bon ordre) entraine l'énoncé qui est à l'origine du présent fil. Certes, c'est bien un théorème, mais il est parfaitement évident, ce n'est qu'une réécriture de la définition quasiment telle quelle.

Dire "toute partie non vide a un plus petit élément" c'est dire (et pas seulement "équivalent par théorème à dire"):

$$ \forall A: [(\forall x:[ (\forall y<x: y\notin A) \to (x\notin A) ] )\to (A\ vide) ]$$

edit, j'avais écrit $ \forall A: [(\forall x:[ (\forall y<x: y\notin A) \to (x\notin A) ] ) ]$ qui non seulement est faux, mais même plus, ne veut pas dire grand chose.

J'ai fait des fautes de frappe sous la barre horizontale j'écris l'hypothèse mais pas la conclusion je corrigerai oublie ce psg pour l'instant.

Et oui x ne doit pas figurer pour ta Q1

Salut, j'ai lu la conversation en diagonale et comme je suis assez débutant et donc pas toujours à l'aise avec les "mélanges de grammaires" ou autre raccourcis, je tiens à apporter ces deux précisions à l'intention de PierreCap:

- Posée comme elle est, ta question laisse penser que tu n'as pas cerné la différence fondamentale entre la récurrence "simple" et la récurrence forte. La première n'est valide que dans le cas où chaque élément (sauf 0) a un prédécesseur, donc dans le cas où ton ensemble bien ordonné est isomorphe à $(\mathbb{N}, \leq )$ ou un de ses segments initiaux (lui-même ou un ensemble fini), tandis que la récurrence forte est valide pour tout ensemble bien ordonné (si tu es au-delà de $\mathbb{N}$ il y aura au moins un élément sans prédécesseur, le premier d'entre eux est le plus petit élément plus grand que tout les entiers naturels, il existe car l'ensemble est bien ordonné).

- Ici vous vous êtes surtout concentré sur le fait qu'en utilisant cette formule on peut se passer d'une formule d'initialisation, c'est exact, mais si on est pas habitué, il faut faire super attention à plusieurs raccourcis qui ont été utilisés ici, et dont les gens déjà très à l'aise avec la logique font abstraction (alors que ça peut méchamment bloquer les néophytes).

Tu as écris à peu près cela:

$\forall x\in E \left( \left[\forall y <x \rightarrow P(y) \right] \rightarrow P(x) \right) $

On notera d'une part que quand on écrit $y<x$ c'est que y appartient à E (sinon la relation d'ordre n'a pas été définie) et les trucs du genre $\forall x \in E(F(x))$ (où F est une formule) sont en fait un raccourci pour dire $\forall x (x\in E \rightarrow F(x))$ (et pour la petite histoire, quand tu écris $\exists x\in E (F(x))$ ça signifie $\exists x (x\in E \wedge F(x) )$ ).
Une formule "grammaticalement correcte" pour les règles de logique classique (dit aussi "calcul des séquents") ressemblerait plutôt à cela:

$ \forall x \left( x\in E \rightarrow \left[ \left(\forall y \left[y \in E \rightarrow \left(y<x \rightarrow P(y)\right) \right] \right) \rightarrow P(x) \right] \right)$

C'est à partir de cela que tu dois utiliser cette histoire d'hypothèse vide comme l'ont au début proposé ev et Champ-au-Lion, mais les premières fois, ce n'est pas évident et tu as donc tout intérêt à "transformer" cette formule de manière à avoir un machin qui te rendra plus évidente cette hypothèse vide, d'une part en mettant les implications sous formes disjonctives au niveau de $ y \in E \rightarrow \left(y<x \rightarrow P(y)\right) $ ( tu dois obtenir un truc dans ce goût-là: $\neg y\in E \lor \neg y<x \lor P(x) $, si je ne me trompe pas sur les conventions de priorités entre la négation et les opérateurs binaires ) et ensuite, comme ça a été proposé d'utiliser notamment ces histoires de négation et de quantificateur pour montrer que la formule est en fait équivalente à ce machin-là:

$\forall x\left( x\in E\rightarrow \left[ \left( \neg\exists y[y\in E \wedge y<x\wedge \neg P(y)]\right) \rightarrow P(x)\right]\right)$

Et là, ça pose moins de problème car la formule $\neg\exists y[y\in E \wedge y<x\wedge \neg P(y)]$ est évidemment vrai pour $x=0$.