Welche interessanten Sätze in TCS stützen sich auf das Axiom of Choice? (Oder alternativ das Axiom of Determinacy?)

67

Mathematiker sorgen sich manchmal um das Axiom of Choice (AC) und das Axiom of Determinancy (AD).

Axiom of Choice : Bei einer gegebenen Sammlung nicht leerer Mengen gibt es eine Funktion f , die bei gegebener Menge S in C ein Mitglied von S zurückgibt .CfSCS

Axiom of Determinacy : Sei eine Menge unendlich langer Bitketten. Alice und Bob spielen ein Spiel, bei dem Alice ein erstes Bit b 1 , Bob ein zweites Bit b 2 usw. auswählt, bis eine unendliche Zeichenfolge x = b 1 b 2 konstruiert ist. Alice gewinnt das Spiel , wenn x S , Bob das Spiel gewinnt , wenn x S . Die Annahme ist, dass es für jeden S eine Gewinnstrategie für einen der Spieler gibt. (Wenn zum Beispiel S nur aus der Einsen-Saite besteht, kann Bob in endlich vielen Zügen gewinnen.)Sb1b2x=b1b2xSxS SS

Es ist bekannt, dass diese beiden Axiome nicht miteinander vereinbar sind. (Denken Sie darüber nach, oder gehen Sie hierher .)

Andere Mathematiker schenken der Verwendung dieser Axiome in einem Beweis wenig oder gar keine Beachtung. Sie scheinen für die theoretische Informatik fast irrelevant zu sein, da wir glauben, dass wir hauptsächlich mit endlichen Objekten arbeiten. Da TCS Berechnungsentscheidungsprobleme als unendliche Bitfolgen definiert und wir (zum Beispiel) die zeitliche Komplexität eines Algorithmus als asymptotische Funktion über den Naturals messen, besteht immer die Möglichkeit, dass sich die Verwendung eines dieser Axiome verschlechtert in einige Beweise.

Was ist das auffälligste Beispiel in TCS, von dem Sie wissen, wo eines dieser Axiome erforderlich ist ? (Kennen Sie Beispiele?)

Beachten Sie, dass ein Diagonalisierungsargument (etwa über die Menge aller Turing-Maschinen) keine Anwendung des Axioms der Wahl ist. Obwohl die Sprache, die eine Turing-Maschine definiert, eine unendliche Bitfolge ist, hat jede Turing-Maschine eine endliche Beschreibung, so dass wir hier wirklich keine Auswahlfunktion für unendlich viele unendliche Mengen benötigen.

(Ich habe viele Tags gesetzt, weil ich keine Ahnung habe, woher die Beispiele kommen werden.)

Ryan Williams
quelle
CW? oder nicht ? nicht sicher.
Suresh Venkat
Ich bin mir auch nicht sicher ... dies ist eine Frage, bei der ich über die "Komplexität" der Antwort sehr unsicher bin ...
Ryan Williams
5
Andere Mathematiker schenken der Verwendung dieser Axiome in einem Beweis wenig oder gar keine Beachtung. Verwenden Mathematiker wirklich beide Axiome sorglos? Wenn Sie versehentlich beide Axiome annehmen, können Sie alles beweisen!
Warren Schudy
1
Harvey Friedmans Vermutung . Ich weiß nicht, ob es auch für die theoretische Informatik gilt.
Kaveh
1
Ich kenne kein Ergebnis in der theoretischen Informatik, das sich in ZF nicht nachweisen lässt, das sich aber in einer interessanten Erweiterung von ZF nachweisen lässt. Meine wilde Vermutung ist jedoch, dass selbst solche Ergebnisse wahrscheinlich nicht das volle Axiom der Wahl (AC) erfordern und dass sie nur eine schwächere Version von AC erfordern, wie das Axiom der abhängigen Wahl (DC) oder das noch schwächere Axiom der Zählbarkeit Wahl (AC_ω). Abgesehen davon stimmt DC (und damit AC_ω) mit dem Bestimmungsaxiom überein .
Tsuyoshi Ito

Antworten:

47

