Maszyny Turinga, których zakończenie jest niemożliwe do udowodnienia?

Mam naiwne pytanie: czy istnieje maszyna Turinga, której zakończenie jest prawdziwe, ale której nie da się udowodnić żadną naturalną, spójną i skończoną aksjomatyczną teorią? Proszę o zwykły dowód istnienia, a nie o konkretny przykład.

Może to mieć związek z analizą porządkową . Rzeczywiście, dla maszyny Turinga możemy zdefiniować jako najmniejszy porządek spójnej teorii dowodzącej jej zakończenia (lub minimum tych rzędnych). Sądzę więc, że równoważne byłoby pytanie, czy istnieje takie , że ? $M$ $O(M)$ $M$ $O(M) \geq \omega_1^{CK}$

turing-machines proof-theory halting-problem

— Super8
źródło

Czy kwantyfikacja nie powinna działać na odwrót? Po prostu dodanie w zatrzymaniu TM X jako aksjomat byłoby spójne dla każdego X, który faktycznie zatrzymuje się na wszystkich wejściach (i skończony, jeśli zrobisz to tylko dla danej TM). Przy odwróconych kwantyfikatorach, co powiesz na TM, która zatrzymuje się, jeśli dane wejściowe nie są dowodem zgodności dla systemu aksjomatycznego i w przeciwnym razie wchodzą w nieskończoną pętlę.

— Yonatan N

Twoja sugestia jest interesująca, dzięki. Byłem świadomy waszej troski przy formułowaniu pytania, dlatego dodałem „naturalny” do wymagań. Oczywiście problemem jest to, czy możemy podać formalną definicję „naturalności”, która wykluczałaby tę sztuczną konstrukcję.

— Super8

myślę, że odpowiedź brzmi „nie”, ponieważ jeśli się zatrzyma, to wystarczy uruchomić maszynę i zatrzyma się ona w skończonej liczbie kroków, i to jest dowód, a fakt ten można przekształcić w dowolny dość wydajny system dowodu. z drugiej strony myślę, że można zakodować / przekonwertować / przetłumaczyć thm godla Boskiego na nieusuwalną maszynę, dla której nie można tego udowodnić. to pytanie jest podobne, czy istnieje baza TM, która zatrzymuje się na wszystkich danych wejściowych, ale właściwość nie jest możliwa do udowodnienia cs.se

— od

Możesz zbudować maszynę Turinga która oblicza sekwencję Goodsteina wejścia i zatrzymuje się, gdy osiągnie Nie można udowodnić zatrzymania w arytmetyce Peano; tzn. Twierdzenie Goodsteina nie jest możliwe do udowodnienia przy użyciu arytmetyki Peano. Zobacz Laurie Kirby, Jeff Paris, Dostępne wyniki niezależności dla arytmetyki Peano (1982)

M

$M$

G (n)

$G(n)$

n

$n$

0

$0$

M

$M$

— Marzio De Biasi

Dzięki, nie znałem tych wpisów. To, o co proszę, jest silniejsze, chciałbym, aby nie można było udowodnić jakiejkolwiek rozsądnej teorii (a nie konkretnej teorii, takiej jak PA). Nie jestem jednak pewien, czy pytanie ma jednoznaczną odpowiedź.

— Super8

Odpowiedzi:

Zakończenie maszyny Turinga (na stałym wejściu) to $\Sigma^0_1$ zdanie i wszystkie zwykłe teorie arytmetyczne pierwszego rzędu są kompletne $\Sigma^0_1$ zdania, tj. wszystkie prawdziwe $\Sigma^0_1$ twierdzenia te można udowodnić w tych teoriach.

Jeśli spojrzysz na całość zamiast na zatrzymanie , tj. TM zatrzymuje się na wszystkich wejściach, to jest to $\Pi^0_2$ -kompletne zdanie i dla każdej możliwej do obliczenia aksjomatycznej spójnej teorii, która jest wystarczająco silna (np. przedłuża, powiedzmy Robinsona $Q$ teoria) istnieje TM, której całości nie można udowodnić w tej teorii.

— Kaveh
źródło

