Aksjomaty niezbędne w informatyce teoretycznej

37

To pytanie jest inspirowane podobnym pytaniem o matematykę stosowaną w matematycznym przepływie i ta dokuczliwa myśl, że ważne pytania TCS, takie jak P vs. NP, mogą być niezależne od ZFC (lub innych systemów). Jako małe tło, matematyka odwrotna to projekt znalezienia aksjomatów niezbędnych do udowodnienia pewnych ważnych twierdzeń. Innymi słowy, zaczynamy od zestawu twierdzeń, które, jak się spodziewamy, są prawdziwe, i staramy się uzyskać minimalny zbiór „naturalnych” aksjomatów, które je czynią.

Zastanawiałem się, czy matematyka odwrotna została zastosowana do jakichkolwiek ważnych twierdzeń TCS. W szczególności teoria złożoności. Przy impasie wielu otwartych pytań w TCS wydaje się naturalne pytanie „jakich aksjomatów nie próbowaliśmy użyć?”. Alternatywnie, czy jakieś ważne pytania w TCS okazały się niezależne od pewnych prostych podsystemów arytmetyki drugiego rzędu?

Artem Kaznatcheev
źródło
Dwa możliwe aksjomaty, które mogą nie być niezależne: 1) 3-SAT wymaga czasu. 2) Biorąc pod uwagę zadowalającą formułę 3SAT, każdy wydajny algorytm spełnia najwyżej -frakcji klauzul. Również mnożenie dwóch liczb pierwszych równych rozmiarów jest trudne do odwrócenia (skutecznie). 2Ω(n)7/8
Mohammad Al-Turkistany
Niniejszy artykuł jest istotny: Harry Buhrman, Lance Fortnow, Leen Torenvliet, „Sześć hipotez w poszukiwaniu twierdzenia”, CCC, s. 2, 12. doroczna konferencja IEEE na temat złożoności obliczeniowej (CCC'97), 1997
Mohammad Al-Turkistany
6
Powiązane jest następujące pytanie: cstheory.stackexchange.com/questions/1923/... Większość TCS można sformalizować w RCA_0. Twierdzenie o mniejszym wykresie jest rzadkim wyjątkiem. Jak podkreśla Neel, jeśli chcesz nowych pomysłów, szukaj nowych pomysłów; nie szukaj nowych aksjomatów. Oba nie są wcale takie same.
Timothy Chow
1
Jestem zdezorientowany, dlaczego podano wyniki takie jak stwierdzenia lub . W moim pierwszym wykładzie TCS zaczęliśmy od liczb naturalnych i niektórych podstawowych funkcji na nich. Reszta następuje. Najwyraźniej nie rozumiem pytania. PNP
Raphael
1
Właśnie to zauważyłem, ale najwyraźniej Lipton zadał podobne pytanie w tym poście: rjlipton.wordpress.com/2011/02/03/... , aby zacytować: „Zastanawiam się, czy istnieją techniki dowodowe, które obejmują pomysły wykraczające daleko poza PA, które mamy nieużywane, a które pomogłyby rozwiązać niektóre ważne problemy. Czy powinniśmy uczyć naszych absolwentów metod z dziedzin matematyki, które leżą poza nauką komputerową? ” (PA = arytmetyka Peano)
Artem Kaznatcheev

Odpowiedzi:

23

Tak, temat został zbadany pod kątem złożoności dowodu. Nazywa się to Bounded Reverse Mathematics . Tabelę zawierającą niektóre wyniki matematyki odwrotnej można znaleźć na stronie 8 książki Cooka i Nguyena „ Logical Foundations of Proof Complexity ”, 2010. Niektórzy z poprzednich uczniów Steve'a Cooka pracowali nad podobnymi tematami, np. Tezy Nguyena, „ Bounded Reverse Mathematics ” , University of Toronto, 2008.

Alexander Razborov (także inni teoretycy złożoności dowodów) ma pewne wyniki dotyczące słabych teorii potrzebnych do sformalizowania technik złożoności obwodów i udowodnienia niższych granic złożoności obwodów. Uzyskuje pewne wyniki nie do udowodnienia dla słabych teorii, ale teorie są uważane za zbyt słabe.

Wszystkie te wyniki można udowodnić w (podstawowa teoria Simpsona dla matematyki odwrotnej), więc AFAIK nie mamy niezależności wynikającej z silnych teorii (i w rzeczywistości takie wyniki niezależności miałyby poważne konsekwencje, jak wspomniała Neel, patrz praca Ben-David (i powiązane wyniki) w sprawie niezależności od gdzie jest rozszerzeniem ).RCA0Pvs.NPPA1PA1PA

Kaveh
źródło
Takie wyniki w zakresie niezależności byłyby znaczącymi przełomami, ale nie sądzę, aby miały one natychmiastowe poważne konsekwencje; zobacz mój komentarz do odpowiedzi Neela.
Timothy Chow,
@ Czas, dzięki, masz rację, naprawiłem moją odpowiedź. To nie jest , to , rozszerzone o wszystkie prawdziwe uniwersalne zdania arytmetyki, a Ben-David twierdzi, że jeśli pytanie jest niezależne od tej silniejszej teorii, wówczas SAT ma prawie wielomianowy algorytm czasu. Zatem założenie jest (znacznie) silniejsze, ale ostateczne twierdzenie jest takie samo. (i obecnie znane metody dowodzenia niezależności od oznaczałyby także niezależność od ).PAPA1PAPAPA1
Kaveh
21

Jako pozytywną odpowiedź na ostatnie pytanie, dowody normalizacji polimorficznych rachunków lambda, takich jak rachunek konstrukcji, wymagają arytmetyki co najmniej wyższego rzędu, a mocniejsze układy (takie jak rachunek konstrukcji indukcyjnych) są zgodne z ZFC i niezliczoną liczbą niedostępnych.

Jako odpowiedź przeczącą na ostatnie pytanie, Ben-David i Halevi wykazali, że jeśli jest niezależny od , arytmetyka Peano jest rozszerzona o aksjomaty dla wszystkich uniwersalnych prawd arytmetycznych, wówczas istnieje prawie algorytm wielomianowy dla SAT. Ponadto, obecnie nie ma znanych sposobów generowania zdań, które są niezależne od ale nie .PNPPA1DTIME(nlog(n))PAPA1

Mówiąc bardziej filozoficznie, nie popełniaj błędu, utożsamiając siłę spójności z siłą abstrakcji.

Prawidłowy sposób zorganizowania tematu może obejmować najwyraźniej dzikie zasady teorii zbiorów, nawet jeśli nie są one absolutnie konieczne pod względem siły spójności. Na przykład zasady silnego zbierania są bardzo przydatne do określania właściwości jednorodności - np. Teoretycy kategorii ostatecznie chcą słabych, dużych kardynalnych aksjomatów do manipulowania takimi rzeczami, jak kategoria wszystkich grup, tak jakby były obiektami. Najbardziej znanym przykładem jest geometria algebraiczna, której rozwój w szerokim zakresie wykorzystuje wszechświaty Grothendiecka, ale wszystkie z nich (takie jak ostatnie twierdzenie Fermata) najwyraźniej mieszczą się w arytmetyki trzeciego rzędu. Jako o wiele bardziej trywialny przykład zauważ, że ogólne operacje tożsamości i kompozycji nie są funkcjami, ponieważ są indeksowane w całym wszechświecie zbiorów.

Z drugiej strony czasem związek między siłą konsystencji a abstrakcyjnością idzie w przeciwnym kierunku. Rozważ związek między środkami a środkami motywacyjnymi. Środki zostały zdefiniowane na rodziny podzbiorów ( -algebras) na zbiorze , natomiast środki motywiczną są określone bezpośrednio na wzorach interpretowane . Tak więc, chociaż miara motywacyjna uogólnia miarę, złożoność teorii zbiorów maleje , ponieważ jedno użycie zestawu mocy zanika.σXX

EDYCJA: System logiczny A ma większą siłę konsystencji niż system B, jeśli spójność A implikuje spójność B. Na przykład, ZFC ma większą siłę konsystencji niż arytmetyka Peano, ponieważ można udowodnić spójność PA w ZFC. A i B mają tę samą siłę konsystencji, jeśli są równomierne. Na przykład arytmetyka Peano jest spójna wtedy i tylko wtedy, gdy arytmetyka Heyting (konstruktywna) jest.

IMO, jednym z najbardziej zadziwiających faktów na temat logiki jest to, że siła spójności sprowadza się do pytania „jaką najszybciej rozwijającą się funkcję można udowodnić w tej logice?” W rezultacie spójność wielu klas logiki można uporządkować liniowo! Jeśli masz zwykłą notację, która jest w stanie opisać najszybciej rozwijające się funkcje, twoje dwie logiki mogą pokazać całkowitą liczbę, to przez trichotomię wiesz, że jedna z nich może udowodnić spójność drugiej, lub są one jednakowo spójne.

Ale ten zadziwiający fakt powoduje również, że siła spójności nie jest właściwym narzędziem do mówienia o abstrakcjach matematycznych. Jest niezmiennikiem systemu zawierającego sztuczki kodujące, a dobra abstrakcja pozwala wyrazić pomysł bez sztuczek. Jednak nie wiemy wystarczająco dużo o logice, aby formalnie wyrazić ten pomysł.

Neel Krishnaswami
źródło
7
czym jest „siła konsystencji”?
Suresh Venkat
7
Tego nie udowodnili Ben-David i Halevi. Przeoczyłeś ich kluczowego jeźdźca „wykorzystującego obecnie dostępne techniki”. Interpretuję ich artykuł jako podkreślenie, jak słabe są nasze obecne techniki dowodowe, a nie jako mówienie dużo o pytaniu P = NP.
Timothy Chow,