Types, Tableaus, and Gödel’s God
Fitting (Melvin)
This Page provides (where held) the Abstract of the above Book and those of all the Papers contained in it.


Author’s Introduction

  1. This is a book about intensional logic. It also provides a thorough look at higher-type classical logic, including tableaus and a completeness proof for them. It also provides a formal examination of the Godel ontological argument. These are not disparate topics. Higher-type classical logic is intensional logic with the intensional features removed, so this is a good place to start. Ontological arguments, Godel's in particular, are natural examples of intensional logic at work, so this is a good place to finish.
  2. The term formal logic covers a broad range of inventions. At one end are small, special-purpose systems; at the other are rich, expressive ones. Higher-type modal logic1 - intensional logic - is one of the rich ones. Originating with Carnap and Montague, it has been applied to provide a semantics for natural language, to model intensional notions, and to treat long-standing philosophical problems. Recently it has also supplied a semantic foundation for some complex database systems. But besides being rich and expressive, it is also tremendously complex, and requires patience and sympathy on the part of its students.
  3. There are two quite different reasons to be interested in a logic. There is its formal machinery for its own sake, and there is using the formal machinery to address problems from the outside world. The mechanism of higher-type modal logic2 is complex and requires serious mathematics to develop properly. Models are not simple to define, and tableau systems are quite elaborate. A completeness argument, to connect the two, is difficult. But, the machinery is of considerable interest, if this is the sort of thing you have a considerable interest in. If you are such a reader, applications concerning the existence of God can simply be skipped. On the other hand, if philosophical applications are what you are after, the Godel ontological argument is a prime example. If this is the kind of reader you are, much of the mathematical background can be taken on faith, so to speak. It is a rare reader who will be interested equally in both the formal and the applied aspects of intensional logic. In a sense, then, this book has no audience-there are separate audiences for different parts of it . (But I encourage these audiences to do some 'crossing over.')
  4. If you are interested in ontological arguments for their own sakes, start with Part III, and pick up material from earlier chapters as it is needed. If you are interested in the mathematical details of the formal system, its semantics and its proof theory, Parts I and II will be of interest-you can skimp on reading Part III. Part I is entirely devoted to classical logic, and Part II to modal3. Here is a more detailed summary. Part I presents higher-type classical logic. It begins with a discussion of syntax matters, Chapter 1. I present types in Schutte's style, rather than following Church. Types can be somewhat daunting and I've tried to make things go as smoothly as I can.
  5. Chapter 2 examines semantics in considerable detail. What are sometimes called "true" higher-order models are presented first. After this, Henkin's generalization is given, and finally a non-extensional version of Henkin models is defined. Henkin himself mentioned such models, but knowledge of them does not seem to be widespread. They are natural, and should become more familiar to the logic community-the philosophical logic community in particular.
  6. Classical higher-order tableaus are formulated in Chapter 3. These are not original here-versions can be found in several places. A number of worked out examples of tableau proofs are given, and more are in exercises. The system is best understood if used. I do not attempt a consideration of automation - the system is designed entirely for human application. There is even some discussion of why.
  7. Soundness and completeness are proved in Chapter 4. Tableaus are complete with respect to non-extensional Henkin models. The completeness argument is not original; it is, however, intricate, and detailed proofs are scarce in the literature.
  8. After the hard work has been done, equality and extensionality are easy to add using axioms, and this is done in Chapters 5 and 6. And this concludes Part I. Except for the explicit formulation of non-extensional models, the material in Part I is not original.
  9. Part II is devoted to the complications that modality4 brings. Chapter 7 adds the usual box and diamond to the syntax, and possible worlds to the semantics. It is now that choices must be made, since quantified modal logic5 is not a thing, but a multitude.
  10. First, at ground level quantifiers could be actualist or possibilist they can range over what actually exists at a world, or over what might exist. This corresponds to the varying domain, constant domain split familiar to many from first-order modal6 discussions. However, either an actualist or a possibilist approach can simulate the other. I opt for a possibilist approach, with an explicit existence predicate, because it is technically simpler.
  11. Next, we must go up the ladder of higher types. Doing so extensionally, as in classical logic, means we take subsets of the ground-level domain, subsets of these, and so on. Going up intensionally, as Montague did, means we introduce functions from possible worlds to sets of groundlevel objects, functions from possible worlds to sets of such things, and so on. What is presented here mixes the two notions-both extensional and intensional objects are present. I refer you [elsewhere] for applications of these ideas to database theory - intensional and extensional objects make natural sense even in such a context.
  12. Classical tableau rules are adapted in Chapter 8, using prefixes, to produce modal7 systems. While the modal8 tableau rules are rather straightforward, they are new to the literature, and should be of interest . Since things are already quite complex, no completeness proof is given. If it were given, it would be a direct extension of the classical proof of Part 1. Using modal9 semantics and tableaus, in Chapter 9 I discuss the relationships between rigidity, de re and de dicto usages, and what I call Godel's stability conditions, which arise in his proof of the existence of God. I also relate all this to definite descriptions. While this is not deep material, much of it does not seem to have been noted before, and many should find it of some significance.
  13. Finally, Part III is devoted to ontological proofs. Chapter 10 gives a brief history and analysis of arguments of Anselm, Descartes, and Leibniz. This is followed by a longer, still informal, presentation of the Godel argument itself. Formal methods are applied in Chapter 11, where Godel's proof is examined in great detail. While Godel's argument is formally correct, some fundamental flaws are pointed out. One, noted by Sobel, is that it is too strong-the modal10 system collapses. This could be seen as showing that free will is incompatible with Godel's assumptions. Some ways out of this are explored. Another flaw is equally serious: Godel assumes as an axiom something directly equivalent to a key conclusion of his argument. The problematic axiom is related to a principle Leibniz proposed as a way of dealing with a hole he found in an ontological proof of Descartes. Descartes, Leibniz, and Godel (and also Anselm) all have proofs that stick at the same point: showing that the existence of God is possible.
  14. If the Godel argument is what you are interested in, start with Part III, and pick up earlier material as needed. Many of the uses of the formalism are relatively intuitive. Indeed, in Godel’s notes on his ontological argument, formal machinery is never discussed, yet it is possible to get a sense of what it is about anyway.

  • Springer Academic Publishers, 2002
  • Downloaded during Springer promotion, Dec. 2015

Text Colour Conventions (see disclaimer)
  1. Blue: Text by me; © Theo Todman, 2019
  2. Mauve: Text by correspondent(s) or other author(s); © the author(s)

© Theo Todman, June 2007 - March 2019. Please address any comments on this page to theo@theotodman.com. File output:
Website Maintenance Dashboard
Return to Top of this Page Return to Theo Todman's Philosophy Page Return to Theo Todman's Home Page