Résultats en CS théorique indépendants de ZFC

Je vais poser une question assez vague, car la frontière entre l'informatique théorique et les mathématiques n'est pas toujours facile à distinguer.

QUESTION: Connaissez -vous des résultats intéressants dans CS qui sont indépendants de ZFC (c'est-à-dire de la théorie des ensembles standard) ou qui ont été prouvés à l'origine dans ZFC (+ un autre axiome) et seulement plus tard dans ZFC alorne?

Je pose la question parce que je suis sur le point de terminer ma thèse de doctorat et que mon principal résultat (la détermination d’une classe de jeux utilisée pour donner la "sémantique de jeu" à un calcul modal probabiliste ) est pour le moment prouvé dans ZFC étendu avec d'autres axiomes (à savoir la négation de l'hypothèse de Continuum ¬ C H et, Axiome M A de Martin ).$\mu$$\neg CH$$MA$

Le réglage est donc clairement informatique (le modal calcul est une logique temporelle, et je l’étend au travail avec des systèmes probabilistes).$\mu$

J'aimerais citer dans ma thèse d'autres exemples de ce type (si vous en connaissez).

Merci d'avance,

au revoir

Matteo

Bien que je ne sois pas au courant de tels résultats, autres que les vôtres, je pense que vous pourriez élargir quelque peu la portée et demander: quels sont les résultats obtenus par le SDC utilisant des axiomes non standard. Par non standard, j'entends autre chose que la logique classique avec ZF (ou ZFC).

Les résultats d'Alex Simpson sur les propriétés des langages de programmation utilisant la théorie des domaines synthétiques constituent un bel exemple du type de travail auquel je pense. Il utilise la théorie des ensembles intuitionniste avec des axiomes en contradiction avec la logique classique.

Alex et moi avons également utilisé des axiomes intuitionnistes avec des principes de continuité anti-classiques pour montrer des résultats concernant la calculabilité de Banach-Mazur.

Cependant, aucun des exemples cités n’a un statut "ouvert", à l’instar de vos preuves, car nous savons que les axiomes non standard que nous avons utilisés peuvent être simplement compris comme s’appuyant sur un modèle de mathématiques intuitionnistes, dans lequel le modèle peut être démontré. dans ZFC. Donc, la configuration non standard est vraiment une façon de faire les choses plus élégamment, et en principe, elles pourraient être faites directement en ZFC (bien que je craigne de penser à comment exactement cela irait).

Cela dépend de votre définition du terme "informatique". Prenons l'exemple ci-dessous - ça compte?

Un codage des entiers est un code binaire de décodable de manière unique . Si la longueur des mots de code n'est pas décroissante, nous appelons le code monotone . Un code C 1 est mieux qu'un code C 2 si | C 1 ( n ) | - | C 2 ( n ) | → - ∞ . En d' autres termes, pour chaque L , d'un point sur les mots de code C 1 sont au moins L bits de plus courte.$\mathbb{N}$$C_1$$C_2$$|C_1(n)| - |C_2(n)| \rightarrow -\infty$$L$$C_1$$L$

Un ensemble de codes est appelé cofinal si pour tout le code C il y a un code D ∈ S qui est mieux que C . Il est bien ordonné s'il est bien ordonné en ce qui concerne "mieux". Une balance est un ensemble de codes cofinal bien ordonné.$S$$C$$D \in S$$C$

Voici deux propriétés indépendantes de ZFC:

1. Il existe une échelle de codes.
2. Il existe une échelle de codes monotones (c’est-à-dire un ensemble de codes monotones bien ordonné cofinal dans l’ensemble des codes monotones).

Un cône de degrés de Turing est un ensemble de degrés avec une certaine base de b ∈ D tel que pour tous les degrés c , b ≤ T c si et seulement si c ∈ D .$D$$b \in D$$c$$b \leq_T c$$c \in D$

La déclaration de la détermination du degré de Turing :

Chaque ensemble de degrés de Turing contient un cône ou est disjoint d'un cône

est une conséquence de l’axiome de la détermination (AD), qui est indépendant de ZF et incompatible avec ZFC. La déclaration plus faible

Chaque ensemble de réels de Borel qui est fermé sous l’équivalence de Turing contient un cône ou est disjoint d’un cône

est une conséquence du théorème de Martin sur la détermination de Borel, qui est prouvable dans ZFC. Ces deux déclarations ont été étudiées avant que le résultat de Martin sur le déterminisme de Borel ne soit prouvé. À ce moment-là, on savait seulement qu'elles étaient toutes deux prouvables dans ZF + AD.

Le deuxième résultat cité a la conclusion intéressante suivante: supposons que soit un ensemble de réels de Borel fermés sous une équivalence de Turing telle que pour tout réel b, il existe un certain c ∈ S avec b ≤ T c (cela indique simplement que S est ascendant dense les degrés de Turing). Alors S doit contenir un cône entier de degrés de Turing.$S$$b$$c \in S$$b \leq_T c$$S$$S$

J'ai récemment assisté à un entretien avec l'un de ces résultats sur la détermination des jeux Büchi à un compteur: Olivier Finkel, Détermination des jeux sans contexte , STACS 2012, http://drops.dagstuhl.de/opus/volltexte/2012/ 3389 / pdf / 5.pdf .

Beaucoup de mathématiques constructives. Voir les travaux de Per Martin-Löf sur la théorie des ensembles constructive, utilisée comme base pour les langages de programmation typés de manière dépendante.