b'\n_START_ARTICLE_\nTeoremi di incompletezza di G\xc3\xb6del\n_START_PARAGRAPH_\nIn logica matematica, i teoremi di incompletezza di G\xc3\xb6del sono due famosi teoremi dimostrati da Kurt G\xc3\xb6del nel 1931. Essi fanno parte dei teoremi limitativi, che precisano le propriet\xc3\xa0 che i sistemi formali non possono avere.\n_START_SECTION_\nSignificato dei teoremi di G\xc3\xb6del\n_START_PARAGRAPH_\nI teoremi di G\xc3\xb6del sono teoremi di logica del primo ordine, e devono essere collocati in questo contesto. Nella logica formale, tanto gli enunciati matematici quanto le dimostrazioni sono scritti in un linguaggio simbolico, dove \xc3\xa8 possibile verificare meccanicamente la validit\xc3\xa0 delle dimostrazioni, e non ci possono essere dubbi sul fatto che un teorema sia conseguenza degli assiomi inizialmente elencati. In teoria, qualsiasi dimostrazione sviluppata entro un sistema formale pu\xc3\xb2 essere verificata da un computer, e di fatto esistono programmi fatti per controllare la validit\xc3\xa0 delle dimostrazioni o per cercare nuove dimostrazioni (sono chiamati dimostratori automatici dei teoremi o General Theorem Prover - G.T.P.)._NEWLINE_Per definire una teoria formale bisogna conoscere e definire alcuni assiomi di partenza. Ad esempio si pu\xc3\xb2 partire da un insieme finito di assiomi, come nella geometria euclidea, oppure, con maggiore generalit\xc3\xa0, si pu\xc3\xb2 consentire che esista un insieme infinito di assiomi. In questo caso, per\xc3\xb2, deve essere possibile controllare meccanicamente se un qualsiasi enunciato \xc3\xa8 un assioma di quell\'insieme oppure no (si parla in questo caso di schema di assiomi). In informatica si direbbe che esiste un insieme ricorsivo di assiomi. Anche se pu\xc3\xb2 sembrare strano immaginare un elenco infinito di assiomi, questo \xc3\xa8 proprio ci\xc3\xb2 che si usa nella assiomatizzazione dei numeri naturali nella logica del primo ordine: quando vogliamo convertire gli assiomi di Peano in un linguaggio del primo ordine, il principio di induzione diventa uno schema di assiomi - esso dice che per ogni possibile propriet\xc3\xa0 se lo zero ha quella certa propriet\xc3\xa0 e il successore di qualsiasi numero naturale che abbia quella propriet\xc3\xa0 ha anch\'esso quella propriet\xc3\xa0, allora tutti i numeri naturali hanno quella propriet\xc3\xa0 -. Poich\xc3\xa9 ci\xc3\xb2 deve valere per ogni possibile propriet\xc3\xa0 e nel linguaggio del primo ordine non si pu\xc3\xb2 quantificare sulle propriet\xc3\xa0, l\'unico modo possibile per definire il principio di induzione in questo contesto \xc3\xa8 considerare un numero infinito di assiomi, uno per ogni possibile propriet\xc3\xa0 che si pu\xc3\xb2 definire nel linguaggio del primo ordine. La teoria assiomatica che si ottiene con tale formalizzazione \xc3\xa8 nota nell\'ambito della logica matematica con l\'acronimo PA (Peano Arithmetic)._NEWLINE_Il primo teorema di incompletezza di G\xc3\xb6del dimostra che qualsiasi sistema che permette di definire i numeri naturali \xc3\xa8 necessariamente incompleto: esso contiene affermazioni di cui non si pu\xc3\xb2 dimostrare n\xc3\xa9 la verit\xc3\xa0 n\xc3\xa9 la falsit\xc3\xa0._NEWLINE_Il fatto che possano esistere sistemi incompleti non \xc3\xa8 una scoperta particolarmente sorprendente. Ad esempio se si elimina il postulato delle parallele dalla geometria euclidea si ottiene un sistema incompleto (nel senso che il sistema non dimostra tutte le proposizioni vere). L\'essere incompleto per un sistema formale significa semplicemente - da un punto di vista semantico - che esso non include tutti gli assiomi necessari a caratterizzare univocamente uno specifico modello (\xc3\xa8 il caso ad esempio dei primi 4 assiomi di Euclide che ammettono come modello sia la geometria euclidea sia le geometrie non euclidee)._NEWLINE_Ci\xc3\xb2 che G\xc3\xb6del ha mostrato \xc3\xa8 che, in molti casi importanti, come nella teoria dei numeri, nella teoria degli insiemi o nell\'analisi matematica, non \xc3\xa8 mai possibile giungere a definire la lista completa degli assiomi che permetta di dimostrare tutte le verit\xc3\xa0. Ogni volta che si aggiunge un enunciato all\'insieme degli assiomi, ci sar\xc3\xa0 sempre un altro enunciato non incluso._NEWLINE_Si possono sempre aggiungere infiniti assiomi; ad esempio, si possono aggiungere tutti gli enunciati veri sui numeri naturali alla lista degli assiomi, ma tale lista non \xc3\xa8 un insieme ricorsivo. Se si prende un qualsiasi enunciato casuale, non sar\xc3\xa0 possibile stabilire se esso \xc3\xa8 o non \xc3\xa8 un assioma del sistema. Pertanto data una qualsiasi dimostrazione, in generale, non sar\xc3\xa0 pi\xc3\xb9 possibile verificarne la correttezza._NEWLINE_Il teorema di G\xc3\xb6del ha un\'altra interpretazione esprimibile nel contesto informatico. Nella logica del primo ordine l\'insieme di tutti i teoremi di una teoria \xc3\xa8 un insieme ricorsivamente enumerabile: ci\xc3\xb2 significa che \xc3\xa8 possibile scrivere un algoritmo che possa generare, prima o poi, ogni dimostrazione valida. Ci si pu\xc3\xb2 chiedere se questi teoremi soddisfino la propriet\xc3\xa0 pi\xc3\xb9 restrittiva di essere anche ricorsivi. \xc3\x88 possibile scrivere un programma per computer in grado di determinare con certezza se una certa affermazione \xc3\xa8 vera o falsa? Il teorema di G\xc3\xb6del dice che ci\xc3\xb2, in generale, non \xc3\xa8 possibile._NEWLINE_Molti studiosi di logica sostengono che i teoremi di incompletezza di G\xc3\xb6del abbiano definitivamente affossato il programma di David Hilbert volto a costruire un formalismo matematico universale. L\'idea generalmente condivisa \xc3\xa8 che nel secondo teorema si trovi la risposta definitiva che ha dato il colpo di grazia al programma di Hilbert, altri pensano che tale risposta si trovi nel primo teorema, ma c\'\xc3\xa8 anche chi ritiene che nessuno dei due conduca necessariamente a questo tipo di conclusione circa il programma di Hilbert.\n_START_SECTION_\nEsempi di enunciati indecidibili\n_START_PARAGRAPH_\nL\'esistenza di un enunciato indecidibile all\'interno di un sistema formale non \xc3\xa8 un fatto di per se stesso particolarmente sorprendente._NEWLINE_Nel successivo lavoro congiunto di G\xc3\xb6del e Paul Cohen si trovano esempi concreti di enunciati indecidibili (enunciati che non possono essere n\xc3\xa9 provati n\xc3\xa9 refutati): sia l\'assioma della scelta che l\'ipotesi del continuo sono indecidibili nella assiomatizzazione tradizionale della teoria degli insiemi. _NEWLINE_Questi risultati non si basano sul teorema di incompletezza._NEWLINE_Nel 1936, Alan Turing ha dimostrato che il problema dell\'arresto\xe2\x80\x94 se cio\xc3\xa8 una macchina di Turing si arresta eseguendo un certo programma \xe2\x80\x94\xc3\xa8 indecidibile. Questo risultato fu successivamente generalizzato nel campo delle funzioni ricorsive con il teorema di Rice che mostra come tutti i problemi non banali di decisione sono indecidibili in un sistema completo secondo Turing._NEWLINE_Nel 1973 si \xc3\xa8 dimostrato che il problema di Whitehead della teoria dei gruppi \xc3\xa8 indecidibile nel sistema della teoria degli insiemi._NEWLINE_Nel 1977, Kirby, Paris e Harrington dimostrarono che un enunciato della combinatorica, una variazione del teorema di Ramsey, \xc3\xa8 indecidibile nella assiomatizzazione dell\'aritmetica data dagli assiomi di Peano ma che pu\xc3\xb2 essere dimostrato nel sistema pi\xc3\xb9 ampio della teoria degli insiemi._NEWLINE_Anche il teorema di Kruskal, che trova applicazioni in informatica, \xc3\xa8 indecidibile a partire dagli assiomi di Peano, ma pu\xc3\xb2 essere dimostrato in teoria degli insiemi. _NEWLINE_Il teorema di Goodstein propone un\'affermazione relativamente semplice sui numeri naturali che \xc3\xa8 indecidibile nell\'aritmetica di Peano._NEWLINE_Gregory Chaitin ha formulato enunciati indecidibili nella teoria algoritmica dell\'informazione e ha di fatto dimostrato un suo teorema di incompletezza valido in questo settore._NEWLINE_Uno dei primi problemi sospettati di essere indecidibili fu il problema della parola per i gruppi, proposto da Max Dehn nel 1911, secondo cui esiste un gruppo finitamente generato che non possiede nessun algoritmo in grado di stabilire se due parole sono equivalenti. Solo nel 1952 si \xc3\xa8 dimostrata l\'indecidibilit\xc3\xa0 di questo problema.\n_START_SECTION_\nSchema della dimostrazione del secondo teorema\n_START_PARAGRAPH_\nSia p l\'enunciato indecidibile costruito prima, e si assuma che la coerenza del sistema sia dimostrabile all\'interno del sistema stesso. _NEWLINE_Precedentemente si \xc3\xa8 mostrato che se il sistema \xc3\xa8 coerente, allora p non \xc3\xa8 dimostrabile._NEWLINE_La dimostrazione di questa implicazione pu\xc3\xb2 essere formalizzata nel sistema stesso, e quindi l\'affermazione "p non \xc3\xa8 dimostrabile", o "\xc2\xacP(p)" pu\xc3\xb2 essere dimostrata nel sistema._NEWLINE_Ma quest\'ultima affermazione \xc3\xa8 equivalente allo stesso enunciato p (e questa equivalenza pu\xc3\xb2 essere dimostrata nel sistema), quindi p pu\xc3\xb2 essere dimostrato nel sistema. _NEWLINE_Questa contraddizione implica che il sistema deve essere incoerente.'