Il teorema di completezza aritmetizzata
Nell'articolo di Kikuchi Kolmogorov complessità e il secondo teorema di incompletezza egli afferma il "teorema di completezza aritmetizzata" come segue:
Permettere $T$ essere una teoria ricorsivamente assiomatizzabile in una lingua $\mathcal{L}$, $C$ essere un insieme di nuove costanti e $\overline{\mathcal{L}}=\mathcal{L}\cup C$. Diciamo una formula$\phi(x)$ in $\mathcal{L}_{A}$ definisce un modello di $T$ in una teoria $S$ in $\mathcal{L}_{A}$ se possiamo provare dentro $S$ che il set
$$ \{ \sigma : \text{$\sigma$ is a sentence in $\ overline {\ mathcal {L}}$ that satisfies $\ phi (\ ulcorner \ sigma \ urcorner)$} \} $$
forma un diagramma elementare di un modello di $T$ con un universo da $C$.
Teorema 4.1. (Il teorema di completezza aritmetizzata). Esiste una formula$\text{Tr}_{T}({\ulcorner}x{\urcorner})$ in $\mathcal{L}_{A}$ [il linguaggio dell'aritmetica] che definisce un modello di $T$ in $\text{PA} + \text{Con}(T)$ , dove $\text{Con}(T)$ è una frase in $\mathcal{L}_{A}$ questo significa $T$ è consistente.
Ci sono diversi aspetti di questo teorema che non capisco:
La nozione di formula che definisce un modello di $T$ in $\text{PA} + \text{Con}(T)$ coinvolge il set $ \{ \sigma : \text{$\sigma$ is a sentence in $\ overline {\ mathcal {L}}$ that satisfies $\ phi (\ ulcorner \ sigma \ urcorner)$} \} $. Non so come formalizzarlo in$\text{PA}$, figuriamoci provare qualcosa al riguardo.
La stessa cosa con il parlare di modelli di $T$. Dire$T = \text{ZFC}$, allora come puoi persino affermare nel linguaggio dell'aritmetica di cui esiste un modello $T$ con tale o tale proprietà (il suo diagramma elementare è l'insieme di cui sopra e il suo universo)?
Un diverso tipo di domanda: a cosa serve questo teorema (in termini generali, al di là della carta citata)? Perché si chiama teorema di completezza aritmetizzata?
Risposte
Ri: $(1)$, c'è meno qui di quanto sembri. Il punto chiave è che possiamo inventare una formula$\theta$ che definisce l'insieme dei numeri Godel di $\overline{\mathcal{L}}$-frasi; con questo in mano, stiamo solo guardando$$S=\{x: \theta(x)\wedge\phi(x)\}.$$ Questo è abbastanza noiosamente definibile.
Ora quando lo diciamo $S$ è il diagramma elementare di una struttura con dominio $C$, intendiamo quello $S$ soddisfa le proprietà usuali di un diagramma elementare - e poiché queste sono proprietà sintattiche, possiamo esprimere con la numerazione di Godel che $S$li possiede o non li possiede. Ad esempio, vorremo ciascuno dei seguenti:
Se $\ulcorner\sigma_0\urcorner$, $\ulcorner\sigma_1\urcorner\in S$ poi $\ulcorner\sigma_0\wedge\sigma_1\urcorner\in S$.
Se $\ulcorner \exists x\sigma(x)\urcorner\in S$ poi per alcuni $c\in C$ noi abbiamo $\ulcorner\sigma(c)\urcorner\in S$. (Questo riguarda il "con l'universo da$C$" po.)
$\ulcorner\perp\urcorner\not\in S$.
Un po 'più accuratamente, abbiamo funzioni ricorsive primitive corrispondenti ad es. Congiunzione e quantificazione esistenziale rispetto ad alcune variabili fisse, ei primi due elenchi puntati sopra corrispondono a condizioni di chiusura / esistenza appropriate su $S$rispetto a queste funzioni. Il terzo punto elenco nel frattempo impedisce la banalità.
Fondamentalmente, il punto è che la proprietà di essere il diagramma elementare di una struttura con dominio $\mathbb{N}$ è esprimibile di primo ordine (perché equivale a "condizioni di chiusura / esistenza / non esistenza locali" per quanto sopra).
Ri: $(2)$, intuitivamente parlando il punto è che non stiamo parlando di modelli arbitrari di es $\mathsf{ZFC}$, ma solo quelli con dominio $\mathbb{N}$. Una struttura con dominio$\mathbb{N}$ è interamente descritto da un unico insieme di numeri naturali $X$, e "$X$ è il diagramma atomico di un modello di $\mathsf{ZFC}$"è esprimibile in base al primo ordine di cui sopra: diciamo solo"$X$ ha le proprietà sintattiche di base sopra, e ciascuna $\mathsf{ZFC}$-Assiomi è dentro $X$. "
Penso che questo potrebbe essere reso più misterioso perché di solito pensiamo a modelli di $\mathsf{ZFC}$come altamente complicata e sicuramente non avendo dominio$\mathbb{N}$. Ma per Lowenheim-Skolem verso il basso,$\mathsf{ZFC}$(supponendo che sia affatto coerente) ha anche molti modelli con dominio$\mathbb{N}$. Questi sono i modelli che possiamo considerare in questo approccio.
Ri: $(3)$, il punto è che il solito fraseggio del teorema di completezza
ogni teoria coerente ha un modello
è totalmente folle nel contesto dell'aritmetica. Fondamentalmente, possiamo parlare direttamente di insiemi finiti solo nel linguaggio dell'aritmetica, quindi se ingenuamente "formuliamo aritmeticamente" la frase "l'aritmetica di Presburger non ha modelli" otteniamo qualcosa di vero.
(Vedi ad esempio l' interpretazione di Ackermann . Possiamo passare da (diciamo)$\mathsf{PA}$ a una teoria degli insiemi appropriatamente equivalente, ma quella teoria dimostra che "Ogni insieme è finito".)
Quindi, se vogliamo che una qualche versione del teorema di completezza valga in una teoria dell'aritmetica, i suoi "modelli" devono consistere in relazioni sull'intero universo; e ovviamente dovranno consistere in relazioni definibili , dal momento che non si può parlare internamente di relazioni indefinibili.
Un'altra opzione sarebbe quella di utilizzare estensioni conservative che possono parlare direttamente di insiemi infiniti; questo è ad esempio l'approccio adottato qui . In tutti i contesti in cui ho giocato questo approccio funziona e quindi generalmente lo preferisco. Detto ciò,$(i)$ se ricordo bene ci sono situazioni in cui questo approccio è fastidiosamente sgradevole o oscura informazioni preziose (penso che ciò avvenga con teorie aritmetiche molto deboli) e $(ii)$ il fatto che possiamo ottenere un teorema di completezza solo nel linguaggio dell'aritmetica del primo ordine è interessante di per sé.