Variants of Godel's Ontological Proof in a Natural Deduction Calculus

This paper presents detailed formalizations of ontological arguments in a simple modal natural deduction calculus. The first formal proof closely follows the hints in Scott's manuscript about Godel's argument and fills in the gaps, thus verifying its correctness. The second formal proof improves the first one, by relying on the weaker modal logic KB instead of S5 and by avoiding the equality relation. The second proof is also technically shorter than the first one, because it eliminates unnecessary detours and uses Axiom 1 for the positivity of properties only once. The third and fourth proofs formalize, respectively, Anderson's and Bjordal's variants of the ontological argument, which are known to be immune to modal collapse.