There is a known old argument in St. Anslem, Leibnitz and Gödel for that in a pantheistic picture. Gödel adopted higher order modal logic, and factors the quest

There is a known old argument in St. Anslem, Leibnitz and Gödel for that in a pantheistic picture. Gödel adopted higher order modal logic, and factors the question via the axiom 'if possible then actual' (god/reality existence). I'm now pleased to discover that in 2017 someone has went through the pains of porting the thing to a proof verifier, Isabelle/HOL (they start from Melvin Fitting reconstruction of the idea in 1999). [1] https://www.researchgate.net/publication/317956529_Types_Tableaus_and_Godel's_God_in_IsabelleHOL https://www.researchgate.net/publication/317956529_Types_Tab...