Possibilmente funzioni totali in $\mathsf{Q}$

Aug 23 2020

Ero interessato alle relazioni tra induzione e ricorsione, e quindi una domanda naturale (a mio avviso, comunque), era quanto possiamo dimostrare senza fare appello all'induzione, cioè quali funzioni sono dimostrabilmente ricorsive in $\mathsf{Q}$(Robinson Arithmetic). Ricapitolando, una funzione$f$ è provabilmente ricorsivo in una teoria aritmetica $T$ se è presente un file $\Sigma_1$ formula $\phi$ nella lingua di $T$ tale che (i) $f(n)=m$ iff $T \vdash \phi(n, m)$ e (ii) $T \vdash \forall x \exists !y \phi(x, y)$.

Ora, ho pensato che una funzione fosse dimostrabilmente ricorsiva in$\mathsf{Q}$se e solo una funzione ricorsiva. Il mio ragionamento era il seguente. Una funzione è ricorsiva se e solo se è rappresentabile in$\mathsf{Q}$, e, è un risultato ben noto (vedi https://arxiv.org/pdf/1907.00658.pdf) che la rappresentabilità in $\mathsf{Q}$ è equivalente a una rappresentabilità forte in $\mathsf{Q}$ che equivale ad essere dimostrabilmente totale in $\mathsf{Q}$.

Tuttavia, sono diventato immediatamente confuso, perché, se ho capito correttamente Fairtlough e Wainer ("Gerarchie di funzioni ricorsive provabili"), le funzioni ricorsive dimostrabili di $\mathsf{I}\Sigma^0_1$sono esattamente le primitive funzioni ricorsive. Da$\mathsf{I}\Sigma^0_1$ si estende $\mathsf{Q}$, è più forte di $\mathsf{Q}$, e quindi non può dimostrare che un numero inferiore di funzioni è totale. Per aggiungere al pasticcio, ricordo (ma forse sto ricordando male) Nelson che lo ha affermato$\mathsf{Q}$non può provare che l'elevazione a potenza sia totale. Se è così, allora ovviamente$\mathsf{Q}$non può dimostrare che tutte le funzioni ricorsive siano totali. Ma, ancora una volta, potrei ricordare male l'affermazione di Nelson.

Quindi, da un lato, sembra che ogni funzione ricorsiva sia dimostrabilmente totale in $\mathsf{Q}$, ma, dall'altro, sembra che nemmeno tutte le funzioni ricorsive primitive siano totali in $\mathsf{Q}$. Chiaramente ho sbagliato da qualche parte.

Domanda 1: Allora, in quali sono le funzioni totali comprovabili$\mathsf{Q}$?

E, a seconda della risposta a questa domanda, ho l'una o l'altra ulteriore domanda:

Domanda 2a: If$\mathsf{Q}$non senza provare, per ogni funzione ricorsiva, che è totale, allora che cosa ho frainteso circa l'equivalenza tra rappresentabilità in$\mathsf{Q}$ ed essere dimostrabilmente totale?

Domanda 2b: se ogni funzione ricorsiva è dimostrabilmente totale in$\mathsf{Q}$, allora cosa ho capito male $\mathsf{I}\Sigma^0_1$? C'è una diversa definizione di totale dimostrabile in gioco?

Qualsiasi aiuto per risolvere questo problema sarebbe molto apprezzato.

Risposte

1 NoahSchweber Aug 24 2020 at 02:16

Il problema qui è una sottile differenza tra due nozioni: "totalità dimostrabile" (nel senso di Salehi) e "ricorsività dimostrabile". Il primo coincide con la ricorsività, ma il secondo no. Di conseguenza, nella mia esperienza - e questo spiega la mia parentetica sopra - sia "provabilmente totale" che "provabilmente ricorsivo" sono usati per riferirsi alla classe di funzioni più ristretta.

Ecco le definizioni rilevanti:

Una funzione $f$è (Salehi-) dimostrabilmente totale (e queste sono le funzioni di cui Salehi discute) se e solo se c'è una formula$\eta$ tale che:
- $T\vdash$ "Per ciascuno $x$ ce n'è esattamente uno $y$ tale che $\eta(x,y)$. "
- Per ciascuno $a\in\mathbb{N}$ noi abbiamo $T\vdash\eta(\underline{a},\underline{f(a)})$.
Una funzione è dimostrabilmente ricorsiva (e queste sono le funzioni che descrivi nel tuo OP) se e solo quanto sopra vale per alcune$\Sigma^0_1$ formula $\eta$.

L'argomento fornito da Salehi mostra effettivamente che ogni funzione ricorsiva totale è risultata totale $\mathsf{Q}$. Tuttavia, non mostra lo stesso per la ricorsività dimostrabile, e infatti la ricorsività dimostrabile e la ricorsività totale (genuina) non coincidono mai per le teorie ragionevoli poiché possiamo sempre diagonalizzare contro le prove in tali teorie.

Nota che possiamo allo stesso modo suddividere le varie nozioni di rappresentabilità nei loro "grassetto" e "$\Sigma^0_1$"; tuttavia, questo in realtà non cambia nulla ora (ed è un buon esercizio per verificarlo).

Proprio a causa della coincidenza di cui sopra, la totalità dimostrabile nel senso di Salehi non è molto interessante, e quindi in questi giorni (almeno nella mia esperienza) "provabilmente totale" è solitamente usato come sinonimo di "ricorsivo dimostrabile"; per esempio, vedihttps://projecteuclid.org/euclid.pl/1235421933 o https://www.jstor.org/stable/4617258?seq=1#metadata_info_tab_contents. In particolare, quando diciamo "Le funzioni comprovabilmente totali di$\mathsf{I\Sigma_1}$ sono le funzioni ricorsive primitive ", ci riferiamo alla ricorsività dimostrabile.

Allora, in cosa sono esattamente le funzioni ricorsive provabili$\mathsf{Q}$? Beh, in realtà non riesco a trovare una risposta a questa domanda. Ma questo non è troppo sorprendente, penso: da allora$\mathsf{Q}$ è così debole questa è una domanda meno interessante che per teorie aritmetiche più forti.

Detto questo, ecco quello che so (per semplicità mi riferirò a funzioni piuttosto che appropriate $\Sigma^0_1$formule). Permettere$\mathfrak{Q}$ essere la classe di $\mathsf{Q}$- funzioni probabilmente ricorsive. I membri più evidenti di$\mathfrak{Q}$ sono le "funzioni simili a termini", con le quali intendo le funzioni della forma $$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}$$ per qualche sequenza $p_1,..., p_n$ di polinomi e qualche sequenza $\varphi_1,...,\varphi_n$ di $\Delta^0_1$ formule che $\mathsf{Q}$dimostra la divisione dell'universo. Banalmente ogni funzione simile a un termine è$\mathsf{Q}$-provabilmente ricorsivo.

