Problem zatrzymania, niepoliczalne zbiory: wspólny dowód matematyczny?

Wiadomo, że z policzalnym zestawem algorytmów (charakteryzujących się liczbą Gödla) nie możemy obliczyć (zbudować algorytmu binarnego, który sprawdza przynależność) wszystkich podzbiorów N.

Dowód można podsumować w następujący sposób: jeśli moglibyśmy, to zestaw wszystkich podzbiorów N byłby policzalny (moglibyśmy powiązać z każdym podzbiorem liczbę Gödla algorytmu, który go oblicza). Ponieważ jest to fałsz, potwierdza to wynik.

Jest to dowód, który mi się podoba, ponieważ pokazuje, że problem jest równoważny podzbiorom N, których nie można policzyć.

Teraz chciałbym udowodnić, że problemu zatrzymania nie da się rozwiązać przy użyciu tylko tego samego wyniku (niepoliczalność N podzbiorów), ponieważ myślę, że są to bardzo bliski problem. Czy można to udowodnić w ten sposób?

computability halting-problem

— Weier
źródło

Oczywiście oba wyniki można udowodnić za pomocą tej samej techniki (diagonalizacji). Nie sądzę jednak, aby można było udowodnić nierozstrzygalność problemu zatrzymania, używając po prostu niepoliczalności rodziny podzbiorów ℕ, ponieważ pierwsza dotyczy porównania RE i R , z których obie są policzalnymi rodzinami podzbiory ℕ.

— Tsuyoshi Ito,

Istnieje tylko niezliczona ilość programów z dostępem do wyroczni zatrzymującej, znowu charakteryzującej się liczbą Godla. Jednak problem zatrzymania JEST wśród tego policzalnego zestawu.

— David Harris

Twierdzenie o zatrzymaniu, twierdzenie Cantora (nieizomorfizm zbioru i jego zestawu sił) oraz twierdzenie o niekompletności Goedela to wszystkie przypadki twierdzenia Lawpowa o stałym punkcie, który mówi, że dla dowolnej zamkniętej kartezjańskiej kategorii, jeśli istnieje mapa epimorficzna a następnie każdy ma ustalony punkt. $e : A \to (A \Rightarrow B)$ $f : B \to B$

Lawvere, F. William. Argumenty przekątne i kartezjańskie kategorie zamknięte . Wykład notatki w matematyce, 92 (1969), 134-145.

Miłe wprowadzenie do tych pomysłów można znaleźć w tym poście na blogu Andreja Bauera .

— Neel Krishnaswami
źródło

to całkiem miłe. Nie zdawałem sobie sprawy, że istniał rzeczywisty formalny argument jednoczący ich.

— Suresh Venkat,

Nauczyłem się już podejrzewać, że jeśli wygląda tak samo i pachnie tak samo, istnieje kategoryczny spór o sens, w jakim jest taki sam.

— Vijay D

IMO, dwie naprawdę fajne rzeczy w twierdzeniu Lawvere'a jest to, że (a) jest to twierdzenie dodatnie, a nie ujemne, i (b) dowodem jest pół tuzina linii prostych obliczeń rachunku lambda.

— Neel Krishnaswami,

Czytając to pytanie, pomyślałem sobie, że ktoś powinien wspomnieć o twierdzeniu Lawvere'a o punkcie stałym. Wyobraź sobie moją radość, gdy czytam odpowiedź :-)

— Andrej Bauer,

Epimorficzna nie jest właściwym warunkiem. Potrzebujesz punktowotliwości, która nie implikuje ani nie implikuje warunku bycia epimorficznym. Zobacz uwagę 2.3 ncatlab.org/nlab/show/Lawvere%27s+fixed+point+theorem

— fhyve