Aksjomaty niezbędne w informatyce teoretycznej

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?

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 ).$RCA_0$$\mathbf{P} vs. \mathbf{NP}$$PA_1$$PA_1$$PA$

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 .$P \not= NP$$PA_1$$DTIME(n^{\log^{*}(n)})$$PA$$PA_1$

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.$\sigma$$X$$X$

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