Se il computer impara la teologia

In queste settimane la presentazione, in una importante conferenza scientifica mondiale, da parte di alcuni ricercatori di Google del sistema di gestione della conoscenza Knowledge Vault ha richiamato l’attenzione sia dei giornali specialistici sia di quelli popolari. Quasi sicuramente l’attenzione mediatica su questo sistema nasce dal fatto che il proponente è il colosso Google che in quanto a sistemi di gestioni di dati non è secondo a nessuno. Infatti, di per sé i sistemi informatici per la gestione della conoscenza (knowledge management systems) sono noti da qualche decennio e quindi non rappresentano una vera novità scientifica e tecnologica. Semmai la novità sta nel fatto che Google abbia deciso di adottare questa tecnologia che finora sembrava non gli interessasse. Se a questo interesse si associa il fatto che la conoscenza da gestire viene estratta dai dati disponibili e quelli che Google può avere a disposizione sono immensamente grandi, si può comprendere l’attenzione e l’allarme che la presentazione di Knowledge Vault abbia potuto generare.

Eppure, ci sono risultati scientifici che meriterebbero la stessa attenzione e anche maggiore curiosità degli specialisti e del pubblico non addetto ai lavori. Purtroppo però molti di queste ricerche non suscitano l’interesse della stampa e delle televisioni perché non hanno sponsor importanti come Google o perché non hanno un impatto economico simile a quello che potrebbero avere sistemi come Knowledge Vault.

Uno di questi risultati a cui ci piace accennare è stato presentato qualche tempo fa da Paul Oppenheimer e Edward Zalta, i quali hanno usato un software che implementa un dimostratore automatico di teoremi, PROVER9, per validare la prova ontologica di Anselmo d’Aosta. La questione affrontata Anselmo, teologo di grande valore, è una di quelle con cui gli esseri umani si sono sempre confrontati e sulla quale hanno ragionato le menti più eccelse che l’umanità abbia avuto: la prova dell’esistenza di Dio. Il monaco e teologo medievale riteneva di aver trovato una argomentazione per provare l’esistenza di Dio basata sul fatto che “Dio è l’essere di cui non si può pensare nulla di più grande”. Lui l’ha quindi sviluppata tramite una dimostrazione logica per assurdo, cioè  assumendo una tesi opposta a quella che voleva dimostrare e arrivando ad una conclusione impossibile o, appunto, assurda, che quindi conferma la tesi iniziale.

Noi naturalmente non pensiamo, neanche lontanamente, di affrontare la sfida della prova ontologica di Anselmo, ne di analizzare come altri grandi pensatori (Tommaso d’Aquino, Cartesio, Kant e i grandi logici del Novecento) hanno criticato la prova di Anselmo d’Aosta o ne abbiamo proposto delle altre. Ci limitiamo molto semplicemente a far osservare che Oppenheimer e Zalta all’Università di Stanford, usando un semplice programma software che aiuta i ricercatori nella dimostrazione di teoremi (PROVER9 costruisce dimostrazioni matematiche a partire da una serie di assiomi), hanno rappresentato le ipotesi e la conclusione usate da Anselmo nella sua opera teologica Proslogion. Usando il linguaggio di PROVER9 e il suo sistema di elaborazione, questo software ha dimostrato la correttezza dell’argomentazione definita dal monaco medievale. Inoltre, PROVER9 ha chiarito che è possibile semplificare l’argomentazione proposta circa mille anni fa da Anselmo, passando dalle tre premesse usate nella formulazione originale ad una soltanto, sufficiente a dimostrare la correttezza di quel processo logico. 

La ricerca di Oppenheimer e Zalta ha mostrato come i calcolatori e i sistemi software basati sulla logica matematica possono essere usati efficacemente anche nello studio della metafisica, semplificando problemi complessi come quello della prova ontologica. L’esperimento fatto dai due docenti di filosofia a Stanford è uno dei tanti esempi di problemi affrontati da una disciplina che va sotto il nome di teologia computazionale. Disciplina che certamente potrà apparire astrusa, fumosa e forse inutile, eppure sta lì a dimostrare come l’uso di strumenti sofisticati di calcolo permette di affrontare i problemi più vari (anche quelli che ci può essere difficile immaginare) e i temi più spinosi e complessi che l’uomo ha sempre avuto di fronte e che ha studiato e studierà non soltanto per spirito utilitaristico, ma semplicemente per desiderio di conoscenza.