Comments on La réalisabilité propositionnelle, et ce qu'elle nous apprend sur les algorithmes

> Il y a quelques éléments d'information dans le survey « The Disjunction Property of Intermediate Logics » de Chagrov et Zakharyashchev (*Studia Logica* 1991, <URL: https://www.jstor.org/stable/20015573 >).

Merci, je rajoute ça à mon dossier des n-millions de livres/articles scientifiques que j'ai envie de lire depuis une éternité. (Et j'ai fumé l'autre jour avec mon histoire d'élimination des coupures, quand on rajoute ces schémas d'axiome, bah ça ne marche plus du tout.)

4. Vu que la valeur d'un témoin (d'une promesse) ne compte pas, il est plus intéressant de dire que le programme doit toujours terminer, mais que la valeur retournée n'est consultée que dans l'autre cas.

3. Ah, et est-ce qu'il y aurait un bi-rapport entre typage / réalisabilité et types à la Church / types à la Curry?

1. Plutôt que "promesse", je dirais "témoin".

2. Cette histoire de réalisabilité me rappelle la "computability logic" de Giorgi Japaridze. Mais penser à ce qui est pareil ou diffère me fait mal à la tête.

Encore un commentaire et j'arrête mon monologue, promis. J'ai quand même posé la question sur ≲ à des gens qui s'y connaissent, et on m'a dirigé… vers un obscur papier en Russe de 1968 d'un certain Jankov. <URL:https://www.cambridge.org/core/journals/journal-of-symbolic-logic/article/abs/v-a-jankov-constructing-a-sequence-of-strongly-independent-superintuitionistic-propositional-calculi-english-translation-of-xxxvii-2066-by-a-yablonsky-soviet-mathematics-vol-9-no-4-1968-pp-806807-v-a-jankov-the-calculus-of-the-weak-law-of-excluded-middle-english-translation-of-xxxvii-2067-mathematics-of-the-ussrizvestija-providence-vol-2-no-5-for-1968-pub-1969-pp-9971004/A6411145CBFEB629DD444BA00FCA6721> Tiens donc 🙂 Et la réponse est qu'on sait que ≲ n'est pas un beau préordre (à double titre, en fait : ≲ n'est ni bien fondé ni à antichaînes finies).

Ah, c'est ballot. Je reviens au billet, je clique sur le lien « publiée en 2002 », je lis la première phrase de <URL:https://link.springer.com/chapter/10.1007/3-540-45793-3_6> : « It is unknown, whether the logic of propositional formulas that are realizable in the sense of Kleene has a finite or recursive axiomatization. ». Question résolue.

Ouf, Control-P → 24 pages de maths… Heureusement que ça se lit bien. C'est fascinant, merci ! Ça me fait me sentir moins bête que tu aies aussi été surpris que réalisable n'implique pas intuitionnistement prouvable (j'avais conscience de la différence et je pensais vaguement que ça ferait une différence au premier ordre, mais je n'aurais jamais imaginé qu'il y ait déjà une différence au niveau propositionnel). D'une manière générale, j'apprécie vraiment sur ce blog que contrairement à beaucoup de livres de maths, on n'a pas uniquement les faits, mais on le sait quand une affirmation est surprenante, ou bien triviale, ou bien quand une question qu'on a naturellement envie de se poser n'a pas de réponse connue, ou quand une démonstration a l'air simple mais qu'elle a mis 20 ans à être trouvée, …

La question qui me vient immédiatement à l'esprit, c'est : est-ce qu'on sait si l'ensemble des formules réalisables est engendré à partir de la logique intuitionniste en supposant un nombre fini de formules avec leurs raffinements, de même que la logique classique est formée en supposant l'unique formule P ∨ ¬P avec ses raffinements, et que la logique du tiers exclu faible est formée en supposant l'unique formule P ∨ ¬¬P avec ses raffinements ?

Plus précisément, si j'ai une formule F, je peux former un schéma d'axiome

__________________________________ (P1, …, Pn variables, G1, …, Gn formules)
⊢ F[P1:=G1, P2:=G2, …, Pn:=Gn]

Est-ce qu'on obtient les formules réalisables comme ensemble des formules prouvables en rajoutant au calcul des séquents intuitionniste un nombre fini de tels schémas d'axiome ?

Si on savait que oui, ce serait forcément dans ce billet vu que ça clorait complètement la question de « mais qu'est-ce qu'on peut faire exactement pour réaliser une formule ». Est-ce que par hasard, dans le peu qu'on sait de la réalisabilité, on sait quand même que non, ou bien est-ce qu'on ne sait pas ?

Autre point de vue : je peux définir un préordre ≲ sur les formules propositionnelles par X ≲ Y ssi (∀̅ X) ⇒ (∀̅ Y) est prouvable dans la logique propositionnelle intuitionniste du second ordre (où ∀̅ veut dire qu'on quantifie universellement toutes les variables libres, en particulier X ≲ Y est plus faible que « X ⇒ Y intuitionnistement »). La question est alors de savoir si l'ensemble des formules réalisables, qui est clos par le haut et dirigé vers le bas, est un cône, c'est à dire qu'il s'écrit comme ↑{F} := {G | F ≲ G}. Si ≲ est un beau préordre, alors c'est forcément oui, mais je ne crois pas que ≲ soit un beau préordre. Enfin, je ne peux plus réfléchir, là.

D'ailleurs, si c'était oui, alors je crois que le problème de savoir si une formule est réalisable serait automatiquement décidable (on doit pouvoir faire de l'élimination des coupures dans le calcul des séquents enrichi de ces schémas d'axiome pour récupérer la propriété de la sous-formule).