Jede in ZFC nachweisbare arithmetische Aussage ist in ZF nachweisbar und "benötigt" daher nicht das Axiom der Wahl. Mit einer "arithmetischen" Aussage meine ich eine Aussage in der Sprache erster Ordnung der Arithmetik, was bedeutet, dass sie nur unter Verwendung von Quantifizierern über natürlichen Zahlen angegeben werden kann ("für alle natürlichen Zahlen x" oder "es gibt eine natürliche Zahl x"). ohne über Mengen von natürlichen Zahlen zu quantifizieren . Auf den ersten Blick mag es sehr restriktiv erscheinen, die Quantifizierung über ganze Zahlenmengen zu verbieten. jedoch endliche Mengen von ganzen Zahlen können „codiert“ werden , um eine einzelne ganze Zahl verwendet wird , so ist es OK endliche Mengen von ganzen Zahlen zu quantifizieren über.

PNP

Aber warten Sie, Sie können sagen, was ist mit arithmetischen Aussagen, deren Beweis so etwas wie Koenigs Lemma oder Kruskals Baumsatz erfordert? Benötigen diese nicht eine schwache Form des Axioms der Wahl? Die Antwort ist, dass es genau darauf ankommt, wie Sie das fragliche Ergebnis angeben. Wenn Sie beispielsweise den Satz von Graph Minor in der Form angeben, dass "bei einer unendlichen Menge von unbeschrifteten Graphen zwei vorhanden sein müssen, so dass einer ein Minor des anderen ist", dann ist eine gewisse Auswahl erforderlich, um durch die Graphen zu marschieren Ihre unendlichen Datenmengen, die Auswahl von Eckpunkten, Untergraphen usw. [EDIT: Ich habe hier einen Fehler gemacht. Wie Emil Jeřábek erklärt, der Graph-Minor-Satz - oder zumindest die natürlichste Aussage in Abwesenheit von AC - ist in ZF nachweisbar. Aber modulo dieser Fehler, was ich unten sage, ist immer noch im Wesentlichen richtig. ] Wenn Sie jedoch stattdessen eine bestimmte Codierung der Nebenrelation auf beschrifteten endlichen Graphen durch natürliche Zahlen aufschreiben und den Satz von Nebengraphen als Aussage über diese bestimmte Teilreihenfolge formulieren, wird die Aussage arithmetisch und erfordert kein AC in der Beweis.

Die meisten Leute glauben, dass das "kombinatorische Wesen" des Graph-Minor-Theorems bereits von der Version erfasst wird, die eine bestimmte Kodierung festlegt, und dass die Notwendigkeit besteht, AC aufzurufen, um alles zu kennzeichnen, falls Ihnen die allgemeine Menge präsentiert wird. Die theoretische Version des Problems ist eine Art irrelevantes Artefakt der Entscheidung, die Mengenlehre anstelle der Arithmetik als logische Grundlage zu verwenden. Wenn Sie genauso denken, dann benötigt der Graph-Minor-Satz keine AC. (Siehe auch diesen Beitrag von Ali Enayat an die Mailingliste Foundations of Mathematics, geschrieben als Antwort auf eine ähnliche Frage, die ich einmal hatte.)

Das Beispiel der chromatischen Zahl der Ebene ist ebenfalls eine Interpretationssache. Es gibt verschiedene Fragen, die Sie stellen können und die sich als gleichwertig herausstellen, wenn Sie eine Wechselstromversorgung annehmen. Es handelt sich jedoch um unterschiedliche Fragen, wenn Sie keine Wechselstromversorgung annehmen. Aus TCS-Sicht ist der kombinatorische Kern der Frage die Färbbarkeit endlicher Teilgraphen der Ebene und die Tatsache, dass Sie dann (wenn Sie möchten) ein Kompaktheitsargument verwenden können (hier kommt AC ins Spiel), um etwas zu schließen über die chromatische Zahl der ganzen Ebene ist amüsant, aber von etwas tangentialem Interesse. Ich denke also nicht, dass dies ein wirklich gutes Beispiel ist.

