Konstruktywna wersja rozstrzygalności?

Dzisiaj podczas lunchu poruszyłem ten problem z kolegami i ku mojemu zdziwieniu argument Jeffa E., że problem jest rozstrzygalny, nie przekonał ich ( oto ściśle powiązany post na temat przepływu matematyki). Stwierdzenie problemu, które jest łatwiejsze do wyjaśnienia („czy P = NP?”) Jest również rozstrzygalne: albo tak, albo nie, a więc jedna z dwóch baz TM, które zawsze wysyłają te odpowiedzi, decyduje o problemie. Formalnie możemy zdecydować o zestawie : albo maszyna, która wyprowadza tylko dla wejścia a inaczej decyduje o tym, lub maszyna, która robi to dla wejścia .$S :=\{|\{P, NP\}|\}$$1$$1$$0$$2$

Jeden z nich sprowadził się do tego zarzutu: jeśli tak słabe jest kryterium rozstrzygalności - co oznacza, że ​​każde pytanie, które możemy sformalizować jako język, który możemy pokazać jako skończony, jest rozstrzygalne - wówczas powinniśmy sformalizować kryterium, które nie czyni żadnego problemu z skończoną liczbą możliwych odpowiedzi, które można sformalizować w ten sposób rozstrzygalne. Chociaż poniższe kryterium jest prawdopodobnie silniejszym kryterium, zasugerowałem, że być może można to sprecyzować, wymagając, aby rozstrzygalność powinna zależeć od możliwości wykazania TM, zasadniczo proponując intuicyjny pogląd na tę sprawę (do którego nie skłaniam się - ani czy którykolwiek z moich kolegów, wszyscy akceptują prawo wykluczonego środka).

Czy ludzie sformalizowali i prawdopodobnie przestudiowali konstruktywną teorię rozstrzygalności?

Myślę, że pytanie, które próbujesz zadać, brzmi „czy teoria obliczalności jest konstruktywna?”. To interesujące pytanie, jak można zobaczyć w tej dyskusji na liście mailingowej Podstawy matematyki.

Nie jest zaskoczeniem, że zostało to wzięte pod uwagę, ponieważ wiele teorii rekurencji zostało opracowanych przez ludzi o konstruktywnej wrażliwości i odwrotnie. Patrz np . Książka Bessona i czcigodny wstęp do metamatematyki . Jest całkiem jasne, że pierwsze kilka rozdziałów teorii rekurencji przetrwało, przechodząc do konstruktywnego otoczenia z minimalnymi zmianami: np. Twierdzenie snm, twierdzenie Rice'a lub twierdzenie rekurencyjne Kleene'a przetrwały bez zmian.

Jednak po pierwszych rozdziałach sprawy stają się nieco trudniejsze. W szczególności wyższe poziomy hierarchii arytmetycznej są zwykle definiowane przez pojęcie prawdy. W szczególności powszechnie stosowane twierdzenia, takie jak twierdzenie o niskiej podstawie, wydają się wyraźnie niekonstruktywne.

Być może jednak bardziej pragmatyczną odpowiedzią jest to, że te „paradoksalnie obliczalne języki” są po prostu cechą charakterystyczną, którą można (i trzeba było!) Badać na wielką skalę, podobnie jak nie mierzalne zestawy rzeczywistości, ale gdy początkowa niespodzianka była przezwyciężyć, można przejść do bardziej interesujących rzeczy.

W klasycznej logice każde stwierdzenie jest prawdziwe lub fałszywe w danym modelu. Na przykład każde stwierdzenie pierwszego rzędu dotyczące liczb naturalnych jest albo prawdziwe, albo fałszywe w „świecie rzeczywistym” (znanym w tym kontekście jako prawdziwa arytmetyka ). Co zatem z twierdzeniem o niekompletności Gödela? Stwierdza jedynie, że żadna rekurencyjnie wyliczalna aksjatyzacja prawdziwej arytmetyki nie jest kompletna.

