Blog personnel d'Arthur Milchior

Soit E un ensemble fini. Soit P une propriété que je veux prouver. Soit Q(S) une propriété que je veux prouver où S est un sous-ensemble de E. Je suis capable de prouver:

• Q(ensemble vide)
• Pour tout ensemble S dans E tel que Q(S), alors:
  • Soit il existe un surensemble S' stricte de S dans E tel que Q(S')
  • soit P

On peut donc montrer P par induction sur un entier i en disant que soit il existe un ensemble Ei de cardinal au moins i tel que Q(E), soit P est vrai. Ce que je trouve perturbant car, d'une part, P ne dépend pas de i, et d'autre part, il existe un entier i (le cardinal de E) tel que je sais que qu'il n'existe pas d'ensemble Ei.

Pour dire ça autrement, j'ai deux propriétés presque indépendantes, tel que je fais une induction sur l'une, que je sais être fausse au bout d'un moment, pour prouver un truc qui ne dépend pas de l'induction.

Mon autre résultat est probablement moins bizarre, à part que je ne l'avais jamais vu en vrai, jamais vu utiliser ailleurs que dans des preuves coq, preuves qui nécessitent de s'intéresser à la base, aux axiomes.

Je veux créer un grand entier. J'ai deux algorithmes A(E) et B(x), où E est un ensemble fini d'entiers et x un truc. L'algorithme A génère un ensemble un élément n(E), et B(n(E)) génère un entier n'appartenant pas à E. Ensuite, je fais A(E U {x}), et je recommence. Il me reste alors qu'à appliquer alternativement A et B jusqu'à obtenir un élément assez grand.

Bon, dis comme ça, c'est clair que je pourrais dire que AoB(E) génère simplement un entier n'appartenant pas à E. Mais intuitivement, c'est vraiment deux algorithme très différents, qui n'ont rien à faire ensemble. D'ailleurs, ce n'est même pas des algorithmes, officiellement c'est des preuves qui sont accessoirement constructive.

En passant, je me suis fait refuser le papier d'où je sors ça. Parait qu'il y a de la place pour améliorer la rédaction. Alors même que le résultat est jugé intéressant (mais pas révolutionnaire non plus), non trivial, dans l'optique du journal, et sans faute mathématiques pour autant que les referee puissent dire. Je pense en écrivant ce billet que je vois un peu mieux pour quoi.