Ich denke, letztendlich haben Sie vielleicht mehr Glück, wenn Sie sich die Frage stellen, ob es TCS-Fragen gibt, für deren Lösung große Kardinalaxiome erforderlich sind (und nicht AC). Die Arbeit von Harvey Friedman hat gezeigt, dass bestimmte finitäre Aussagen in der Graphentheorie große Kardinalaxiome (oder zumindest die 1-Konsistenz solcher Axiome) erfordern können. Friedmans bisherige Beispiele sind ein wenig künstlich, aber ich wäre nicht überrascht, wenn ähnliche Beispiele in unserem Leben "natürlich" in TCS auftauchten.

Timothy Chow
quelle
8
Um eine Normalisierung für typisierte Lambda-Rechnungen mit Polymorphismus zu beweisen, ist mindestens eine Arithmetik 2. Ordnung erforderlich, und um dies für die allgemeineren Typentheorien zu beweisen, sind möglicherweise große, wenn auch recht bescheidene Kardinalaxiome erforderlich. IIRC, Coqs Normalisierungsbeweis, benötigt zählbar viele unzugängliche Elemente, da Sie ihn zum Codieren von Universumsargumenten im Grothendieck-Stil verwenden können.
Neel Krishnaswami
3
@Neel: Guter Punkt, obwohl IMO diese Beispiele "betrügen", weil es ziemlich offensichtlich ist, dass Sie starke logische Axiome benötigen, um die Konsistenz eines logischen Systems zu beweisen.
Timothy Chow
4
Diese Antwort gefällt mir, weil sie erklärt, warum die Verwendung des Axioms der Wahl bei TCS äußerst selten erscheint.
Tsuyoshi Ito
11
Π31Π31ZFCZF
1
Diese Antwort wird vorgestellt auf dem Community - Blog.
Aaron Sterling
39

Ich verstehe, dass der bekannte Beweis für das Robertson-Seymour-Theorem das Axiom of Choice (über Kruskals Baumsatz) verwendet. Dies ist vom TCS-Standpunkt aus sehr interessant, da der Satz von Robertson-Seymour impliziert, dass Zugehörigkeitstests in einer gegebenen Familie von Graphen mit kleinen geschlossenen Graphen in polynomieller Zeit durchgeführt werden können. Mit anderen Worten kann das Auswahlaxiom verwendet indirekt zu beweisen , dass Polynomzeit Algorithmen existiert für bestimmte Probleme, ohne tatsächlich diese Algorithmen zu konstruieren.

Dies könnte jedoch nicht genau das sein, wonach Sie suchen, da nicht klar ist, ob hier tatsächlich eine Wechselstromversorgung erforderlich ist.

Janne H. Korhonen
quelle
Dies ist ein guter Anfang, da nicht bekannt ist, wie der Satz anders zu beweisen ist.
Ryan Williams
7
Wie auf der Wikipedia-Seite erwähnt, zeigt die Arbeit von Friedman, Robertson und Seymour über die Metamathematik des Graph-Minor-Theorems, dass der Graph-Minor-Theorem (eine Form von) Kruskals Baumsatz über der Basistheorie RCA_0 impliziert Der Baumsatz wird für den Graph-Minor-Satz in starkem Sinne benötigt. Ob dies jedoch bedeutet, dass das Axiom der Wahl für den Satz von graph minor erforderlich ist, ist eine etwas knifflige Frage. Es hängt in subtiler Weise davon ab, wie Sie den Graph-Minor-Satz angeben. Siehe meine Antwort für weitere Details.
Timothy Chow
7
Emil Jeřábek hat auf MathOverflow gezeigt, wie man den Satz von Robertson-Seymour ohne das Axiom der Wahl beweisen kann. Dies war für mich überraschend, da ich auch den Eindruck hatte, dass der Robertson-Seymour für unbeschriftete Diagramme eine Wechselstromversorgung benötigte, aber das war offensichtlich ein falscher Eindruck.
Timothy Chow
Also ist die akzeptierte Antwort tatsächlich falsch?
Andrej Bauer
@AndrejBauer: Wenn Sie sich auf meine Antwort beziehen, haben Sie Recht, dass das, was ich über Robertson-Seymour gesagt habe, falsch ist. Ich habe gerade versucht, meine Antwort zu bearbeiten, konnte es aber nicht. Vielleicht habe ich nicht genug Ruf, um einen so alten Beitrag zu bearbeiten.
Timothy Chow
21

