Obliczeniowe konsekwencje twierdzenia Friedmana (nie do udowodnienia) na temat przesunięcia górnego o stałym punkcie?

Harvey Friedman wykazał, że istnieje dokładny wynik punktu stałego, którego nie można udowodnić w ZFC (zwykła teoria mnogości Zermelo-Frankela z Axiom of Choice). Wiele współczesnych układów logicznych opiera się na operatorach stałoprzecinkowych, więc zastanawiałem się: czy są znane konsekwencje twierdzenia o przesunięciu górnego przesunięcia dla teoretycznej informatyki?

Nie do udowodnienia Twierdzenie o stałym punkcie przesunięcia górnego
Dla wszystkich $R \in \text{SDOI}(Q^k,Q^k)$ część $A = \text{cube}(A,0) \setminus R[A]$ zawiera $\text{us}(A)$ .

Twierdzenie USFP wydaje się być twierdzeniem $\Pi^1_1$ , więc może być „wystarczająco blisko” do obliczalności (np. Sprawdzanie nieizomorfizmu struktur automatycznych), aby wpłynąć na teoretyczną informatykę.

Aby uzyskać kompletność, oto definicje z przemówienia Friedmana na MIT z listopada 2009 r. (Patrz także szkic książki „Teoria relacji logicznych” ).

$Q$ jest zbiorem liczb wymiernych. $x, y \in Q^k$ sąrównoważne porządkom,jeśli ilekroć$1 \le i,j \le k$ to$x_i \lt x_j \Leftrightarrow y_i \lt y_j$ . Gdy$x \in Q^k$ wówczasgórny przesuwnyz$x$ , oznaczonej$\text{us}(x)$ , otrzymuje się przez dodanie 1 do każdego nieujemne współrzędnej$x$ . Relacja$A \subseteq Q^k$ jestkolejność niezmienna, jeśli dla każdego rzęduniezmiennego równoważnej $x,y \in Q^k$ jest warunek$x \in A \Leftrightarrow y \in A$ . Relacja$R \subseteq Q^k \times Q^k$ jest niezmiennikiem porządku, jeśli$R$ jest niezmiennikiem porządku jako podzbiorem$Q^{2k}$ , iściśle dominuje,jeśli dla wszystkich$x,y \in Q^k$ za każdym razem, gdy$R(x,y)$A Q k R [ A ] { y | ∃ x ∈ A R ( x , y ) } A us ( A ) = { us ( x ) | x ∈ A } sześcian ( A , 0 ) B k 0 ∈ B A B $\max(x) \lt \max(y)$$A$$Q^k$$R[A]$$\{ y | \exists x \in A R(x,y)\}$$A$$\text{us}(A) = \{\text{us}(x) | x \in A\}$$\text{cube}(A,0)$$B^k$$0 \in B$$A$$B^k$R ⊆ Q k × Q $\text{SDOI}(Q^k,Q^k)$$R \subseteq Q^k \times Q^k$

Edycja: Jak zauważył Dömötör Pálvölgyi w komentarzach, przyjmowanie i jako zwykłej kolejności racjonalnej wydaje się dawać kontrprzykład. Po pierwsze, zestaw nie może być pusty, ponieważ jest wówczas również pusty, a musiałby wówczas zawierać 0 według warunku kostki, co jest sprzecznością. Jeśli niepuste zbiory mają minimum, to nie mogą zawierać żadnych racjonalności większych niż to, więc musi to być singleton, co jest sprzeczne z warunkiem górnej zmiany. Jeżeli natomiast nie ma minimum, to więc musi być puste, co jest sprzecznością. R A R [ A ] A A A R [ A ] = Q $k=1$$R$$A$$R[A]$$A$$A$$A$$R[A] = Q$$A$Jakieś komentarze na temat tego, czy są jakieś ukryte nieoczywiste problemy definicyjne, takie jak być może ukryty niestandardowy model racjonalności?

Dalsza edycja: powyższy argument jest w przybliżeniu poprawny, ale jest błędny w zastosowaniu górnego przesunięcia. Ten operator dotyczy tylko współrzędnych nieujemnych , więc ustawienie na dowolny ujemny zbiór singletonów daje stały punkt, zgodnie z potrzebami. Innymi słowy, jeśli to jest rozwiązaniem i nie ma innych rozwiązań.m < 0 A = { m $A$$m < 0$$A = \{m\}$

Nie znam żadnych konsekwencji tego konkretnego twierdzenia, ale dowody normalizacyjne rachunku lambda, takie jak rachunek konstrukcji indukcyjnych, opierają się na dużych kardynalnych aksjomatach - nawet jeśli zbiór terminów lambda jest tak policzalny, jak tylko chcesz.

Myślę, że najlepszym sposobem na zrozumienie obliczeniowego znaczenia aksjomatów teorii mnogości potwierdzających istnienie dużych kardynałów jest myślenie o teorii mnogości jako sposobie sformułowania teorii grafów. Oznacza to, że model zbioru jest zbiorem elementów wyposażonych w relację binarną służącą do interpretacji członkostwa. Następnie aksjomaty teorii zbiorów informują o właściwościach relacji członkostwa, w tym o tym, jak można tworzyć nowe zbiory ze starych. W szczególności aksjomat podstaw oznacza, że ​​relacja członkowska jest dobrze ugruntowana (tzn. Nie ma nieskończonych łańcuchów zstępujących). Ta uzasadniona z kolei oznacza, że ​​jeśli możesz wyrównać stany wykonania programu z przechodnim członkostwem w elementach zestawu, to masz dowód zakończenia.

Zatem twierdzenie, że istnieje „duży” zestaw, ma obliczeniową wypłatę jako twierdzenie, że pewna klasa pętli w ogólnym rekurencyjnym języku programowania kończy się. Ta interpretacja działa jednolicie, od prostego starego aksjomatu nieskończoności (który uzasadnia iterację liczb naturalnych) aż do dużych kardiomimów kardynalnych.

Czy te aksjomaty są prawdziwe ? Cóż, jeśli aksjomat jest fałszywy, możesz znaleźć program w jednej z tych klas, który się nie kończy. Ale jeśli to prawda, nigdy nie będziemy pewni dzięki twierdzeniu Haltinga. Wszystko, od włączenia indukcji liczb naturalnych, jest kwestią indukcji naukowej , którą zawsze można sfałszować eksperymentem - Edward Nelson miał nadzieję udowodnić, że potęgowanie jest funkcją częściową!