Extension du théorème de Statman

Le théorème de Statman dit la chose suivante: la question de savoir si une formule propositionnelle est ou non un théorème de la logique intuitionniste est PSPACE-complete

Autrement dit, pour n'importe quel jeu de longueur finie fixée à l'avance, où chaque coup est une lettre de l'alphabet, si tu disposes d'un "oracle" auquel tu peux poser des questions du genre "P est-elle un théorème intuitionniste?" alors avec un algorithme qui s'execute en temps polynomial $/$règles et longueur du jeu, tu peux gagner "mécaniquement" la partie.

La logique classique n'est "que" co-NP-complete...

Le problème dans tous ces énoncés est qu'ils ne concernent que des propositions finies. Donc, je propose ce fil où vous pourriez faire quelques suggestions pour étendre ces idées à des phrases "infiniment" longues (ie, fabriquées avec des conjonctions infinies et des implications)

Rappel: la logique intuitionniste est définie comme l'ensemble des formules obtenues par modus ponens et conjonction à partir des axiomes suivant:

1) $A\to (B\to A)$ (droit de jeter une hypothèse)

2) $[A\to (A\to ]\to (A\to $ (droit de dupliquer une hypothèse)

3) $(B\to C)\to ((A\to \to (A\to C))$ (droit de raisonner en plusieurs étapes)

4) $[A\to (B\to C)]\to [B\to (A\to C)]$ (droit de permuter des hypothèses)

5) $Conjonction\to $cas particulier

5bis) $($conjonction des $A\to X_i)\to (A\to $conjonction des $X_i)$

6) $tout\to A$

7) $A\to A$

8) (optionnel): $C\to (D\to Z)$ avec $D:=$disjonction des $A_i, i\in I$ et $C:=$conjonction des $(A_i\to Z), i\in I$

9) (optionnel): $A\to $disjonction dans laquelle $A$ figure

Les lettres majuscules représentent des propositions quelconques


Le modus ponens consiste à inférer B comme nouveau "théorème" quand $A\to B$ et $A$ ont préalablement été établis

La règle de conjonction consiste à inférer {\it conjonction des $A_i$} quand chaque $A_i$ a été prouvée préalablement

Définitions:

$\neg A:=A\to tout$