Dies bezieht sich auf die Antwort von Janne Korhonen.

In den 80er und 90er Jahren gab es eine Reihe von Ergebnissen, die versuchten, die Axiomensysteme (mit anderen Worten die arithmetische Theorie) zu charakterisieren, die zum Nachweis von Erweiterungen des Kruskal-Baumsatzes (KTT; das ursprüngliche KTT stammt aus dem Jahr 1960) erforderlich sind. Insbesondere hat Harvey Friedman mehrere Ergebnisse nach dieser Linie bewiesen (siehe SG Simpson. Nicht-Beweisbarkeit bestimmter kombinatorischer Eigenschaften endlicher Bäume . In LA Harrington et al., Herausgeber, Harvey Friedmans Research on Foundations of Mathematics. Elsevier, Nordholland, 1985). . Diese Ergebnisse zeigten, dass (bestimmte Erweiterungen von) KTT "starke" Verständnisaxiome verwenden müssen (dh Axiome, die besagen, dass bestimmte Mengen von hoher logischer Komplexität existieren). Ich weiß nicht genau, ob KTT-Erweiterungen in ZF (ohne das Axiom der Wahl) nachweisbar sind.

Parallel zu diesem Ergebnisstrom wurde versucht, ihn über Rewrite-Systeme mit ("Theorie B") TCS zu verbinden . Die Idee ist, Umschreibungssysteme zu konstruieren (denken Sie an eine Art funktionale Programmierung oder Lambda-Kalkül-Programme), für die ihre Beendigung von bestimmten (Erweiterungen) von KTT abhängt (die ursprüngliche Verbindung zwischen KTT und der Beendigung von Umschreibungssystemen wurde von N bewiesen) Dershowitz (1982)). Dies impliziert, dass man starke Axiome braucht, um zu zeigen, dass bestimmte Programme enden (da KTT-Erweiterungen solche Axiome benötigen). Für diese Art von Ergebnissen siehe zB A. Weiermann, Komplexitätsgrenzen für einige endliche Formen von Kruskals Theorem , Journal of Symbolic Computation 18 (1994), 463-488.

Iddo Tzameret
quelle
16

R2

In Shelah und Soifer, "Axiom der Wahl und chromatische Zahl der Ebene" , wird gezeigt, dass, wenn alle endlichen Teilgraphen der Ebene vierfarbig sind, dann

  • Wenn Sie das Axiom der Wahl annehmen, ist die Ebene vierfarbig.
  • Wenn Sie das Prinzip der abhängigen Auswahl annehmen und alle Mengen Lebesgue-messbar sind, ist die Ebene fünf-, sechs- oder siebenfarbig.
Derrick Stolee
quelle
Ist das nicht mehr mathematisch als TCS-orientiert?
MS Dousti
Deshalb habe ich gesagt "tangential" verwandt. Farbprobleme sind TCS-orientiert, nur nicht dieses spezielle.
Derrick Stolee
4
α
Ausgezeichnet. Validierung.
Derrick Stolee
5

Ein Teil der Arbeit von Olivier Finkel scheint mit der Frage zu tun zu haben - wenn auch nicht unbedingt explizit mit dem Axiom of Choice selbst - und mit der Antwort von Timothy Chow. Zum Beispiel unter Bezugnahme auf die Zusammenfassung von Unvollständigkeitssätzen, großen Kardinälen und Automaten über endlichen Wörtern , TAMC 2017 ,

Tn:=ZFC+``There exist (at least) n inaccessible cardinals''n0
Sylvain
quelle
3

[Dies ist keine direkte Antwort auf Ihre Frage, dennoch kann es für manche Menschen suggestiv und / oder informativ sein.]

