Teorema di indefinibilità di Tarski

Il teorema di indefinibilità di Tarski, enunciato e dimostrato da Alfred Tarski nel 1935, è un importante risultato limitativo della logica matematica, dei fondamenti della matematica e della semantica formale. L'enunciato si può esprimere, in termini non rigorosi, come

La verità aritmetica non può essere definita all'interno dell'aritmetica.

Il teorema si applica più generalmente ad ogni sistema formale sufficientemente potente, mostrando che la verità nel modello del sistema non può essere definita all'interno del sistema stesso.

Storia

Nel 1931, Kurt Gödel pubblicò i suoi famosi teoremi di incompletezza, in cui mostra come rappresentare enunciati sulla sintassi aritmetica (meta-enunciati) all'interno dell'aritmetica stessa, assegnando ad ogni formula del linguaggio aritmetico un numero distinto. Questa procedura è nota come numerazione di Gödel, codifica e più in generale come aritmetizzazione.

In particolare, molti insiemi di espressioni sono codificati come insiemi di numeri. Così si scopre che questi insiemi sono computabili rispetto a molte proprietà sintattiche (come l'essere una formula, l'essere una formula chiusa, ecc.). Inoltre, qualsiasi insieme computabile di numeri può essere definito da qualche formula aritmetica. Ad esempio, ci sono formule nel linguaggio aritmetico che definiscono l'insieme delle espressioni per le formule aritmetiche, e ci sono formule per definire l'insieme delle formule aritmetiche dimostrabili. Questi ultimi esempi fanno notare come un linguaggio che permette l'aritmetica sia abbastanza potente da descrivere le sue stesse proprietà sintattiche, con tutto quello che l'autoreferenzialità comporta.

Il teorema di indefinibilità mostra come questo tipo di codifica non può essere utilizzato per concetti semantici come, ad esempio, la verità. Questo significa che nessun linguaggio per quanto riccamente interpretato può rappresentare la sua stessa semantica. Un corollario è che ogni metalinguaggio capace di esprimere la semantica di un linguaggio formale deve avere una potenza espressiva maggiore del linguaggio formale. Un metalinguaggio, infatti, include nozioni primitive, assiomi e regole che sono assenti nel linguaggio formale e per questo motivo ci sono teoremi dimostrabili nel metalinguaggio che non sono dimostrabili nel linguaggio formale.

Il teorema di indefinibilità è abitualmente attribuito ad Alfred Tarski. Lo stesso Gödel scoprì il teorema di indefinibilità nel 1930, mentre dimostrava il suo teorema di incompletezza, e quindi molto prima della pubblicazione di Tarski che risale al 1935. Sebbene Gödel non abbia mai rivendicato pubblicamente la sua dimostrazione indipendente dell'indefinibilità, ne scrisse a John von Neumann in una lettera del 1931. Tarski ottenne quasi tutti i risultati del suo scritto Der Wahrheitsbegriff in den formalisierten Sprachen, pubblicato nel '36, tra il 1929 e il 1931, e li espose al pubblico polacco. Infatti, come sottolineò egli stesso nell'articolo, il teorema di indefinibilità era l'unico risultato non ottenuto già molto tempo prima. Come recita la nota a piè di pagina relativa al teorema di indefinibilità (Satz I) dell'articolo del '36, il teorema e la dimostrazione furono aggiunti solo dopo che il libro venne mandato a stampare. Quando Tarski aveva presentato lo scritto alla Accademia delle Scienze di Varsavia era stato in grado di fornire solo alcune congetture invece del risultato che ottenne in seguito ai suoi sforzi e, in parte, grazie al teorema di incompletezza di Gödel annunciato nell'articolo "Einige metamathematische Resultate über Entscheidungsdefinitheit und Widerspruchsfreiheit", Akademie der Wissenschaft in Wien, 1930.

Enunciato del teorema

La versione semplificata dice: sia L il linguaggio dell'aritmetica del primo ordine, e N la sua struttura standard. Dunque (L, N) è il "linguaggio interpretato dell'aritmetica del primo ordine". Sia ora T l'insieme degli L-enunciati veri in N, e T* l'insieme dei numeri di Gödel degli enunciati di T. Il teorema dimostra che non è possibile che T* sia definito da una formula dell'aritmetica del primo ordine.

Teorema di indefinibilità di Tarski: non esiste alcuna L-formula Vero(x) che definisce T*. Cioè, non esiste alcuna L-formula Vero(x) tale che per ogni L-formula x, Vero(x) se e solo se x è vero.

Voci correlate

• Teorema di Henkin

Collegamenti esterni

• Alfred Tarski, "The Concept of Truth in Formalized Languages" (PDF)