Tak, szukałem całości, ponieważ oczywiście problem jest trywialny dla stałego wkładu. Zastanowię się nad twoim twierdzeniem i jak je udowodnić, ale w tym momencie nie rozumiem, w jaki sposób rozważanie teorii „możliwej do aksjomatyzacji” wyklucza wspomniany problem? Także w twoim stwierdzeniu TM zależy od rozważanej teorii, czy możemy uzyskać moje mocniejsze stwierdzenie poprzez jakąś diagonalizację?

— Super8

Oto prosty sposób: zestawem możliwych do udowodnienia całkowitych funkcji obliczeniowych takiej teorii jest ce, zestawem całkowitych funkcji obliczalnych nie jest ce, lub alternatywnie można przekątnie w stosunku do możliwych do udowodnienia całkowitych funkcji teorii.

— Kaveh

Po zastanowieniu proponuję rozważyć ograniczenie problemu w następujący sposób. Biorąc pod uwagę porządek notacji

σ

$\sigma$ reprezentujący porządek

α

$\alpha$ możemy zdefiniować odpowiednią „teorię elementarną”

T (α, σ)

$\mathcal{T}(\alpha,\sigma)$ która pozwala na indukcję transfinitową do

α

$\alpha$ . Biorąc pod uwagę TM

M

$M$ , zdefiniowalibyśmy wtedy

O (M)

$O(M)$ jako najmniejszy porządek

α

$\alpha$ tak, że zakończenie

M

$M$ można udowodnić teorią

T (α, σ)

$\mathcal{T}(\alpha,\sigma)$ (tzn. system notacji można dowolnie wybierać). Czy ta definicja ma sens?

— Super8

@ Super8, nie jestem pewien. Zasadniczo powiązanie porządków z teoriami nie jest kanoniczne, istnieją różne sposoby na powiązanie tego celu. Możesz zacząć od słabej teorii, takiej jak PRA, i dodać indukcję w stosunku do rzędnych obliczalnych z ładnymi podstawowymi sekwencjami itp., Ale nie jestem pewien, dlaczego chcesz to zrobić.

— Kaveh

Ok, nie zdawałem sobie sprawy z problemu, wtedy sam spróbuję znaleźć lepszą definicję.

— Super8

Nie jestem ekspertem od logiki, ale wierzę, że odpowiedź brzmi „ nie” . Jeśli maszyna Turinga zatrzyma się, a system jest wystarczająco silny, powinieneś być w stanie zapisać pełną historię obliczeń maszyny Turinga na jej wejściu. Kiedy weryfikuje się, że wynikiem obliczeń jest kończąca sekwencja przejść, można zauważyć, że maszyna zatrzymuje się. Niezależnie od tego, jak sformalizujesz maszyny Turinga w swojej teorii, powinieneś być w stanie wykazać w każdej rozsądnej teorii, że maszyna, która się zatrzymuje, faktycznie zatrzymuje się. Analogicznie pomyśl o próbie udowodnienia, że skończona suma jest równa temu, co jest równa; np. udowodnij, że 5 + 2 + 3 + 19 + 7 + 6 = 42 lub 5 + 5 + 5 = 15. Tak jak zawsze jest to możliwe, o ile liczba kroków jest skończona, tak samo udowadnia wynik obliczeń skończonych.

Jako dodatkowy oczywisty punkt - nawet jeśli twoja teoria jest niespójna, nadal możesz pokazać, że maszyna zatrzymuje się, nawet jeśli tak nie jest, ponieważ możesz udowodnić wff w niespójnej teorii, niezależnie od tego, czy jest właściwie prawda.

— Philip White
źródło

Zgadzam się z twoim pierwszym punktem, zobacz moją odpowiedź poniżej. Jeśli chodzi o twój drugi punkt, niespójna teoria również udowodni zakończenie (faktycznie nieterminacyjnej) TM, skąd ograniczenie do spójnych teorii.

— Super8

Myślę, że mówimy to samo; Właśnie zauważyłem, że powiedziałeś „konsekwentnie” w pytaniu, przepraszam, że tego nie zauważyłem. Myślę, że odpowiedź Kaveha obejmuje te same rzeczy i jest bardziej elegancko napisana.

— Philip White