Ergebnisse in Theoretischen CS unabhängig von ZFC

Ich werde eine ziemlich vage Frage stellen, da die Grenze zwischen theoretischer Informatik und Mathematik nicht immer leicht zu unterscheiden ist.

FRAGE: Ist Ihnen ein interessantes Ergebnis in CS bekannt, das entweder unabhängig von ZFC (dh von der Standardsatztheorie) ist oder das ursprünglich in ZFC (+ ein anderes Axiom) und erst später in ZFC alorne nachgewiesen wurde?

Ich frage, weil ich kurz vor dem Abschluss meiner Doktorarbeit stehe und mein Hauptergebnis (die Bestimmbarkeit einer Klasse von Spielen, die verwendet werden, um einem probabilistischen modalen Kalkül eine " Spielsemantik " zu verleihen) im Moment bewiesen ist in ZFC erweitert mit anderen Axiomen (nämlich die Negation der Kontinuumshypothese und Martins Axiom ).$\mu$M $\neg CH$$MA$

Die Einstellung ist also eindeutig Informatik (der modale Kalkül ist eine zeitliche Logik und ich erweitere ihn, um mit probabilistischen Systemen zu arbeiten).$\mu$

Ich möchte in meiner Diplomarbeit andere Beispiele dieser Art anführen (falls Ihnen bekannt ist).

Danke im Voraus,

Tschüss

Matteo

Obwohl mir keine anderen Ergebnisse als Ihre bekannt sind, können Sie den Anwendungsbereich meines Erachtens etwas erweitern und fragen: Welche Ergebnisse in TCS wurden mit (jeder Art von) nicht standardmäßigen Axiomen bewiesen? Mit Nicht-Standard meine ich hier etwas anderes als klassische Logik mit ZF (oder ZFC).

Ein schönes Beispiel für die Art von Arbeit, an die ich denke, sind Alex Simpsons Ergebnisse zu Eigenschaften von Programmiersprachen unter Verwendung der Theorie der synthetischen Domänen. Er verwendet die intuitionistische Mengenlehre mit Axiomen, die der klassischen Logik widersprechen.

Außerdem verwendeten Alex und ich intuitionistische Axiome mit antiklassischen Kontinuitätsprinzipien, um Ergebnisse über die Banach-Mazur-Kompatibilität zu zeigen.

Keines der genannten Beispiele hat jedoch einen "offenen" Status wie Ihre Beweise, da wir wissen, dass die von uns verwendeten nicht-standardmäßigen Axiome einfach als Arbeiten in einem Modell der intuitionistischen Mathematik verstanden werden können, in dem gezeigt werden kann, dass das Modell existiert in ZFC. Das nicht standardmäßige Setup ist also eine Möglichkeit, die Dinge eleganter zu machen, und im Prinzip könnten sie in reinem ZFC durchgeführt werden (obwohl ich Angst habe, darüber nachzudenken, wie genau das gehen würde).

Es hängt von Ihrer Definition von "Informatik" ab. Nehmen Sie das folgende Beispiel - zählt es?

Eine Codierung der ganzen Zahlen ist ein eindeutig decodierbarer Binärcode von . Wenn die Länge der Codewörter nicht abnimmt, nennen wir den Code monoton . Ein Code ist besser als ein Code wenn . Mit anderen Worten, für jedes sind die Codewörter von von einem Punkt an mindestens Bits kürzer.C 1 C 2 | C 1 ( n ) | - | C 2 ( n ) | → - ∞ L C 1$\mathbb{N}$$C_1$$C_2$$|C_1(n)| - |C_2(n)| \rightarrow -\infty$$L$$C_1$$L$

Ein Satz von Codes heißt kofinale wenn für jeden Code gibt einen Code , die besser ist , als . Es ist gut geordnet, wenn es in Bezug auf "besser" gut geordnet ist. Eine Skala ist eine geordnete Gruppe von Codes.C D ∈ S $S$$C$$D \in S$$C$

Hier sind zwei von ZFC unabhängige Eigenschaften:

1. Es gibt eine Skala von Codes.
2. Es gibt eine Skala von monotonen Codes (dh eine gut geordnete Menge von monotonen Codes, die in der Menge aller monotonen Codes endgültig ist).

Ein Konus von Turing Grad ist ein Satz von Graden mit einiger Basis , so daß für alle Grade , , wenn und nur wenn .b ∈ D c b ≤ T c c ∈ $D$$b \in D$$c$$b \leq_T c$$c \in D$

Die Aussage zur Turing-Grad-Bestimmtheit :

Jeder Satz von Turing-Graden enthält entweder einen Kegel oder ist von einem Kegel getrennt

ist eine Folge des von ZF unabhängigen und mit ZFC inkompatiblen Determinantenaxioms (AD). Die schwächere Aussage

Jede unter Turing-Äquivalenz abgeschlossene Borel-Menge von Real enthält entweder einen Kegel oder ist von einem Kegel getrennt

ist eine Konsequenz von Martins Satz über die Borel-Determiniertheit, die in ZFC bewiesen werden kann. Beide Aussagen wurden untersucht, bevor Martins Ergebnis zur Borel-Bestimmbarkeit bewiesen wurde. Zu diesem Zeitpunkt war nur bekannt, dass beide Aussagen in ZF + AD nachweisbar sind.

Das zweitzitierte Ergebnis hat die folgende interessante Schlussfolgerung: Angenommen, ist eine unter Turing-Äquivalenz geschlossene Borel-Menge von Reellen, so dass für jedes reelle ein mit (dies besagt nur, dass nach oben dicht ist in den Turinggraden). Dann muss einen ganzen Kegel von Turing-Graden enthalten.b c ∈ S b ≤ T C S $S$$b$$c \in S$$b \leq_T c$$S$$S$

Ich habe kürzlich an einem Vortrag über die Bestimmung von Büchi-Spielen mit einem Zähler teilgenommen: Olivier Finkel, Die Bestimmung von kontextfreien Spielen , STACS 2012, http://drops.dagstuhl.de/opus/volltexte/2012/ 3389 / pdf / 5.pdf .

Viel konstruktive Mathematik. Siehe Per Martin-Löfs Arbeit zur konstruktiven Mengenlehre, die als Grundlage für abhängig typisierte Programmiersprachen dient.