Types, Tableaus, and Gödels God

The book delves into Gödel's modal ontological argument within the framework of intensional logic. It begins with a semantic presentation of classical type theory and introduces tableau rules, culminating in a completeness proof. The discussion expands to include modal logic, exploring concepts like extensionality and identity. Various ontological proofs for God's existence are examined, leading to a formalization of Gödel's argument. The author critiques objections, particularly Sobel's challenge regarding Gödel's assumptions, emphasizing the distinction between intensional and extensional interpretations of properties.