Comments on La réalisabilité de Kleene (comme prélude au topos effectif)

Je me permets de signaler que je serais également très intéressé par une introduction au « topos effectif ».

@JML oui ce n'est pas clair, mais il est indiqué plus haut :

> il existe une formule T(e,n,x), le "prédicat T de Kleene", qu'on peut écrire explicitement mais je ne le ferai pas, et qui est même à quantificateurs bornés

Je soupçonne que ça ait un lien avec la mention "et même primitive récursive" encore avant (en tout cas il faut bien quelques hypothèses pour se ramener à des quantificateurs bornés).

Chouette une entrée de maths :)

« ∃x.T(e,n,x) […] d'après ce qu'on vient de dire, un tel entier existe si et seulement si la formule est vraie »
Il me semble qu'on est maintenant sur une formule qui a un quantificateur non borné et qu'il faut ajouter un argument à ce qu'on vient de dire.
Mais il faut avouer qu'une bonne compréhension de cette entrée nécessiterait que j'investisse bien plus qu'une lecture attentive vu mon manque de bases… Merci du voyage en tout cas !

> je ne sais même pas bien ce que Kleene cherchait à faire en introduisant cette notion.

Je ne sais pas non plus, je ne me suis pas vraiment penché sur la question. Mais il me semble qu'une des choses qu'il en a fait, c'est prouver des théorèmes indépendance. Typiquement, je crois que c'est comme ça qu'il a montré que le Fan Theorem (une version constructive du Lemme de Kőnig que Brouwer utilisait dans ses mathématiques intuitionnistes, cf https://en.wikipedia.org/w/index.php?title=K%C5%91nig%27s_lemma&oldid=986614246#Relationship_to_constructive_mathematics_and_compactness ) n'était pas une conséquence du reste des maths constructives.

> je pense que la façon de continuer est vraiment de définir le topos effectif, et je ne vais pas me lancer dedans maintenant.

Bouh 😢 .

--

Sans rapport, tout ça, mais je ne me questionne beaucoup sur la pertinence de présenter la réalisabilité de Kleene avec des entiers naturels de nos jours. Alors que la notion de programme est quand-même plutôt bien comprise. Le fait que Kleene était un fan dévoué d'écrire les trucs dans le langage formel l'arithmétique est-il toujours pertinent?