Melvin Fitting
Types, tableaus and Gödel's god.
Kluwer Academic Pub., Norwell, MA, 2002.

ACM CR Categories: F.4.1 Mathematical logic - Modal logic (P)

At one level, this book extends the study of first-order modal logic, by Fitting and Mendelsohn (Kluwer, 1998), to higher order modal logic. Many examples, like the President of the United States who is 50 years old, the King of France who is bald, and the distinction between de re and de dicto modalities, make their reappearance in this book.

At another level, the book presents a clear treatment of higher order classical logic in the manner of Henkin, with examples like Cantor's theorem and the Knaster-Tarski theorem. Computer scientists might find the coverage of the subject matter more appealing here than what is usually found in introductory books on programming language semantics. Even more impressive, this clarity extends to higher-order logic with modalities, where previously we have only had the dense text of Montague's intensional type theory.

But what I like best about this book is its selling example. A few years before his death, the logician Kurt Gödel came up with a formal argument for the existence of a deity. The proofs are formally stated in this book, and examined as logical arguments from assumptions. A simple exercise shows, for example, that under Gödel's assumptions, the deity must be unique. Before this divine exercise, the book presents ontological arguments, criticism of Gödel's argument, counter-arguments, and assumptions. In short, this is the stuff of which philosophy is made. I was intrigued enough to wonder how the ontological arguments might be weakened to allow for a multiplicity of deities, such as those in Indian philosophies.