la prova di (metà) Tao

"Ogni proprietà positiva è necessariamente positiva.
Per definizione Dio ha tutte e solo le proprietà positive.
L'esistenza necessaria è una proprietà positiva.
Quindi Dio, se è possibile, possiede necessariamente l'esistenza.
Il sistema di tutte le proprietà positive è compatibile.
Quindi Dio è possibile.
Essendo possibile, Dio esiste necessariamente"

T3 Necessarily, God - G(x) - exists:   ∃xG(x)

Gödel’s proof is challenging to formalize and verify because it requires an expressive logical language with modal operators (possibly and necessarily) and with quantifiers for individuals and properties. Our computer-assisted formalizations rely on an embedding of the modal logic into classical higher-order logic with Henkin semantics. The formalization is thus essentially done in classical higher-order logic where quantified modal logic is emulated.

In our ongoing computer-assisted study of Gödel’s proof we have obtained the following results:

– The basic modal logic K is sufficient for proving T1, C and T2.

– Modal logic S5 is not needed for proving T3; the logic KB is sufficient.

– Without the first conjunct Φ(x) in D2 the set of axioms and definitions would be inconsistent.

– For proving theorem T1, only the left to right direction of axiom A1 is needed. However, the backward direction of A1 is required for proving T2.

This work attests the maturity of contemporary interactive and automated deduction tools for classical higher-order logic and demonstrates the elegance and practical relevance of the embeddings-based approach. Most importantly, our work opens new perspectives for a computer-assisted theoretical philosophy. The critical discussion of the underlying concepts, definitions and axioms remains a human responsibility, but the computer can assist in building and checking rigorously correct logical arguments. In case of logico-philosophical disputes, the computer can check the disputing arguments and partially fulfill Leibniz’ dictum: Calculemus — Let us calculate!

Raimondo Lullo, Prova logica dell'esistenza di Dio, XIII secolo.

Christoph Benzmüller

Bruno Woltzenlogel Paleo