Types, tableaus, and Gödel's God (Q1406610)

This short book consists of three parts. Part one is an exposition of Henkin semantics for the classical simple theory of types (with or without extensionality) and a cut-elimination proof by extending semi-valuations to total valuations. Part two provides an extension to the modal systems K and S5 in terms of modal tableaux prefixed by worlds. Soundness, completeness and cut elimination are claimed to be elaborations of arguments given earlier for classical logics. They are ``left as a huge exercise''. A short chapter treats equality, de re and de dicto modalities, rigidity, definite descriptions and choice functions in a higher-order modal context. Part three is devoted to Gödel's ontological argument. This one-page informal sketch by Gödel, probably not intended for publication, generated considerable literature. A brief history and analysis of ontological arguments by Anselm, Descartes and Leibniz is given in Chapter 10, followed by a detailed analysis and criticism of Gödel's argument. The author repeats a claim by J. Sobel that the modal system used by Gödel collapses, and explores some ways out. Another flaw in Gödel's argument is an assumed axiom that is directly equivalent to a key conclusion: Gödel's assumption that the family of positive properties is closed under conjunction is equivalent to the possibility of God's existence. The author traces this observation to D. Scott and J. Sobel. There is a very short summary of work by P. Hájek.