Some Completeness Results for Modal Predicate Calculi

  • Richmond H. Thomason
Part of the Synthese Library book series (SYLI, volume 29)


Two systems of first-order predicate calculus with identity, one of them with definite descriptions, will be formulated in this paper along with semantic interpretations, and then shown strongly complete by methods similar to those of Henkin [3]. These systems, Q1 and Q3,1 are generalizations of the systems presented in Kripke [6] and [8], respectively.2 An informal and philosophical account of Q1 and Q3 can be found in [11], together with a historical note concerning the development of the systems and their interpretation.


Modal Logic Intuitionistic Logic Definite Description Individual Constant Simultaneous Induction 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. [1]
    Church, A., Introduction to Mathematical Logic, vol. I, Princeton 1956.Google Scholar
  2. [2]
    Cocchiarella, N., Tense Logic: a Study of Temporal Reference. Dissertation, The University of California, Los Angeles, 1966.Google Scholar
  3. [3]
    Henkin, L., ‘The Completeness of the First-Order Functional Calculus’, Journal of Symbolic Logic 14 (1949) 159–166.CrossRefGoogle Scholar
  4. [4]
    Henkin, L., ‘A Generalization of the Concept of co-Completeness’, Journal of Symbolic Logic 22 (1957) 1–14.CrossRefGoogle Scholar
  5. [5]
    Hintikka, J., Knowledge and Belief. Ithaca, New York, 1962.Google Scholar
  6. [6]
    Kripke, S., ‘A Completeness Theorem in Modal Logic’,Journal of Symbolic Logic 24(1959) 1–14.CrossRefGoogle Scholar
  7. [7]
    Kripke, S., ‘Semantical Analysis of Modal Logic I: Normal Propositional Calculi’, Zeitschrift fur Mathematische Logik und Grundlagen der Mathematik 9 (1963) 67–96.CrossRefGoogle Scholar
  8. [8]
    Kripke, S., ‘Semantical Considerations on Modal and Intuitionistic Logic I’ in Proceedings of a Colloquium on Modal and Many-Valued Logics, Helsinki 1963, pp.83–94.Google Scholar
  9. [9]
    Kripke, S., ‘Semantical Analysis of Intuitionistic Logic I’ inFormal Systems and Recursive Functions (ed. by J. Crossley and M. Dummett), Amsterdam 1965, pp.92–130.CrossRefGoogle Scholar
  10. [10]
    Montague, R. and L. Henkin, ‘On the Definition of “Formal Deduction”’, Journal of Symbolic Logic 21 (1957) 129–136.Google Scholar
  11. [11]
    Stalnaker, R. and R. Thomason, ‘Abstraction in First-Order Modal Logic’, Theoria (Lund), 14 (1968) 203–207.Google Scholar
  12. [12]
    Thomason, R., ‘On the Strong Semantical Completeness of the Intuitionistic Predicate Calculus’, Journal of Symbolic Logic 33 (1968) 1–7.CrossRefGoogle Scholar
  13. [13]
    Thomason, R., ‘Modal Logic and Metaphysics’ in The Logical Way of Doing Things (ed. by K. Lambert), New Haven, Conn., 1969, pp. 119–146.Google Scholar
  14. [14]
    van Fraassen, B. and K. Lambert, ‘On Free Description Theory’, Zeitschrift fur Mathematische Logik und Grundlagen der Mathematik 13 (1967) 225–240.CrossRefGoogle Scholar


  1. 1.
    The system Q2 is discussed in Thomason [13], where a definition of Q2-validity is given. Prof. David Kaplan has informed me (in a private communication, April, 1967) that the notion of Q2-validity cannot be recursively axiomatized.Google Scholar
  2. 2.
    The system Q3 is a generalization of the version of modal predicate calculus described in Kripke [8], which treats only closed formulas, and hence gives no account of individual constants or definite descriptions. On the other hand, the system Q1S5 of modal predicate calculus based on an S5-type modality and on a Ql-type theory of quantification and identity is the system proved semantically complete in Kripke [6]. In this case our generalization of Kripke’s results consists in allowing for sorts of modality other than S5, and in proving strong rather than weak completeness.Google Scholar
  3. 3.
    We will use dots in the usual way in place of parentheses; see Church [1], pp. 74–80.Google Scholar
  4. 4.
    This proof requires that the morphology (i.e. the set of formulas of the morphology) be denumerable.Google Scholar
  5. 5.
    See the articles of Kripke, especially [7] and [8], for an intuitive account of this semantics. Another discussion of this sort may be found in Thomason [13].Google Scholar
  6. 6.
    The requirement that the domains be nonempty is easily lifted; in this case, one must also drop A6’ from the system Q3.Google Scholar
  7. 7.
    This is the only place in the proof of semantic completeness which must be changed to adjust the argument to kinds of modality other than S4.Google Scholar
  8. 8.
    The rules R4—R7 are needed for the proof of semantic completeness of Q3. At present, it is not known whether these rules are redundant.Google Scholar
  9. 9.
    We will use individual variables for instantiation rather than individual constants, as is usual in versions of Henkin’s proof and as we ourselves have done in the case of Ql. The underlying reason for this is semantic; in Q3, individual constants and individual variables are wholly different. Whereas variables range over things (i.e. things-as- identified-across worlds), constants need not be assigned one thing; they may name different things in different worlds.Google Scholar
  10. 10.
    The proof we give of this lemma makes use of our assumption that the morphology is denumerable.Google Scholar
  11. 11.
    This can be made more precise by adding to the definition of a Q3-interpretation on < K, R, D, D’ > an auxiliary function which selects for each definite description 1 x A and member α of K an element of D—D α a to be assigned to 1 x A in case the uniqueexistence condition fails.Google Scholar
  12. 12.
    Our account of descriptions differs only in minor respects from the theory given in van Fraassen and Lambert [14] of the system FD.Google Scholar
  13. 13.
    A version of T4 is established in Cocchiarella [2] by means of semantic tableaux, for a system of modal predicate calculus with tense-operators. When a connective corresponding to necessity is defined in terms of these operators a system equivalent to our Q3 is obtained. Cocchiarella later proved a compactness theorem for his system, which together with his weak completeness theorem yields a result implying our T3. This, however, has not yet appeared in print.Google Scholar
  14. The results appearing in the present paper are, to my knowledge, the first Henkinstyle completeness proofs for systems such as Q3. As I see it, the principal advantage of these results is their flexibility. They are very easy to adapt to other systems, especially to ones obtained by extending the language of Q3. For an example of such an application, see Stalnaker and Thomason [11].Google Scholar

Copyright information

© D. Reidel Publishing Company, Dordrecht, Holland 1970

Authors and Affiliations

  • Richmond H. Thomason
    • 1
  1. 1.Yale UniversityUSA

Personalised recommendations