A new small emendation of Gödel's ontological proof (Q1612687)

This paper initially formulates a formal modal system (called by the author \(AO'_{^0})\) in which the necessary existence of a godlike being can be proved and then characterizes two additional modal systems (viz. \(AOE_0'\), \(AOE_0'')\) that can prove the necessary actual existence of such a being. System \(AO_0'\) constitutes an extension of the two-sorted predicate modal logic S5 (the sorts involved in this logic being individuals and properties). In detail, apart from the costumary axiom set and rules for the aforesaid modal logic, the formal system contains axioms for equality of individuals and properties, an axiom of extensionality for properties, a modal comprehension schema for (monadic) properties, axioms for a monadic predicate constant of the sort of properties (intuitively interpreted as ``the property \(X\) is positive'') and a definition of a predicate constant \(H\) of the sort of individuals (intuitively interpreted as \(``x\) is a godlike being''). In order to take into account the possibility that the set of (actually) existing individuals varies from one possible world to another, the author introduces the system \(AOE_0'\). This system is like \(AO_0'\) except for the addition to the logical syntax of a monadic predicate of existence of individuals, a redefinition of ``\(H\)'' (in which the existence predicate plays a role) and the addition to the axiomatic basis of the background logic of an axiom demanding non-emptiness of the domain of discourse corresponding to every possible world. System \(AOE_0''\) is just a subsystem of \(AOE_0'\) equivalent to it. \(AO_0'\) intends to be an emendation to a formal system, originally formulated by Kurt Gödel, in which the necessary existence of godlike creature can be proved but in which modalities collapse. As the author points out, several attempts have been made to avoid this problem. The author's construction of \(AO_0'\) (as well as that one of \(AOE_0'\) and \(AOE_0'')\) should be viewed in this line of research and it follows a path of solution not previously explored.