Comments on Premier article en calculabilité ?

@Arnaud Spiwack

Oui, tout énoncé est équivalent à "∃∀<qqc sans quantificateur>" mais on change le domaine de quantification. Si on n'a que des quantificateurs sur des entiers, ça doit changer quelque chose non ?

Enfin, je dis ça, mais je n'ai pas vraiment d'idées pour comment changer définir T4, et je ne m'y connais pas beaucoup en calculabilité. Mais je trouve ça passionnant de classifier des topologies de Lawvere-Tierney !

Concernant arxiv, tu évoques dans le post lié le pouvoir donné à Cornell. Arxiv annonce actuellement devenir une organisation à but non lucratif : https://tech.cornell.edu/arxiv/

Est-ce que ça va dans le sens de ce que tu souhaites ?

Je suis allé jusque "allant de gens qui ne connaissent rien en maths — même si ceux-ci ont probablement déjà arrêté de lire à ce point du billet", et j'ai lu la présentation pour comprendre au moins ce que sont globalement les degrés d'Arthur-Nimué-Merlin. :D :D
(Mais je suis satisfait hein. ^^)

A priori, je trouve cette notion de non-déterminisme parfaitement naturelle. Elle est partout en informatique (et il n'y a qu'une définition possible de réduction entre de telles fonctions).

Ça se trouve en théorie des automates (les automates alternants), ça se trouve en méthodes formelles (les predicate transformers, la “weakest precondition” de la logique de Hoare en est un exemple motivant; une partie de la théorie du raffinement d'état est fondée dans cette notion de predicate transformers; dans cet environment, les deux formes de déterminismes sont souvent connus comme “angélique” et “démoniaque”), les predicates transformers forment une algèbre de Kleene parfaitement naturelle (pour la composition, on peut la retrouver par le fait que A→𝒫(𝒫(B)) est isomorphe à 𝒫(B)→𝒫(A) et prendre la composition de ça; du coup, c'est même une catégorie enrichie dans les monoïdes commutatif (munie d'une étoile de Kleene de Hom(A,A) dans Hom(A,A)) et en ceci modélise tous les programmes impératifs, la séquence a même un adjoint d'un côté je crois (je me perd toujours dans les calculs et je n'ai jamais eu le courage de vérifier dans un assistant à la démonstration).

Par ailleurs, je ne pense pas qu'ajouter des joueurs change grand chose au moins si on raisonne classiquement: par skolemisation, toute formule peut se mettre sous la forme ∃∀<qqc sans quantificateur>.

BREF. Au delà de la motivation par les topologies de Lawvere-Tierney (qui me paraît très forte), tout ça m'a l'air de se justifier facilement.