Marco Trainito precisa: «Nel libro Il diavolo in cattedra Odifreddi sostiene che la prova di Anselmo abbia la struttura logica di un particolare tipo di Reductio ad absurdum nota come Consequentia mirabilis. Nel mio saggio, invece, io ho sostenuto, sulla base di una lettura puntuale del passo relativo del Proslogion, che la prova di Anselmo ha la forma di una Reductio ad absurdum che non è una Consequentia mirabilis. Odifreddi ha letto il mio saggio grazie a Ivana Niccolai, la quale è stata così gentile da pubblicarlo nel sito Maecla (cui collabora) e da mandarglielo per un parere. Odifreddi le ha risposto immediatamente e ne è nato il seguente scambio di e-mail, per la cui retta comprensione è indispensabile la lettura del terzo paragrafo del mio saggio Analisi logiche delle prove dell’esistenza di Dio. Russell, Gödel e Odifreddi su Cartesio, Leibniz e Anselmo .»
Con l'autorizzazione dei gentilissimi Piergiorgio Odifreddi e Marco Trainito, che la Redazione di Maecla ringrazia sentitamente, viene pubblicato il seguente scambio di e-mail tra i due professori:

Piergiorgio Odifreddi, 3-9-07

Ho dato uno sguardo all'articolo di Trainito, e posso soltanto dire che:
1) È inutile continuare a formulare la prova di Gödel nel linguaggio della logica modale, perché si è dimostrato in seguito che il suo sistema modale collassa, e dunque le modalita' diventano inutili.
2) A proposito del mio "duplice errore", posso solo dire che: primo, l'osservazione che la prova di Anselmo è "di scarso successo" si riferiva non alla struttura logica dell'argomento (nel qual caso avrei parlato di correttezza), ma alla sua capacità di convinzione, che è per l'appunto nulla (nel senso che chi non crede, certo non sarà invogliato a credere da un argomento del genere); e, secondo, che una dimostrazione può procedere per argomento mirabile, o più in generale per contraddizione, anche se essa stessa non è formalizzabile nel calcolo proposizionale!
Ad esempio, la dimostrazione di Wiles è una tipica dimostrazione per assurdo (supponiamo che esistano soluzioni dell'equazione di Fermat, e facciamo vedere che questo produce una contraddizione), benché essa sia ovviamente non formalizzabile non soltanto nella logica proposizionale, ma nemmeno in quella del prim'ordine.
Trainito sembra fraintendere il fatto che uno schema sia proposizionale, con il fatto che una dimostrazione che segue quello schema debba esserlo anch'essa.
A presto!
Pg

Marco Trainito, 4-9-07
Carissima Ivana,
avevi ragione: Odifreddi è una persona davvero disponibilissima e gentilissima se lancia un feedback in così breve tempo, per giunta per una cosa sicuramente non piacevolissima!
Ho letto le sue parole di replica con una certa emozione e con un certo disagio, perché temo che lui abbia pensato di rispondere a un teologo! Forse dal mio scritterello non si evince abbastanza chiaramente che io sono radicalmente ateo come lui (non a caso sono un suo lettore appassionato), ma la parte finale accenna alla sede (il quadro metafisico di sfondo) in cui cercare gli errori delle prove ontologiche.
Cerco di replicare punto per punto, anche se temo che Odifreddi non abbia risposto al punto-chiave della mia obiezione e abbia invece detto delle cose (peraltro interessanti) su questioni laterali.
1) È inutile continuare a formulare la prova di Gödel nel linguaggio della logica modale, perché si e' dimostrato in seguito che il suo sistema modale collassa, e dunque le modalità diventano inutili.
Questo Odifreddi lo dice anche nel saggio stampato nel volume che contiene la prova di Gödel, e si può essere d'accordo. Ma io formulavo la prova di Gödel esattamente come la propone Gödel perché quella parte del mio saggio è puramente descrittiva. Essendo specializzato in storia delle idee, è mia abitudine dare innanzi tutto la parola all'autore quando si tratta di esporre per la prima volta il suo pensiero. In seguito uno può fare quello che vuole. Lo stesso Odifreddi può ristampare delle pagine critiche in quel volumetto perché c'è già un saggio (quello di Adams) in cui la prova di Gödel è esposta così come l'ha formulata Gödel (cioè in termini modali). Nel mio saggio, si suppone semplicemente che il Lettore Modello non conosca dettagliatamente la prova di Goedel...
2) A proposito del mio "duplice errore", posso solo dire che: primo, l'osservazione che la prova di Anselmo è "di scarso successo" si riferiva non alla struttura logica dell'argomento (nel qual caso avrei parlato di correttezza), ma alla sua capacità di convinzione, che è per l'appunto nulla (nel senso che chi non crede, certo non sarà invogliato a credere da un argomento del genere); e, secondo, che una dimostrazione può procedere per argomento mirabile, o più in generale per contraddizione, anche se essa stessa non è formalizzabile nel calcolo proposizionale!
Sul punto primo, rimando a quanto ho già detto: spero che Odifreddi non pensi che io sia stato convinto da Anselmo!
Il punto secondo lo capisco in linea di principio e naturalmente lo condivido, ma non riesco a capire come possa riguardare la mia obiezione. Io sostenevo che, schematizzandola in questa forma: "Se Dio non esiste, allora esiste; dunque esiste", Odifreddi impoverisca la complessità della prova di Anselmo, sia perché la assimila a un argomento mirabile (e invece secondo me non lo è, perché la sua forma sarebbe piuttosto qualcosa come: "Se Dio non esiste, allora Dio non è Dio; dunque, Dio esiste"), sia perché non tiene conto del fatto che essa richiede un linguaggio del primo ordine, dato che vi entrano in gioco proprietà ben precise strettamente legate tra loro da rapporti interni di implicazione (l'essere ciò di cui non si può pensare il maggiore, l'esistere in re e l'esistere in intellectu). Il punto essenziale è: la prova di Anselmo è non è una Consequentia mirabilis? Odifreddi sostiene di sì, senza fornire riferimenti testuali al Proslogion. Io sostengo di no, ripercorrendo i passi argomentativi di Anselmo direttamente sul testo. Su questo, mi pare, Odifreddi non ha risposto.
Ad esempio, la dimostrazione di Wiles è una tipica dimostrazione per assurdo (supponiamo che esistano soluzioni dell'equazione di Fermat, e facciamo vedere che questo produce una contraddizione), benché essa sia ovviamente non formalizzabile non soltanto nella logica proposizionale, ma nemmeno in quella del prim'ordine.
Perfettamante chiaro. Ma non c'entra con la mia obiezione.
Trainito sembra fraintendere il fatto che uno schema sia proposizionale, con il fatto che una dimostrazione che segue quello schema debba esserlo anch'essa.
Ho riflettuto molto su questo passo così ellittico e sono arrivato alla conclusione che probabilmente sono perfettamente in grado di cadere in questo fraintendimento, visto che la mia competenza nella logica della dimostrazione non è stellare (sono non un professionista ma un lettore appassionato di manuali di logica, da quello di Carnap a quello di Odifreddi, passando per quelli di Copi, Lemmon e Mondadori-D'Agostino). Tuttavia non riesco assolutamente ad afferrare il nesso tra questo fatto e la mia obiezione precisa di cui sopra.
P.S. Se puoi, chiedigli il permesso di rendere noto in FOR questo scambio, perché mi pare interessante. Da popperiano incallito, sarei felicissimo di scoprire e comprendere il mio errore, se c'è.
Ciao
M. Trainito

Piergiorgio Odifreddi, 4-9-07

Cara Ivana,
d'accordo su tutto, direi. Anche sulla formalizzazione di Trainito della prova di Anselmo. Ma, se posso ribattere, anche la mia non mi sembra scorretta. Il fatto è che un argomento informale non ha necessariamente una sola formalizzazione corretta. La cosa è tipica: ad esempio, succede giaà per la dimostrazione di Euclide dell'esistenza di infiniti numeri primi, che si può formulare in maniera sia costruttiva (dato un numero, al più entro il suo fattoriale più uno si trova un nuovo numero primo) che non (supponendo che ci sia un massimo numero primo, si trova una contraddizione dal fatto che entro il suo fattoriale più uno ce n'è uno nuovo).
A presto. E naturalmente, rendete pure noto lo scambio, se può interessare a qualcuno.
Cordialmente
Pg