# Applying Second-Order Quantifier Elimination in Inspecting G"odel's Ontological Proof

arXiv: https://arxiv.org/abs/2110.11108 · HTML: https://mlsanity.com/paper/2110.11108/

## Key facts

- No citing papers in the map yet (data through 14 Oct 2026).
- Builds on 4 of its 33 references that are in the map.
- First posted on arXiv 21 Oct 2021.

## Builds on (most cited first, 4 of 4)

- [Facets of the PIE Environment for Proving, Interpolating and Eliminating on the Basis of First-Order Logic](https://mlsanity.com/paper/2002.10892/) (2020)
- [Formalization, Mechanization and Automation of G"odel's Proof of God's Existence](https://mlsanity.com/paper/1308.4526/) (2013)
- [Computer Science and Metaphysics: A Cross-Fertilization](https://mlsanity.com/paper/1905.00787/) (2019)
- [A (Simplified) Supreme Being Necessarily Exists, says the Computer: Computationally Explored Variants of G"odel's Ontological Argument](https://mlsanity.com/paper/2001.04701/) (2020)

## Abstract (arXiv)

In recent years, G"odel's ontological proof and variations of it were formalized and analyzed with automated tools in various ways. We supplement these analyses with a modeling in an automated environment based on first-order logic extended by predicate quantification. Formula macros are used to structure complex formulas and tasks. The analysis is presented as a generated type-set document where informal explanations are interspersed with pretty-printed formulas and outputs of reasoners for first-order theorem proving and second-order quantifier elimination. Previously unnoticed or obscured aspects and details of G"odel's proof become apparent. Practical application possibilities of second-order quantifier elimination are shown and the encountered elimination tasks may serve as benchmarks.