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

37

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 ).μ¬CHMA

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).μ

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

Merci d'avance,

au revoir

Matteo

IamMeeoh
la source
9
Ces questions précédentes pourraient être utiles: cstheory.stackexchange.com/questions/4816/… cstheory.stackexchange.com/questions/1923/…
Mark Reitblatt le
9
J'allais répondre que Matteo Mio et Alex Simpson ont utilisé Axiom de Martin pour prouver des résultats très intéressants ...
Andrej Bauer
7
C'est peut-être le meilleur exemple que j'ai vu d'une question dont la meilleure réponse est contenue dans la question elle-même! Je n'étais pas au courant de votre résultat très intéressant.
Timothy Chow

Réponses:

19

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).

Andrej Bauer
la source
Merci! Je demanderai à alex plus de détails à ce sujet lors de la rédaction de l'introduction.
IamMeeoh
13

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.NC1C2|C1(n)||C2(n)|LC1L

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é.SCDSC

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).
Yuval Filmus
la source
Bonjour Yuval, merci pour la réponse. Je ne suis pas sûr que votre exemple corresponde à ma définition "Informatique". Parler de "codes" ne suffit certainement pas pour le classer comme CS. Ce qui rend un papier "un papier CS" à l’imho est le suivant: est-il paru dans une conférence / journal CS, ou a-t-il été utilisé pour prouver un résultat dans une conférence / journal CS? par CS paper, je suis assez flexible mais les sujets peuvent être "théorie de l'information, complexité, logique de programme / système, théorie de la récursivité", etc. de codes "? Merci! Au revoir
IamMeeoh
1
Les articles sur les codes des nombres entiers apparaissent dans des journaux de génie électrique, tels que les transactions IEEE sur la théorie de l'information. Cela frappe l'un de vos mots-clés.
Yuval Filmus
1
Je ne pense pas qu'il y ait de papier utilisant ces résultats. De plus, je suis fermement convaincu qu'un résultat indépendant de ZFC n'a aucune utilité en termes de complexité. Votre question concerne donc dans une certaine mesure l'extension des limites de ce que l'on considère comme une science informatique.
Yuval Filmus
1
Bonjour Yuval, permettez-moi tout d'abord de vous remercier à nouveau pour vos réponses. Je ne suis pas d'accord avec votre position forte cependant. Par exemple, le théorème de Robertson-Seymour (qui semble nécessiter un choix) a des conséquences importantes en termes de complexité. Il est donc clair que le choix est utile (peut-être un peu surprenant) dans la théorie de la complexité. Maintenant, travailler avec des extensions cohérentes de ZFC simplifie évidemment la tâche de prouver, par exemple de complexité, des résultats, même si ces résultats sont peut-être prouvables dans ZFC mais personne ne sait comment, pour le moment.
IamMeeoh
1
De plus, je ne vois pas pourquoi il ne devrait pas y avoir de résultats concrets dans une complexité indépendante de ZFC, de la même manière que le théorème de Robertson-Seymour est (peut-être) indépendant de ZF.
IamMeeoh
9

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 .DbDcbTccD

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.SbcSbTcSS

Carl Mummert
la source
0

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.

Rob
la source
6
La théorie des types de IIRC, Martin-Lof a la même force de consistance que la théorie des ensembles de Kripke-Platek, qui est beaucoup plus faible que la ZFC. En outre, MLTT n’a pas de principes explicitement anti-classiques, comme les axiomes de continuité mentionnés par Andrej.
Neel Krishnaswami
@Neel, je n'ai jamais rien dit sur la cohérence ou la force de MLTT. Cependant, j'estime que certains résultats en mathématiques constructives sont pertinents pour la question, demandant "un résultat intéressant dans CS qui est ... indépendant de ZFC".
Rob
5
Je suppose que le terme "indépendant" désigne ici le sens formel.
Mark Reitblatt