Jeśli chodzi o vs. , większość badaczy uważa, że , niektórzy że , a garstka zabawia przekonanie, że jest niezależny (powiedzmy) ZFC. Załóżmy, że jesteś skłonny przyznać, że tak naprawdę nie jest niezależny od ZFC (w ten sam sposób, w jaki przyznajesz, że ZFC jest spójny w pierwszej kolejności). W takim przypadku istnieje całkowicie jawna maszyna Turinga, która oblicza Twój język. Maszyna szuka dowodu lub dopóki nie zostanie znaleziony, a następnie kontynuuje odpowiednio. Możemy to udowodnić$\mathsf{P}$$\mathsf{NP}$$\mathsf{P} \neq \mathsf{NP}$$\mathsf{P} = \mathsf{NP}$$\mathsf{P} = \mathsf{NP}$$\mathsf{P} \neq \mathsf{NP}$ że ta maszyna akceptuje twój język, nawet jeśli nadal nie wiemy, co to za język!

Jeśli nie chcesz przyznać, że o decyduje ZFC, możesz nadal zapytać, czy istnieje jawna maszyna Turinga, która akceptuje twój język. To zadziwiające pytanie pozostawiam zainteresowanemu czytelnikowi.$\mathsf{P} \stackrel{?}{=} \mathsf{NP}$

(wyłączenie odpowiedzialności, rozmyta odpowiedź na rozmyte pytanie, które może lepiej pasować do cstheory ). Konstruktywność to „wielka sprawa” w matematyce teoretycznej, ale ujawnia się zwłaszcza w ciągłych kontekstach, takich jak półfamiczny paradoks Banacha-Tarskiego . wydaje się, że paradoksy te jak dotąd nie pojawiły się w „bardziej dyskretnych” CS . więc czym jest (analogowa / równoległa) konstruowalność w CS? odpowiedź wydaje się nie tak jasna. jest to koncepcja wywodząca się z badań matematycznych bardziej niż CS, a te dwie wydają się zbyt mocno powiązane z tym szczególnym tematem zbyt „jak dotąd” .

jedną z odpowiedzi jest to, że teoria rozstrzygalności wydaje się być odmianą konstruowalności, tj. jest to ścisła metoda określania, które zbiory są obliczalne, a które wydają się być ściśle powiązane.

Konstruktywność w sercu zajmuje się pewnymi kwestiami „niezależności od ZFC”, a te obszary są szczegółowo omówione w tym artykule przez Aaronsona wr P i NP, czy P i NP jest formalnie niezależny? .

tak naprawdę nie wykazano, że „paradoksy” wydają się wskazywać na problemy z konstruktywnością, ale można to potraktować jako przybliżony przewodnik dla przybliżonej analogii, jak w pracy Aaronsona, w której rozważa np. wyniki wyroczni, które wydają się mieć pewien „paradoksalny” smak, w szczególności Baker skrzeli Solovay 1975 wyników, przepowiedni istnieją zarówno takie, że P = nP i P ^B ≠ nP ^B . inne paradoksalne, jak thms, to twierdzenia o luce Blum i przyspieszeniu .

czy to tylko zbieg okoliczności, że CS koncentruje się na funkcjach konstrukcyjnych „czas / przestrzeń” w swoich podstawowych twierdzeniach dotyczących hierarchii czasu / przestrzeni? (które następnie wykluczają paradoksy podobne do Bluma prawie „z założenia” ?)

inną odpowiedzią jest to, że jest to przedmiotem aktywnych badań / badań, np. jak w tym odkryciu. Konstruktywność jest powiązana z „dużymi kardynałami” z matematyki: strategie wygrywające w nieskończonych grach: od dużych kardynałów do informatyki / Ressayre.

Posługując się dużym kardynalnym aksjomatem „ostrych” Martin udowodnił analityczną determinację: istnienie zwycięskiej strategii dla jednego z graczy w każdej nieskończonej grze doskonałej informacji między dwoma graczami, pod warunkiem, że zwycięski zestaw jednego z graczy okazał się analityczny jeden. Modyfikuję i uzupełniam jego dowód, aby uzyskać nowy dowód twierdzenia Rabina, Buechi-Landwebera, Gurewicza-Harringtona o determinacji stanu skończonego: istnienie strategii wygranej obliczonej przez maszynę skończonego stanu, gdy zwycięskie sety gracza są skończone stan zaakceptowany.