Oui, enfin attention, il s'agit avant tout de logique modale. D'ailleurs les auteurs prennent soin de bémoliser le propos avec "selon les règles de logique"!
Ce que je comprends -et d'après ce qu'un éminent mathématicien de l'Université de Genève a tenté de me vulgariser- : Gödel a démontré qu'il y avait de l'indémontrable (le théorème d'incomplétude) et qu'il existait une "réalité" hors des modèles et des compréhensions mathématiques (La Preuve ontologique de Gödel) ...qui me semble tenir au moins autant de la figure réthorique que des mathématiques (voir axiomes içi). Gödel n'a jamais publié cette preuve ontologique de son vivant.
C'est pourtant cette dernière qui tend a être vérifiée depuis 2013 déjà grâce à la puissance de calcul informatique par Christoph Benzmüller et Bruno Woltzenlogel Paleo. (« Gödel's God in Isabelle/HOL », Archive of Formal Proofs, 2013). Ils se sont concentrés sur la version de Godel pour laquelle, jusqu'à présent, aucun prouveur de théorèmes en logique modale n'était disponible. En ce sens, l'expérience semble avoir donné des résultats positifs.
Le point de la preuve de Gödel est de dire que si quelque chose est possible, alors il existe nécessairement. Si le raisonnement peut être validé par l'informatique ( il s'agit encore une fois de logique modale!), il ne signifie pas qu'il soit "vrai" dans la réalité que nous expérimentons (même si elle reste encore à définir...). D'ailleurs les axiomes originaux rendraient aussitôt tout autre personnage imaginaire existant (licornes, elfes, trolls, fées ou que sais-je)!
Selon ce que j'en comprends, si cette définition de ce "Dieu mathématique" tend à être démontrée cela signifie simplement que celui qui "croit", rend sa croyance tangible dans le monde des "possibles" mathématiques.
Einstein préférait dire: "dites moi ce que vous entendez par Dieu et je vous dirai si j'y crois"...