Die P vs. NP-Umfrage von William Gasarch liefert einige Statistiken darüber, "wie P vs. NP gelöst wird":

  1. 61 dachte P ≠ NP.
  2. 9 dachte P = NP.
  3. 4 dachte, dass es unabhängig ist . Obwohl kein bestimmtes Axiomensystem erwähnt wurde, gehe ich davon aus, dass es von ZFC unabhängig ist .
  4. 3 hat gerade angegeben, dass es NICHT unabhängig von der primitiven rekursiven Arithmetik ist.
  5. Ich sagte, es würde vom Modell abhängen.
  6. 22 gaben keine Meinung ab.

Wikipedia hat eine interessante Sicht auf die Unabhängigkeit:

... Diese Barrieren haben auch einige Informatiker dazu veranlasst, anzunehmen, dass das P-gegen-NP-Problem möglicherweise unabhängig von Standard-Axiomensystemen wie ZFC ist (kann darin nicht bewiesen oder widerlegt werden). Die Interpretation eines Unabhängigkeitsergebnisses könnte sein, dass entweder kein Polynomzeitalgorithmus für ein NP-vollständiges Problem existiert und ein solcher Beweis nicht in (z. B.) ZFC konstruiert werden kann, oder dass Polynomzeitalgorithmen für NP-vollständige Probleme existieren könnten. In ZFC ist es jedoch unmöglich zu beweisen, dass solche Algorithmen korrekt sind [ 1]. Wenn jedoch gezeigt werden kann, dass mit Techniken der derzeit als anwendbar bekannten Art das Problem auch mit viel schwächeren Annahmen, die die Peano-Axiome (PA) für Ganzzahlarithmetik erweitern, nicht entschieden werden kann, dann würde es notwendigerweise beinahe Polynom-Zeit-Algorithmen für jedes Problem in NP [ 2 ]. Wenn man daher glaubt (wie die meisten Komplexitätstheoretiker), dass nicht alle Probleme in NP effiziente Algorithmen haben, würde dies bedeuten, dass Beweise für die Unabhängigkeit unter Verwendung dieser Techniken nicht möglich sind. Darüber hinaus impliziert dieses Ergebnis, dass der Nachweis der Unabhängigkeit von PA oder ZFC mit derzeit bekannten Techniken nicht einfacher ist als der Nachweis der Existenz effizienter Algorithmen für alle Probleme in NP.

MS Dousti
quelle
5
Eine weitere interessante Tatsache (auch aus Wikipedia) ist, dass die wichtigste (einzige?) Allgemeine Methode zum Nachweis der Unabhängigkeit in ZFC, die erzwingt, nicht beweisen kann, dass P =? NP unabhängig von ZFC ist. Dies ist eine Folgerung aus Shoenfields Absolutheitssatz.
Travis Service
Beachten Sie, dass Bill an einer weiteren Umfrage teilnimmt
Charles,
@Charles: Danke für das Update. Ich bin sehr gespannt auf den jüngsten Konsens der Community.
MS Dousti
2

ZF

Gχ(H)HGG

ZF

Stella Biderman
quelle
Nettes Beispiel. Ich denke, Timothy Chow hat diese Art von Beispiel in dem Absatz über die chromatische Nummer des Flugzeugs angesprochen.
Sasho Nikolov
@SashoNikolov Die Färbbarkeit von Grafiken ist meines Erachtens eindeutig ein TCS-Problem, auch wenn die Grafiken unendlich sind. Das Hadwiger-Nelson-Problem ist im Bereich TCS viel weniger offensichtlich, wie die Kommentatoren hervorhoben und das OP dieser Antwort zustimmte. Im Gegensatz dazu denke ich, dass es niemanden gibt, der sich diesen Satz ansieht und sagt: "Das ist kein wirkliches CS-Problem."
Stella Biderman
Ich sehe den Unterschied überhaupt nicht: Hadwiger-Nelson geht es auch darum, ein unendliches geometrisches Diagramm zu färben. Auf jeden Fall mag ich beide Beispiele und habe sie hochgestuft, und ich denke, es ist sinnlos zu versuchen, eine zu feine Unterscheidung zwischen TCS und anderen Bereichen der Mathematik zu treffen.
Sasho Nikolov