Conséquences informatiques du théorème du point fixe de décalage supérieur de Friedman (non démontrable)?

Harvey Friedman a montré qu'il existe un résultat net précis qui ne peut pas être prouvé en ZFC (la théorie des ensembles de Zermelo-Frankel habituelle avec l'Axiom of Choice). De nombreuses logiques modernes sont construites sur des opérateurs à virgule fixe, alors je me demandais: y a-t-il des conséquences connues du théorème du point fixe du décalage supérieur pour l'informatique théorique?

Théorème de point fixe de décalage supérieur non démontrable
Pour tous les , certains contient .A = cube ( A , 0 ) ∖ R [ A ] us ( A $R \in \text{SDOI}(Q^k,Q^k)$$A = \text{cube}(A,0) \setminus R[A]$$\text{us}(A)$

Le théorème de l'USFP semble être une instruction , il pourrait donc être "assez proche" de la calculabilité (comme la vérification de la non-isomorphisme des structures automatiques), pour avoir un impact sur l'informatique théorique.$\Pi^1_1$

Pour être complet, voici les définitions du discours de Friedman au MIT de novembre 2009 (voir aussi le projet de livre sur la «théorie des relations booléennes» ).

x , y ∈ Q k 1 ≤ i , j ≤ k x i < x j ⇔ y i < y j x ∈ Q $Q$ est l'ensemble des nombres rationnels. sont des ordres équivalents si à chaque fois puis . Lorsque le décalage supérieur de , noté , est obtenu en ajoutant 1 à chaque coordonnée non négative de . Une relation est invariante de commande si pour tout ordre invariant équivalent il estime que . Une relation$x, y \in Q^k$$1 \le i,j \le k$$x_i \lt x_j \Leftrightarrow y_i \lt y_j$$x \in Q^k$us ( x ) x A ⊆ Q $x$$\text{us}(x)$$x$$A \subseteq Q^k$ x ∈ A ⇔ y ∈ A R ⊆ Q k × Q $x,y \in Q^k$$x \in A \Leftrightarrow y \in A$$R \subseteq Q^k \times Q^k$est invariant par ordre si est invariant par ordre comme un sous-ensemble de , et est strictement dominant si pour tout chaque fois que alors . De plus, si A est un sous-ensemble de Q ^ k, alors R [A] désigne \ {y | \ existe x \ dans AR (x, y) \} , le décalage supérieur de A est \ text {us} (A) = \ {\ text {us} (x) | x \ dans A \} , et \ text {cube} (A, 0) désigne le moins B ^ k tel que 0 \ dans B et A est contenu dans B ^ k . LaisserQ 2 $R$$Q^{2k}$$x,y \in Q^k$$R(x,y)$$\max(x) \lt \max(y)$$A$$Q^k$$R[A]$$\{ y | \exists x \in A R(x,y)\}$$A$$\text{us}(A) = \{\text{us}(x) | x \in A\}$$\text{cube}(A,0)$$B^k$$0 \in B$$A$$B^k$$\text{SDOI}(Q^k,Q^k)$ désigne l'ensemble de toutes les relations invariantes d'ordre strictement dominant $R \subseteq Q^k \times Q^k$ .

Edit: Comme le fait remarquer Dömötör Pálvölgyi dans les commentaires, prendre et comme ordre habituel sur les rationnels semble donner un contre-exemple. Tout d'abord, l'ensemble ne peut pas être vide, car est alors également vide et devrait alors contenir 0 par la condition de cube, une contradiction. Si l'ensemble non vide a un minimum, il ne peut pas contenir de rationnels supérieurs à celui-ci, il doit donc être un singleton, ce qui contredit la condition de décalage supérieur. Si par contre n'a pas d'infimum alors donc doit être vide, une contradiction. $k=1$$R$$A$$R[A]$$A$$A$R [ A ] = Q $A$$R[A] = Q$$A$Avez-vous des commentaires sur la présence de problèmes de définition cachés et non évidents, comme peut-être un modèle implicite non standard des justifications?

Édition supplémentaire: L'argument ci-dessus est à peu près correct, mais est incorrect dans l'application du décalage supérieur. Cet opérateur ne s'applique qu'aux coordonnées non négatives , donc le fait de définir comme tout ensemble singleton négatif donne un point fixe, comme vous le souhaitez. En d'autres termes, si alors est une solution, et il n'y a pas d'autres solutions.m < 0 A = { m $A$$m < 0$$A = \{m\}$

Je ne connais aucune conséquence de ce théorème particulier, mais les preuves de normalisation des calculs lambda comme le calcul des constructions inductives reposent sur de grands axiomes cardinaux - même si l'ensemble des termes lambda est aussi dénombrable que vous le souhaitez.

Je pense que la meilleure façon de comprendre la signification informatique des axiomes de la théorie des ensembles affirmant l'existence de grands cardinaux est de penser la théorie des ensembles comme un moyen de formuler la théorie des graphes. C'est-à-dire qu'un modèle d'un ensemble est une collection d'éléments équipés d'une relation binaire utilisée pour interpréter l'appartenance. Ensuite, les axiomes de la théorie des ensembles vous indiquent les propriétés de la relation d'appartenance, y compris comment vous pouvez former de nouveaux ensembles à partir d'anciens. En particulier, l'axiome de la fondation signifie que la relation d'appartenance est bien fondée (c'est-à-dire qu'elle n'a pas de chaînes descendantes infinies). Ce bien-fondé signifie à son tour que si vous pouvez aligner les états d'exécution d'un programme avec l'appartenance transitive des éléments d'un ensemble, alors vous avez une preuve de terminaison.

Ainsi, une affirmation selon laquelle un "grand" ensemble existe a un gain de calcul comme une revendication qu'une certaine classe de boucles dans un langage de programmation récursif général se termine. Cette interprétation fonctionne uniformément, depuis le vieil axiome ordinaire de l'infini (qui justifie l'itération des nombres naturels) jusqu'aux grands axiomes cardinaux.

Ces axiomes sont-ils vrais ? Eh bien, si l'axiome est faux, vous pouvez trouver un programme dans l'une de ces classes qui ne se termine pas. Mais si c'est vrai, nous n'en serons jamais sûrs, grâce au théorème de Halting. Tout, depuis l'induction des nombres naturels, est une question d' induction scientifique , qui peut toujours être falsifiée par l'expérience - Edward Nelson espère que prouver que l'exponentiation est une fonction partielle!