Là je l'ai écrit avec la syntaxe OCaml, mais l'idée était la même : une entier est soit zéro, soit le successeur d'un entier. Avec comme principe fondamental pour raisonner sur ce concept, le principe du raisonnement par récurrence (ou de manière équivalente, tout sous-type des entiers a un plus petit élément).
Pour donner une référence, c'est ainsi que Poincaré présentait l'arithmétique dans la Science et l'Hypothèse (ou la Valeur de la Science, je ne sais plus lequel des deux).
Pour l'encodage des entiers dans ZF et sa théorie des ordinaux, cela a son intérêt mais ZF (la théorie axiomatique des ensembles) est une théorie un peu étrange qui ne manipule pas des ensembles au sens où on l'entend usuellement. Quand tu dis que tu admets sans détails les principes de cette théorie, c'est en fait plutôt ceux de la théorie des types que tu as en tête (bien que tu appelles ensembles ce que cette théorie appelle types).
Je n'ai pas le temps de développer plus sur le sujet ce soir, mais j'essaierai demain ou dans le week-end.
Sapere aude ! Aie le courage de te servir de ton propre entendement. Voilà la devise des Lumières.
[^] # Re: L'analyse au delà de l'agrégation
Posté par kantien . En réponse à la dépêche Le Frido 2018, livre libre de mathématique pour l’agrégation. Évalué à 3. Dernière modification le 14 septembre 2018 à 00:45.
Si, on les définissait ainsi :
Là je l'ai écrit avec la syntaxe OCaml, mais l'idée était la même : une entier est soit zéro, soit le successeur d'un entier. Avec comme principe fondamental pour raisonner sur ce concept, le principe du raisonnement par récurrence (ou de manière équivalente, tout sous-type des entiers a un plus petit élément).
Pour donner une référence, c'est ainsi que Poincaré présentait l'arithmétique dans la Science et l'Hypothèse (ou la Valeur de la Science, je ne sais plus lequel des deux).
Pour l'encodage des entiers dans ZF et sa théorie des ordinaux, cela a son intérêt mais ZF (la théorie axiomatique des ensembles) est une théorie un peu étrange qui ne manipule pas des ensembles au sens où on l'entend usuellement. Quand tu dis que tu admets sans détails les principes de cette théorie, c'est en fait plutôt ceux de la théorie des types que tu as en tête (bien que tu appelles ensembles ce que cette théorie appelle types).
Je n'ai pas le temps de développer plus sur le sujet ce soir, mais j'essaierai demain ou dans le week-end.
Sapere aude ! Aie le courage de te servir de ton propre entendement. Voilà la devise des Lumières.