Martin Steel Woodin

J'essaierai de le retour ver. Mots clés : étudiant de Jacques Duparc ayant rédigé la preuve de Martin Steel dans un mémoire.

Voilà le lien : https://www.irif.fr/~pequignot/Pdf/master_thesis.pdf

@Martial : Malheureusement, ce n'est pas possible.
Si c'était possible cela serait très dangereux. Il y aurait plein de gens qui utiliserait cette intelligence à mauvais escient et patatrac, tout s'écroule, même les ponts.

Moralité vivent les simples d'esprit.

Intelligemment votre,
zephir.

De rien et je confirme que 99.5% de la difficulté de la preuve de la détermination borélienne est dans le fait de ramener un ensemble ouvert à un ouvert-fermé . Les ordinaux limite ne sont pas difficiles à gérer, c'est de la routine notationnelle (ie un argument catégorique): il est habituel que les TDE-istes (à tort ou à raison) considèrent tout théorème de categorie comme trivial et le laissent au lecteur.

Non ne t'inquiète pas. La plupart des choses sont intuitives. Les catégories ont juste "mis en vocabulaire" ces choses. La théorie plus "professionnelle" et spécialisée que les categoriciens utilisent n'intervient pas en forment dans l'infinitisme elle ne sert qu'à faire progresser l'algèbre (ie la résolutions n des équations diophantiennes in fine puisque ce problème n'est pas récursif).

Or pour la thématique ensembliste infinitiste ou consistencystrentghique tout se passe comme si on disait qu'on dispose d'un oracle qui DONNE GRATUITEMENT l'ensemble vérité de (IR, IN, +,×).

C'est ça qui fait que quand un énoncé est absolu et vrai la TDE le laisse au lecteur. Mais attention les TDEistes sont humains et bienveillants, il ne laissent pas au lecteur RH ou Fermat, ils essaient d'être sincères et de ne pas tromper leurs lecteurs. Ce qu'ils laissent ce sont des évidences comme Yoneda etc c'est à dire des trucs où l'ENONCE est suffisant et où la preuve ne présente pas d'intérêt. Mais ils ne privent pas les gens de l'énoncé et l'écrive t en général sans qu'il y ait besoin de pré-requis.

Anecdote: GG a été bloqué par le même problème dans un autre fil ce matin.

C'est parce que Martial en parlait. J'ai essayé de préciser les non dits sous-jacent à la littérature ensembliste et ses motivations.

Il évoquait le fait que Louveau avait laissé au lecteur de prendre une limite inductive en disant "c'est des catégories c'est trivial" et je précisais que dans ce contexte le mot "trivial" désigne "on admet de toute façon le truc et si vous voulez le faire en exo, you are welcome". Ca me semble utile puisque si on détaillait les passages catégoriques dans les paragraphes ensemblistes, on passerait de paragraphes de 15 lignes à des gros ventres de 20 pages et ce serait imbitable (multiplication des textes par plus de 30). Par exemple Martin Steel ferait .... 2000 pages (et peut-être nettement plus parce que les identifications catégoriques y occupent carrément une place assez "envahissantes" (on utilise des arbres de plongements élémentaires dans tous les sens, et on inductive les extrémités (les branches bien fondées) pour en obtenir de nouveaux (le tout sachant que PE n'est pas un objet de l'univers mais que seul l'extender qui l'induit l'est)