Il teorema di indecidibilità

Questo teorema si può enunciare, con qualche semplificazione, come segue:

Se un sistema formale S è consistente, allora esiste un enunciato V vero ma non dimostrabile in S

cioè la consistenza di S implica l'esistenza di (almeno un) enunciato V vero ma non dimostrabile in S.
Prima di discutere sensatamente di questo teorema bisognerebbe definire accuratamente il concetto di sistema formale, ma preferisco lasciar perdere (vedi comunque qui, dove scrivo 'assiomatico', invece che 'formale'). Non che la faccenda sia particolarmente complessa ma, nello spirito di queste pagine, voglio essere davvero semplice nei ragionamenti e devo dire che, anche se il lavoro originale di Gödel non è poi così mostruosamente difficile come si può essere portati a credere, è senz'altro vero che tale lavoro non è semplice... Ho cercato di semplificarlo ma non ci sono riuscito (grazie!) però, anche se non sono stato abile, sono stato fortunato: mi è capitato tra le mani un libro di Roger Penrose (Ombre della mente, Rizzoli 1996) dove viene discussa una 'versione' estremamente semplice del teorema di Gödel, versione sviluppata appunto da Penrose, che sfrutta il concetto di macchina di Turing e che, per essere compresa, non abbisogna di tutto l'enorme apparato formale che si trova - necessariamente - nel lavoro originale di Gödel. Qui riporterò questa versione di Penrose con alcune modifiche che, probabilmente, ne indeboliranno la struttura formale ma che, credo, rendono il teorema di Gödel davvero alla portata di tutti.

Il significato del teorema

Prima di dimostrare il teorema però, cerchiamo di capire davvero il significato di quanto dimostrato da Gödel. A prima vista sembra di aver raggiunto un limite insuperabile: ci sono affermazioni vere che sono indimostrabili, della cui verità cioè non ci potremo mai convincere. Giusto? No, sbagliato! Direi invece che il teorema di indecidibiltà, se lo si segue con un po' di attenzione, ci dice proprio il contrario! In effetti, come vedremo, si può ben dimostrare che una certa proposizione esprimibile nel (e dipendente dal) sistema formale S è vera, anche se questa dimostrazione non potrà mai essere espressa nella sintassi del sistema S stesso! Insomma, Gödel dimostra che l'intuito del matematico umano è in grado di 'svincolarsi' dai limiti imposti da un qualsivoglia sistema formale per cogliere delle verità che resteranno per sempre inconoscibili come tali se si resta nei limiti del sistema.

Sistemi formali ed informatica

Per dimostrare il teorema di Gödel nella forma di Turing-Penrose si deve dapprima evidenziare il rapporto (che dovrà essere il più stretto possibile) tra sistemi formali ed informatica, anzi, più precisamente, tra la coppia di concetti:

e

Senza stare a diventar matti col formalismo, vediamo di convincerci di quanto stretto possa essere questo rapporto con un esempio banale, tratto dall'ordinaria aritmetica (che qui gioca il ruolo del sistema formale S) ed espresso in uno pseudolinguaggio che spero sia chiaro a tutti:

Linguaggio del sistema formale S:

Linguaggio dell'informatica:

Chiamiamo questo programma P0. Vediamo che in un senso ben preciso P0 dipende dal numero intero '2', infatti nel corso della sua esecuzione ciascun numero utilizzato 'internamente' (a, b e c) viene elevato all'esponente 2. Ovvio, perché l'enunciato di partenza si riferiva a numeri quadrati. Indichiamo il programma P0 agente sul numero '2' con la notazione P0(2). Come abbiamo visto P0(2), riferentesi ad un enunciato vero, termina con successo. Vediamo cosa succede con P0(1) cioè al programma analogo a P0(2) dove la condizione:

se a2=b2+c2
viene sostituita da
se a=b+c.

Il banale enunciato relativo, anch'esso vero, afferma che esiste almeno un numero esprimibile come somma di due numeri, e P0(1) termina al secondo ciclo, dopo aver banalmente stampato 2,1,1.
Per trovare qualcosa di più interessante non ci occorrerà essere particolarmente originali: P0(3) equivale all'enunciato 'esiste almeno un cubo esprimibile come somma di due cubi' ed è un caso particolare del celeberrimo ultimo teorema di Fermat. Sappiamo quindi che l'enunciato è falso; che succede al nostro programma P0(3)? Beh, visto che non esiste un cubo esprimibile come somma di due cubi, la condizione:

se a3=b3+c3

non verrà mai soddisfatta, quindi il programma non potrà mai stampare a, b e c, continuerà a ripetere insensatamente il ciclo programmato, incrementando sempre a, b e c e non terminerà mai!

Attenzione: questo fatto non ha niente a che vedere con le proposizioni indecidibili di Gödel: avremmo potuto essere più bravi nello scrivere il programma che realizza l'enunciato in questione, e farlo terminare stampando ad esempio: 'CASO IMPOSSIBILE'. È proprio considerando programmi di questo genere, che terminano quando i nostri programmi tipo P0(n) non terminano, che troveremo le proposizioni indecidibili.

Torniamo al nostro programma P0 ed osserviamo che, quando opportunamente generalizzato

Tutti questi enunciati realizzati da P0 hanno in comune il fatto di riferirsi a tentativi di trovare un numero (di un certo 'tipo' dipendente da n - quadrato, cubo...) esprimibile come somma di due numeri del medesimo 'tipo'.
Non è difficile convincersi che è effettivamente possibile scrivere un programma P1 che realizza un enunciato differente, e che, a seconda del valore di n, termina o non termina in dipendenza del fatto che l'enunciato corrispondente a P1 relativo ad n (cioè P1(n)) sia vero o falso, e così via con P2, P3, eccetera.
Ora, proviamo a convincerci di avere a disposizione un elenco completo di tutti gli enunciati possibili nel sistema formale S dipendenti da un solo numero, così che i programmi Pm con m=0,1,2,3... rappresentino tutti questi possibili enunciati. Come prima esprimeremo la dipendenza di Pm da n con la notazione Pm(n).
Ora chiediamoci se è possibile scrivere un gran bel programma, chiamiamolo D, che, applicato a Pm(n), sia in grado di dirci, senza sbagliare, se Pm(n) termina oppure no. Cosa stiamo chiedendo al nostro bel programma D? Ad esempio, cosa dovrebbe dirci D applicato a P0(3)? Dopo averlo esaminato ben bene, D dovrebbe terminare e dirci una cosa del tipo:

P0(3) non termina
e dovrebbe anche poterci dire
P0(4) non termina
e ancora
P0(5) non termina

e così via... Insomma, D dovrebbe essere in grado, quando applicato ai vari P0(n) con n > 2, di comportarsi come una dimostrazione dell'ultimo teorema di Fermat! Come se non bastasse D, applicato a P1(n), dovrebbe poter 'dimostrare' allo stesso modo l'enunciato relativo al programma P1(n), e così via per P2(n), P3(n) eccetera... Insomma, il nostro bel programma D svolge praticamente il ruolo delle regole del sistema formale S, regole che dovrebbero essere in grado di assegnare il valore vero o falso a tutti gli enunciati (dipendenti da un solo numero) esprimibili in S!
Vedremo che un tale D, indipendentemente dalla nostra bravura, non può venir scritto, e questa impossibilità è l'espressione del teorema di indecidibiltà di Gödel nella versione di Penrose-Turing.

Dimostrazione

Coerentemente con quanto detto poco sopra, supponiamo di avere a disposizione i programmi Pm(n) (che rappresentano tutti i possibili enunciati del sistema formale S dipendenti da un solo numero n) ed indichiamo l'azione di D (che rappresenta le regole di S) su Pm(n) con D(m,n) e diciamo:

(G1.1)

se D(m,n) termina allora Pm(n) non termina

e questo sia senza errori: se D(m,n) termina allora è 'davvero vero' che Pm(n) non termina.
Nostro scopo è dimostrare che D non può racchiudere il nostro concetto di verità, e questo lo otterremo trovando un ben definito programma tra i Pm(n) tale che noi sappiamo che non termina ma che D non riesce ad identificare.
A questo scopo consideriamo il valore m=n (procedura di diagonalizzazione), e otteniamo:

(G1.2)

se D(n,n) termina allora Pn(n) non termina.

Ora D(n,n) è un programma che dipende dal solo numero n e non più da due, come prima: sarà quindi presente nella lista dei programmi che abbiamo costruito e che dipendono appunto da un solo numero. Diciamo che questo programma sia Pk, cioè:

(G1.3)

D(n,n) = Pk(n)

così che la (G1.2) diventa:

(G1.4)

se Pk(n) termina allora Pn(n) non termina.

Applichiamo ancora il procedimento diagonale e poniamo n=k. Otteniamo:

(G1.5)

se Pk(k) termina allora Pk(k) non termina.

Questo suona un po' come una presa per i fondelli, però si può concludere qualcosa di buono dalla (G1.5): chiediamoci se Pk(k) termina o no, e cominciamo col supporre che termini. Dalla sconcertante (G1.5) concludiamo che se Pk(k) terminasse allora non terminerebbe, e questa è una contraddizione bella e buona. Tale contraddizione ci forza a concludere che in effetti Pk(k) non termina! Ma la (G1.3) ci dice che Pk(k) è la stessa cosa di D(k,k), e allora 'anche' D(k,k) non termina. Quindi il nostro bel programma D non riesce a dirci che il particolare programma Pk(k) non termina.

La conclusione è questa: abbiamo trovato il programma Pk(k) che noi sappiamo che non termina, ma il programma che dovrebbe avvertirci di questo fatto, cioè D(k,k), non è in grado di accorgersene.

Questa conclusione si può enunciare così (tra parentesi l'enunciato nei termini dei sistemi formali che - si noterà - è proprio il teorema di Gödel enunciato all'inizio):

Se il programma D(m,n) non commette errori nel dichiarare che un programma Pm(n) non termina (se un sistema formale S è consistente) allora esiste un programma Pk(k) che non termina e D(k,k) non è in grado di dichiarare questo fatto (allora esiste un enunciato V vero ma non dimostrabile in S)

Notiamo esplicitamente che questa conclusione, in un senso molto forte, è del tutto indipendente da quale D stiamo considerando. Qualunque D' possiamo trovare ha per così dire 'nascosto dentro di sé' il programma che se ne fa beffe: per trovarlo basta ripetere il ragionamento appena fatto sostituendo al nostro vecchio D il nuovo D'. Nei termini dei sistemi formali in qualunque sistema formale esistono affermazioni vere ma non dimostrabili.

Alcune osservazioni conclusive

Per rendersi conto precisamente della verità di questo fatto occorre studiarsi il teorema nella sua forma originale, ma noi ci accontentiamo di quanto detto fin qui, e passiamo ad altro...



Home