Całkowite funkcje w programie $\mathsf{Q}$

Aug 23 2020

Interesowały mnie relacje między indukcją a rekurencją, więc naturalnym pytaniem (w każdym razie moim zdaniem) było to, ile możemy udowodnić bez odwoływania się do indukcji, tj. Które funkcje są w sposób możliwy do udowodnienia rekurencyjne w $\mathsf{Q}$(Arytmetyka Robinsona). Podsumowując, funkcja$f$ w teorii arytmetycznej jest rekursywny, jak można udowodnić $T$ jeśli jest $\Sigma_1$ formuła $\phi$ w języku $T$ takie, że (i) $f(n)=m$ iff $T \vdash \phi(n, m)$ i (ii) $T \vdash \forall x \exists !y \phi(x, y)$.

Teraz myślałem, że funkcja jest rekurencyjna w$\mathsf{Q}$jeśli jest to funkcja rekurencyjna. Moje rozumowanie było następujące. Funkcja jest rekurencyjna, jeśli jest reprezentowana w$\mathsf{Q}$i jest to dobrze znany wynik (patrz https://arxiv.org/pdf/1907.00658.pdf), że reprezentowalność w $\mathsf{Q}$ jest równoważne z silną reprezentowalnością w $\mathsf{Q}$ co jest równoznaczne z możliwością udowodnienia całkowitej wartości $\mathsf{Q}$.

Jednak natychmiast się zdezorientowałem, ponieważ jeśli poprawnie zrozumiałem Fairtlough i Wainer („Hierarchie funkcji Provably Recursive”), możliwe do udowodnienia funkcje rekurencyjne $\mathsf{I}\Sigma^0_1$są dokładnie prymitywnymi funkcjami rekurencyjnymi. Od$\mathsf{I}\Sigma^0_1$ rozciąga się $\mathsf{Q}$, jest silniejszy niż $\mathsf{Q}$i dlatego nie może udowodnić, że mniej funkcji jest całkowitych. Aby dodać do tego bałaganu, pamiętam (ale może źle pamiętam), jak twierdził Nelson$\mathsf{Q}$nie może udowodnić, że potęgowanie jest całkowite. Jeśli tak jest, to oczywiście$\mathsf{Q}$nie może udowodnić, że wszystkie funkcje rekurencyjne są całkowite. Ale znowu, być może źle pamiętam twierdzenie Nelsona.

Tak więc, z jednej strony, wydaje się, że każda rekurencyjna funkcja jest sumaryczna w $\mathsf{Q}$, ale z drugiej strony wydaje się, że nawet nie wszystkie prymitywne funkcje rekurencyjne są całkowite $\mathsf{Q}$. Najwyraźniej gdzieś się pomyliłem.

Pytanie 1: Więc jakie są możliwe do udowodnienia całkowite funkcje w programie$\mathsf{Q}$?

I w zależności od odpowiedzi na to pytanie mam jedno lub drugie dalsze pytanie:

Pytanie 2a: Jeśli$\mathsf{Q}$nie nie udowodnić, dla każdej funkcji rekurencyjnej, że jest całkowity, to co ja źle o równoważności w reprezentowalności$\mathsf{Q}$ i będąc w sposób możliwy do udowodnienia całkowitym?

Pytanie 2b: Jeśli każda funkcja rekurencyjna jest sumaryczna w$\mathsf{Q}$, to o czym ja źle zrozumiałem $\mathsf{I}\Sigma^0_1$? Czy w grze jest inna definicja dającej się udowodnić sumy?

Każda pomoc w rozwiązaniu tego problemu byłaby bardzo mile widziana.

Odpowiedzi

1 NoahSchweber Aug 24 2020 at 02:16

Chodzi tutaj o subtelną różnicę między dwoma pojęciami: „dająca się udowodnić całość” (w znaczeniu Salehi) i „dająca się udowodnić rekurencyjność”. Pierwsza pokrywa się z rekurencją, ale druga nie. W konsekwencji, z mojego doświadczenia - i to wyjaśnia mój nawias powyżej - zarówno „możliwe do udowodnienia całkowite”, jak i „możliwe do udowodnienia rekurencyjne” są używane w odniesieniu do węższej klasy funkcji.

Oto odpowiednie definicje:

Funkcja $f$jest (Salehi-) możliwe do udowodnienia całkowite (i są to funkcje omówione przez Salehi), jeśli istnieje jakaś formuła$\eta$ takie, że:
- $T\vdash$ "Dla każdego $x$ jest dokładnie jeden $y$ takie że $\eta(x,y)$”.
- Dla każdego $a\in\mathbb{N}$ mamy $T\vdash\eta(\underline{a},\underline{f(a)})$.
Funkcja jest rekurencyjna (i są to funkcje, które opisujesz w swoim OP), jeśli powyższe dotyczy niektórych$\Sigma^0_1$ formuła $\eta$.

Argument, który podaje Salehi, rzeczywiście pokazuje, że każda całkowita funkcja rekurencyjna ma wartość provaby $\mathsf{Q}$. Jednak nie pokazuje tego samego w przypadku rekurencyjności możliwej do udowodnienia, a rzeczywiście rekurencyjność możliwa do udowodnienia i (prawdziwa) całkowita rekurencyjność nigdy nie pokrywają się w przypadku rozsądnych teorii, ponieważ zawsze możemy przekątować dowody w takich teoriach.

Zauważ, że możemy podobnie podzielić różne pojęcia reprezentowalności na ich „pogrubioną czcionkę” i „$\Sigma^0_1$"; jednak to w rzeczywistości niczego nie zmienia teraz (i warto to sprawdzić).

Właśnie z powodu powyższego zbiegów okoliczności, dająca się udowodnić całość w sensie Salehiego nie jest zbyt interesująca, a więc obecnie (przynajmniej z mojego doświadczenia) termin „dający się udowodnić całkowity” jest zwykle używany jako synonim „rekurencyjny, który można udowodnić”; na przykład zobaczhttps://projecteuclid.org/euclid.pl/1235421933 lub https://www.jstor.org/stable/4617258?seq=1#metadata_info_tab_contents. W szczególności, gdy mówimy „Potwierdzenie wszystkich funkcji$\mathsf{I\Sigma_1}$ są prymitywnymi funkcjami rekurencyjnymi ”- mówimy o rekurencyjności dającej się udowodnić.

Więc jakie dokładnie są funkcje rekurencyjne, które można udowodnić w programie$\mathsf{Q}$? Cóż, właściwie nie mogę znaleźć odpowiedzi na to pytanie. Ale myślę, że nie jest to zbyt zaskakujące: od tego czasu$\mathsf{Q}$ jest tak słaba, że jest to mniej interesujące pytanie niż w przypadku silniejszych teorii arytmetycznych.

To powiedziawszy, oto, co wiem (dla uproszczenia będę odnosić się do funkcji, a nie odpowiednich $\Sigma^0_1$formuły). Pozwolić$\mathfrak{Q}$ być klasą $\mathsf{Q}$funkcje rekurencyjne prawdopodobnie. Najbardziej oczywiste członkowie$\mathfrak{Q}$ są „funkcjami podobnymi do terminów”, przez co rozumiem funkcje formy $$f(x)=\begin{cases} p_1(x) & \mbox{ if }\varphi_1(x)\mbox{ holds }\\ p_2(x) & \mbox{ if }\varphi_2(x)\mbox{ holds}\\ ...\\ p_n(x) & \mbox{ if }\varphi_n(x)\mbox{ holds}\\ \end{cases}$$ dla jakiejś sekwencji $p_1,..., p_n$ wielomianów i jakiejś sekwencji $\varphi_1,...,\varphi_n$ z $\Delta^0_1$ formuły, które $\mathsf{Q}$dowodzi podziału wszechświata. W rzeczywistości każda funkcja podobna do terminu jest$\mathsf{Q}$-prawdopodobnie rekurencyjne.

Jednak to nie wyczerpuje $\mathfrak{Q}$: możemy do pewnego stopnia obejść słabość $\mathsf{Q}$patrząc na oswojone początkowe segmenty. Zasadniczo powiedz, że liczba$x$jest łagodny, jeśli poniżej zachodzi „wystarczająca arytmetyka”$x$ (np. dla wszystkich $y,z<x$ mamy to $y^z$jest zdefiniowane - dobrym ćwiczeniem jest określenie tutaj wystarczającego pojęcia oswojenia). Spójność to$\Delta_1$ własność i $\mathsf{Q}$dowodzi, że zbiór liczb oswojonych jest początkowym segmentem wszechświata. Więc możemy zdefiniować funkcję$g$ która w „części oswojonej” przekątuje się względem funkcji termopodobnych i jest zawsze $0$w „dzikiej części”. Ponieważ każda standardowa liczba naturalna jest oswojona, w rzeczywistości będziemy ją mieć$g$ nie jest terminowe.

Oczywiście od tego czasu jest to dość głupie $g$jest ostatecznie równa funkcji termopodobnej. Przejdźmy więc do przodu:

Dla $T$ teoria arytmetyki może zawierać więcej symboli funkcyjnych niż tylko $+$ i $\times$ (na przykład $\mathsf{PRA}$ lub $\mathsf{PA}$ + prymityw do potęgowania), powiedzmy, że a $T$-prawdopodobnie rekurencyjna funkcja $f(x_1,...,x_n)$ jest $T$-specjalny iff dla każdego semestru$t(x_1,..., x_n, y_1,...,y_k)$ mamy $$T\vdash\forall a_1,...,a_k\exists b\forall c_1>b, ..., c_n>b[f(c_1,...,c_n)\not=t(c_1,...,c_n, a_1,...,a_k)].$$ Zasadniczo $T$-funkcje specjalne to te, które ostatecznie różnią się od każdego terminu funkcja (z dozwolonymi parametrami). Pisać "$\mathfrak{Spec}(T)$„za zestaw $T$-funkcje specjalne.

Zanim przejdę dalej, pozwolę sobie na kilka szybkich obserwacji:

Moglibyśmy również przyjrzeć się, co się stanie, jeśli zastąpimy „wspólnie często” słowem „bardzo często”, ale nie wydaje się to tak naturalne: na przykład $T=\mathsf{PA}$ funkcja wysyłania $x$ do $2^x$ Jeśli $x$ jest równa i do $0$ w przeciwnym razie liczyłby się jako wyjątkowy według tej ostatniej definicji, podczas gdy moim zdaniem zdecydowanie nie powinien.
Musimy uważać, jak interpretujemy $\mathfrak{Spec}(T)$: możemy mieć konserwatywne rozszerzenie $S$ z $T$ z $\mathfrak{Spec}(S)\subsetneq\mathfrak{Spec}(T)$(rozważ rozszerzenia według definicji). Więc w celu leczenia$\mathfrak{Spec}(T)$ jako miara siły $T$, musimy skupić się na jednym języku - powiedzmy, $\{+,\times\}$. Jednak kiedy już to zrobimy, wszystko jest całkiem przyjemne od kiedy$T$ i $S$ są teorie w tym samym języku $T\subseteq S$ sugeruje $\mathfrak{Spec}(T)\subseteq\mathfrak{Spec}(S)$.

Moim zdaniem w ograniczonym języku, takim jak $\{+,\times\}$niedobór funkcji specjalnych można rozsądnie uznać za rodzaj słabości. To rodzi naturalne pytanie: