W dniu wtorek, 27 września 2016 09:04:18 UTC+2 użytkownik bartekltg napisał:
> On 27.09.2016 02:22, M.M. wrote:
> > Nie zgadzamy się, bo problem stopu na MT jest rozstrzygalny.
[...]
> Jakby nie patrzeć, z każdej strony dupa.
> A formalniej, istnienie takiej uniwersalnej procedury
> prowadzi do paradoksu (fałszu). A wiec któreś z założeń
> jest nieprawdziwe. Nie założyliśmy za wiele, więc albo
> matematyka się wali, albo załozenie, że procedura stop
> istenije, jest fałszywe.

Tym niemniej, konstrukcja, którą przedstawił M.M. (która w istocie
nie dotyczy problemu stopu), wydaje się analogiczna do teorii typów,
będącej jedną z propozycji rozwiązania Paradoksu Russella
(o strukturze analogicznej do problemu stopu).

Wydaje się, że tym, czego w istocie dowodzi przedstawiony przez
Ciebie argument, jest to, że logika dwuwartościowa nie jest
dość bogata do wyrażania naszych intuicji dotyczących programów
komputerowych -- bo przecież my jako ludzie nie mamy problemu
ze zrozumieniem źródła sprzeczności w tym dowodzie. Mianowicie
dowód ten mówi nam, że pewne programy, które mają explicite
rozstrzygać o swoich własnych właściwościach, mogą być kłopotliwe
w analize. (Oczywiście będą również takie, które bez problemu
rozstrzygają o pewnych swoich właściwościach)

Oczywiście temat jest bardzo słynny i szeroko dyskutowany,
ale rodzi następujące pytania (gdyby ktoś znał albo umiał
wymyślić na nie odpowiedzi, prosiłbym o ich tu przedstawienie):
- czy jeżeli zawęzimy problem stopu tylko do programów, które
nie odnoszą się do samych siebie, to czy wówczas staje
się rozstrzygalny? czy może też istnieje jakiś argument,
w którym nie używa się samoodnośnych programów, a z którego
również wynika nierozwiązywalność problemu stopu?

- czy istnieje jakaś systematyczna procedura rozpoznawania
programów, które będą popadały w ów paradoks zatrzymywalności?