Logica matematica/Incompletezza/Teoremi di incompletezza di Gödel: differenze tra le versioni
Contenuto cancellato Contenuto aggiunto
Riga 43:
=== Gödelizzazione ===
Sia ora <math>g:(\mathcal{A} \cup \mathcal{F} \cup \mathrm{SEQ})
\mapsto \N</math> una funzione ricorsiva e iniettiva, detta ''numero di Gödel'' (in onore al grande logico). La funzione non fa altro che assegnare univocamente ad ogni stringa di <math>\mathcal{L=\langle A,F \rangle}</math>, e ad ogni sua sequenza di stringhe costituente una dimostrazione (l'insieme <math>\text{SEQ}</math>), uno ed un solo numero naturale, detto appunto ''numero di Gödel'' o
(\mathcal{A} \cup \mathcal{F} \cup \mathrm{SEQ})</math>. Supponiamo che anche <math>g^{-1}</math> sia ricorsiva.
Riga 50:
* la relazione <math>Dim(m,n) \subseteq \N^2</math> è definita come <math>Dim(m,n) =\{\langle m,n \rangle|
g^{-1}(m)=\langle \alpha_1,...,\alpha_k \rangle, g^{-1}(m) \in \text{DIM}, \alpha_k=g^{-1}(n)\}</math>. In sostanza, il predicato <math>Dim</math> codifica la relazione "<math>(l=\langle \alpha_1,...,\alpha_k \rangle) \vdash_S \alpha</math>", cioè, vale sse <math>l</math> dimostra <math>\alpha</math>, ovvero, sse <math>l</math> è una dimostrazione in <math>S</math> e <math>\alpha=\alpha_k</math>.
* la funzione <math>sost:\N^3 \mapsto \N</math> è definita come <math>sost(x,y,z)=g(g^{-1}(x)[\overline{z}/g^{-1}(y)])</math>, cioè, la funzione <math>sost</math> restituisce il
<math>Dim</math> e <math>sost</math> sono ricorsive, essendo definite a partire da <math>g</math>, <math>g^{-1}</math>, <math>\text{DIM}</math> e <math>\mathcal{F}</math> e non contenendo quantificatori nelle loro definizioni.
| |||