Tuttavia, questo non esaurisce $\mathfrak{Q}$: possiamo in una certa misura aggirare la debolezza di $\mathsf{Q}$guardando i segmenti iniziali addomesticati. Fondamentalmente, dì che un numero$x$è docile se "abbastanza aritmetica" vale di seguito$x$ (ad esempio per tutti $y,z<x$ ce l'abbiamo $y^z$è definito - è un buon esercizio definire qui una nozione sufficiente di docilità). Tameness è un$\Delta_1$ proprietà e $\mathsf{Q}$dimostra che l'insieme dei numeri addomesticati è un segmento iniziale dell'universo. Quindi possiamo definire una funzione$g$ che sulla "parte addomesticata" diagonalizza con funzioni simili a termini ed è sempre $0$sulla "parte selvaggia". Poiché ogni numero naturale standard è docile, in effetti lo avremo$g$ non è simile a un termine.

Naturalmente, questo è piuttosto sciocco da allora $g$è alla fine uguale a una funzione simile a un termine. Quindi andiamo avanti:

Per $T$ una teoria dell'aritmetica che potrebbe contenere più simboli di funzione che solo $+$ e $\times$ (per esempio $\mathsf{PRA}$ o $\mathsf{PA}$ + una primitiva per l'elevazione a potenza), diciamo che a $T$-funzione probabilmente ricorsiva $f(x_1,...,x_n)$ è $T$-speciale iff per ogni termine$t(x_1,..., x_n, y_1,...,y_k)$ noi abbiamo $$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)].$$ Fondamentalmente, il $T$-le funzioni speciali sono quelle che sono eventualmente diverse da ogni termine funzione (con parametri consentiti). Scrivi "$\mathfrak{Spec}(T)$"per il set di $T$-funzioni speciali.

Prima di andare avanti, lasciatemi fare un paio di rapide osservazioni:

Potremmo anche esaminare cosa succede se sostituiamo "spesso cofinalmente" con "spesso insieme", ma questo non sembra così naturale: ad esempio, prendere $T=\mathsf{PA}$ la funzione invio $x$ per $2^x$ Se $x$ è pari e a $0$ altrimenti conterebbe come speciale per quest'ultima definizione, mentre a mio parere chiaramente non dovrebbe.
Dobbiamo stare attenti a come interpretiamo $\mathfrak{Spec}(T)$: possiamo avere un'estensione conservativa $S$ di $T$ con $\mathfrak{Spec}(S)\subsetneq\mathfrak{Spec}(T)$(considera le espansioni per definizioni). Quindi, per trattare$\mathfrak{Spec}(T)$ come misura della forza di $T$, dobbiamo limitare l'attenzione a una singola lingua, ad esempio $\{+,\times\}$. Una volta fatto ciò, tuttavia, le cose vanno abbastanza bene da allora se$T$ e $S$ allora sono teorie nella stessa lingua $T\subseteq S$ implica $\mathfrak{Spec}(T)\subseteq\mathfrak{Spec}(S)$.

A mio parere, all'interno di un linguaggio limitato come $\{+,\times\}$una scarsità di funzioni speciali può ragionevolmente essere considerata una sorta di debolezza. E quindi questo solleva una domanda naturale: