La Prova Logica di Dio? Un Viaggio Affascinante negli Argomenti di Gödel e Scott

Ciao a tutti! Oggi voglio portarvi con me in un’avventura intellettuale davvero particolare, un viaggio ai confini tra logica, filosofia e persino teologia. Parleremo di qualcosa che ha affascinato menti brillanti per secoli: l’argomento ontologico per l’esistenza di Dio. Ma non una versione qualsiasi! Ci tufferemo nelle varianti proposte da due giganti del pensiero logico-matematico: Kurt Gödel e Dana Scott. Preparatevi, perché useremo strumenti modernissimi, quasi fantascientifici, per analizzare queste idee secolari. Sarà un po’ come usare un acceleratore di particelle per studiare un testo antico, ma applicato alla metafisica!

Un Incontro Storico e un Segreto Svelato

Tutto inizia in modo quasi romanzesco. Immaginate la scena: primavera 1970, Dipartimento di Filosofia di Princeton. Un Kurt Gödel ormai anziano si incontra confidenzialmente con Dana Scott (che all’epoca era più giovane, il “senior author” del testo originale da cui prendo spunto). Gödel gli affida delle note, chiedendogli di custodirle. Tra queste, uno schizzo stringato di una prova ontologica, frutto di anni di studio su Anselmo, Leibniz e altri. Gödel era convinto che la sua versione, espressa con un rigore matematico inedito in una logica modale d’ordine superiore, fosse un passo avanti significativo.

Poco dopo, però, Scott, in un momento che lui stesso ricorda con imbarazzo come “molto poco professionale”, menziona la prova (peraltro leggermente modificata da lui) durante un seminario di logica modale. Apriti cielo! La notizia si diffonde a macchia d’olio. Scott parte presto per Oxford e non discuterà mai più la cosa direttamente con Gödel. Solo dopo la morte di Gödel, nel suo lascito (il *Nachlass*), verrà ritrovato un manoscritto datato 1970, considerato la versione finale dell’argomento secondo Gödel. Ed è proprio su questo testo, e sulla variante di Scott, che noi (parlo come parte del team di ricerca che ha lavorato su queste formalizzazioni) abbiamo concentrato i nostri esperimenti computazionali.

Gli Strumenti del Mestiere: Logica Modale e Assistenti di Prova

Perché Gödel usa la logica modale? Semplice: doveva distinguere tra esistenza *possibile* ed esistenza *necessaria* di Dio. La logica classica non basta, servono gli operatori modali come e#x25A1; (necessario) e e#x25C7; (possibile). E perché la logica d’ordine superiore (HOL)? Perché l’argomento parla di “proprietà”, e persino di “proprietà di proprietà” (come la proprietà “essere positiva” applicata ad altre proprietà), concetti che richiedono la potenza espressiva della HOL.

Ora, come facciamo a essere sicuri che questi ragionamenti, così astratti e complessi, filino lisci? Qui entrano in gioco gli assistenti di prova come Isabelle/HOL. Pensateli come dei super-controllori logici computerizzati. Noi “traduciamo” gli assiomi e le definizioni di Gödel e Scott nel linguaggio formale di Isabelle/HOL (usando una tecnica chiamata *shallow embedding*, parte della metodologia LogiKEy, che permette di rappresentare la logica modale all’interno della logica classica d’ordine superiore) e poi chiediamo al sistema di verificare, passo dopo passo, se le conclusioni seguono davvero dalle premesse. Non solo: sistemi come Isabelle/HOL integrano anche dimostratori automatici (come Sledgehammer, che a sua volta chiama in causa “mastini” come Z3, CVC4, E, Vampire) e “cercatori di controesempi” (come Nitpick). Questo ci permette di fare esperimenti, testare varianti, scoprire sottigliezze e persino… trovare errori!

L’Argomento di Gödel del 1970: Sotto la Lente d’Ingrandimento

Vediamo più da vicino cosa diceva Gödel nel suo manoscritto del ’70. Il concetto chiave è quello di “proprietà positiva” (simbolo P). Gödel non definisce *quali* siano le proprietà positive, ma ne postula le caratteristiche tramite assiomi:

• Ax1: Se due proprietà e#x03C6; e e#x03C8; sono positive, anche la loro congiunzione (e#x03C6; e e#x03C8;) è positiva. (Gödel aggiunge una nota per estenderlo a infinite congiunzioni, e vedremo che è cruciale!)
• Ax2a: Una proprietà e#x03C6; è positiva se e solo se la sua negazione (~e#x03C6;) non lo è (o viceversa, in modo esclusivo).
• Ax2b: Se una proprietà è positiva, lo è *necessariamente* (e#x25A1;Pe#x03C6;).

Poi definisce:

• Dio (G): Un’entità x è simile a Dio (Gx) se possiede *tutte* le proprietà positive.
• Essenza (Ess.): Una proprietà e#x03C6; è un’essenza di x (e#x03C6; Ess. x) se x possiede e#x03C6; e *tutte* le altre proprietà e#x03C8; di x sono implicate *necessariamente* da e#x03C6; (questa implicazione necessaria, e#x03C6; e#x2283;_N e#x03C8;, significa e#x25A1;e#x2200;y(e#x03C6;y e#x2283; e#x03C8;y)).
• Esistenza Necessaria (E): Un’entità x ha esistenza necessaria (Ex) se tutte le sue essenze sono *necessariamente esemplificate* (cioè, è necessario che esista *qualcosa* con quella proprietà essenziale).

Infine, altri due assiomi:

• Ax3: L’esistenza necessaria (E) è una proprietà positiva.
• Ax4: Se e#x03C6; è positiva e e#x03C6; implica necessariamente e#x03C8;, allora anche e#x03C8; è positiva.

La Sorpresa: un’Inconsistenza Nascosta!

Gödel deriva alcuni teoremi intermedi, come Th1 (essere Dio è un’essenza di un essere divino) e Th2 (se esiste un essere divino, allora *necessariamente* esiste un essere divino). Da qui, usando la logica modale S5 (o in realtà basta la KB, che richiede solo la simmetria della relazione di accessibilità tra mondi possibili), deriva Th3: se è *possibile* che esista un essere divino (e#x25C7;e#x2203;x.Gx), allora è *necessario* che esista (e#x25A1;e#x2203;y.Gy).

Il passo cruciale mancante è dimostrare che l’esistenza di un essere divino è *almeno possibile*. Gödel pensava di averlo fatto con l’assioma Ax4. E qui… sorpresa! I nostri esperimenti con Isabelle/HOL (e in particolare il dimostratore automatico Leo-II) hanno confermato una scoperta precedente: gli assiomi originali di Gödel del 1970, così come sono scritti, sono inconsistenti! Portano a una contraddizione.

Dove sta il problema? Nella definizione di Essenza. Gödel *non* richiede esplicitamente che una proprietà essenziale e#x03C6; di x debba effettivamente valere per x (cioè e#x03C6;x). Questo permette alla “proprietà vuota” (e#x03BB;x.e#x22A5;, la proprietà che nessun oggetto possiede) di essere un’essenza di *qualsiasi* cosa. Ma la proprietà vuota non può essere positiva (per Ax2a e Ax4). D’altro canto, usando Ax3, Ax4 e la definizione di Esistenza Necessaria, si arriva a dimostrare che la proprietà vuota *dovrebbe* essere positiva. Contraddizione! Sembra che Gödel non se ne fosse accorto.

Come Salvare l’Argomento? Due Strade

Fortunatamente, l’inconsistenza si può risolvere facilmente in (almeno) due modi:

1. Modificare l’Essenza (la via di Scott): Basta aggiungere il requisito che mancava nella definizione di Essenza: e#x03C6; Ess. x se e#x03C6;x è vero E per ogni altra proprietà e#x03C8; di x, e#x03C6; implica necessariamente e#x03C8;. Questa è la modifica che Scott aveva introdotto, forse intuitivamente, nella sua versione. Con questa correzione, il sistema di assiomi diventa consistente (Nitpick trova un modello!).
2. Modificare l’Implicazione Necessaria: Un’altra strada, che abbiamo esplorato nei nostri esperimenti più recenti, è modificare la definizione di e#x03C6; e#x2283;_N e#x03C8;. Invece di e#x25A1;e#x2200;y(e#x03C6;y e#x2283; e#x03C8;y), potremmo usare e#x2200;y(e#x03C6;y e#x2283; e#x25A1;e#x03C8;y). Anche questa via porta a un sistema consistente, sebbene con alcune differenze interessanti nei modelli trovati da Nitpick.

Una volta resa consistente la base, per completare la prova serve ancora dimostrare la *possibilità* dell’esistenza divina (Th4: e#x25C7;e#x2203;x.Gx). Qui entra in gioco la nota di Gödel sull’estensione di Ax1 a infinite congiunzioni (che formalizziamo come Ax1Gen). Da Ax1Gen si deriva che la proprietà “essere Dio” (G) è essa stessa una proprietà positiva (Lemma L: P(G)). E da questo, con Ax2a e Ax4 (o A1Gen nella seconda variante), segue Th4.
Finalmente, combinando Th3 e Th4, otteniamo il risultato principale: Th5: e#x25A1;e#x2203;x.Gx. Ovvero: è necessario che esista un’entità simile a Dio. E tutto questo, verificato passo passo dal nostro fido Isabelle/HOL!

La Variante di Scott e Altre Considerazioni

La versione presentata da Scott è molto simile alla prima variante consistente di Gödel che abbiamo visto. Le differenze principali sono:

• Usa assiomi leggermente riformulati (A1-A5) ma logicamente equivalenti o molto vicini a quelli di Gödel (corretti).
• Assume direttamente come assioma (A3) che “essere Dio” è una proprietà positiva (P(G)), bypassando la necessità di Ax1Gen.
• Include fin da subito la definizione “corretta” di Essenza.

Anche la versione di Scott, ovviamente, risulta consistente e valida (sempre in logica KB o S5) secondo Isabelle/HOL.

Cosa succede se proviamo a usare logiche modali più deboli, come la logica K? L’argomento fallisce! Nitpick trova dei controesempi proprio all’ultimo passo (la derivazione di Th5/T3). Questo dimostra quanto la scelta della logica sottostante sia cruciale. E in logica S4? La questione è più sfumata e ancora aperta per alcune varianti.

Un’altra cosa interessante che emerge dagli assiomi (in tutte le varianti consistenti) è il cosiddetto collasso modale: e#x03C6; e#x2283; e#x25A1;e#x03C6;. Significa che tutto ciò che è vero, è *necessariamente* vero. Non c’è contingenza, il mondo non potrebbe essere diverso da com’è. Per molti è una conseguenza problematica, ma forse per Gödel, con la sua visione platonica e razionalista, era un risultato desiderato.

Inoltre, si dimostra che l’insieme delle proprietà positive forma una struttura matematica nota come ultrafiltro (non massimale). E segue anche il monoteismo: può esistere al massimo un’entità divina (due entità divine dovrebbero avere esattamente le stesse proprietà positive, e quindi coincidere per il principio di Leibniz).

E il Male? Potremmo definire un’entità “Malvagia” come colei che possiede tutte le proprietà *non-positive*? Con gli assiomi di Gödel/Scott, si dimostra che *necessariamente non esiste* un’entità simile. Per far “esistere” il Male in questo schema, dovremmo ribaltare completamente gli assiomi, postulando un concetto primitivo di “proprietà negativa”.

Riflessioni Finali: Una Prova di Dio o un Gioco Logico?

Allora, abbiamo “dimostrato” Dio con il computer? Calma! Quello che abbiamo fatto è stato verificare la correttezza logica dell’argomento: date certe premesse (assiomi e definizioni), la conclusione (l’esistenza necessaria di un’entità con quelle caratteristiche) segue in modo stringente all’interno di un certo sistema logico (HOML con semantica S5/KB).

La vera domanda diventa: sono convincenti le premesse? Crediamo davvero che esista un concetto di “proprietà positiva” con quelle caratteristiche? Che l’esistenza necessaria sia “positiva”? Che la definizione di “Dio” come possessore di tutte le proprietà positive catturi adeguatamente il concetto? Qui si entra nel campo della filosofia e della fede personale.

Gödel stesso credeva in una “filosofia e teologia scientifica (esatta)” basata su concetti astratti. Il suo argomento ontologico è forse il tentativo più estremo di realizzare questa visione. Il “Dio” che emerge da questi assiomi è un’entità massimamente astratta, razionale, le cui proprietà hanno una struttura matematica (ultrafiltro). È molto lontano dal Dio personale di molte religioni, ma forse era proprio questo che Gödel cercava.

Il nostro lavoro con Isabelle/HOL mostra la potenza di questi strumenti per analizzare, chiarire, e persino correggere argomenti metafisici complessi. Non danno la risposta finale sull’esistenza di Dio, ma ci aiutano a capire meglio la struttura logica del problema, i presupposti nascosti, le conseguenze inaspettate. È un esempio affascinante di come la logica formale e l’informatica possano gettare nuova luce su questioni antichissime. E chissà quali altre scoperte ci riserva il futuro, continuando a esplorare questi affascinanti territori di confine tra pensiero umano e rigore computazionale… come diceva Gödel, forse “esistono metodi sistematici per la soluzione di tutti i problemi”…

Fonte: Springer