  Three variants of Kurt G\"odel's ontological argument, proposed by Dana
Scott, C. Anthony Anderson and Melvin Fitting, are encoded and rigorously
assessed on the computer. In contrast to Scott's version of G\"odel's argument
the two variants contributed by Anderson and Fitting avoid modal collapse.
Although they appear quite different on a cursory reading they are in fact
closely related. This has been revealed in the computer-supported formal
analysis presented in this article. Key to our formal analysis is the
utilization of suitably adapted notions of (modal) ultrafilters, and a careful
distinction between extensions and intensions of positive properties.
