Gödel's ontological proof is a formal argument for God's existence by the mathematician Kurt Gödel. Can someone please explain what those symbols are, and explain the proof? Thanks.
Does it prove both existence and uniqueness ?
The modal operator $\square$ refers to necessity; its dual, $\lozenge$, refers to possibility. (A sentence is necessarily true iff it isn't possible for it to be false, and vice versa.) $P(\varphi)$ means that $\varphi$ is a positive (in the sense of "good") property; I'll just transcribe it as "$\varphi$ is good". I'll write out the argument colloquially, with the loss of precision that implies. In particular, the words "possible" and "necessary" are vague, and you need to understand modal logic somewhat to follow their precise usage in this argument.
Proof of Theorem $1$: Suppose $\varphi$ were good, but necessarily nothing had property $\varphi$. Then property $\varphi$ would, vacuously, force every other property; in particular $\varphi$ would force $\neg\varphi$. By Axiom $1$, this would mean that $\neg\varphi$ was also good; but this would then contradict Axiom $2$.
Proof of Theorem $2$: This follows directly from Theorem $1$ applied to Axiom $3$.
Proof of Theorem $3$: First note that if $x$ is godlike, it has all good properties (by definition) and no bad properties (by Axiom $2$). So any property that a godlike thing has is good, and is therefore necessarily good (by Axiom $4$), and is therefore necessarily possessed by anything godlike.
Proof of Theorem $4$: If something is godlike, it has every good property by definition. In particular, it's indispensable, since that's a good property (by Axiom $5$); so by definition something with its essence, which is just "being godlike" (by Theorem $3$), must exist. In other words, if something godlike exists, then it's necessary for something godlike to exist. But by Theorem $2$, it's possible that something godlike exists; so it's possible that it's necessary for something godlike to exist; and so it is, in fact, necessary for something godlike to exist. QED.
The box is a modal operator (it is necessarily true that ...), with the diamond its dual (it is possibly true that ...). '$P(\varphi)$' holds when the property expressed by $\varphi$ is 'positive' (maybe better, is a perfection). Other novelties are defined. $G(x)$ says $x$ has all perfections (so is God). $\varphi$ ess $x$ says the property $\varphi$ is the essence of $x$. $E$ is the property of necessary existence (existence in virtue of your essence). [Don't blame me, I'm just reporting ....]
You'll find out just a little more about Gödel's very strange apparent aberration here: http://plato.stanford.edu/entries/ontological-arguments/#GodOntArg
Robert Adams introduction to Gödel's original note in Kurt Gödel: Collected Works. Vol III, Unpublished Essays and Lectures is well worth reading.
Petr Hajek has an amazingly patient exploration of the current state of play in investigations of Gödel's Ontological Proof and its variants in Matthias Baaz et al. (eds) Kurt Gödel and the Foundations of Mathematics (CUP 2011). But I can't say that this changed my impression that this is little more than a curious side note in logic.