Gödel, arguably the greatest logician of the 20th century, dreamed of establishing philosophical theses and ontological results with the rigour and precision of mathematics. His dream was to a remarkable extent fulfilled. Two modal principles that characterize properties of proof, time, and God reveal some intriguing logical interconnections among Gödel's Second Incompleteness Theorem, his argument for the unreality of time in the General Theory of Relativity, and his Ontological argument.