Truth-Value Semantics for the Theory of Types

  • H. Leblanc
  • R. K. Meyer
Part of the Synthese Library book series (SYLI, volume 29)


Gödel showed in 1931 that the valid wffs of T, the simple theory of types, outrun the theorems of T, and in fact cannot but outrun them. It was to be almost two decades before Henkin supplied a semantic characterization of these theorems, when he showed in [5] that a wff A of T is provable in T if and only if A is what he calledvalid in the general sense or what we shall call generally valid. Further semantic characterizations of provability in T then came in rapid succession, among them Hintikka [7] and Schütte [12]. Both of these dispense with Henkin’s general models, the former using general model sets, the latter total valuations.


Alphabetical Order Parametric Extension Semantic Characterization Extensionality Axiom Simple Type Theory 
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]
    E. W. Beth, The Foundations of Mathematics, Amsterdam 1959.Google Scholar
  2. [2]
    A. Church, Introduction to Mathematical Logic, vol. I, Princeton 1956.Google Scholar
  3. [3]
    F. B. Fitch, ‘Intuitionistic Modal Logic with Quantifiers’, Portugaliae Mathematica 7 (1948)113–118.Google Scholar
  4. [4]
    L. Henkin, ‘The Completeness of the First-Order Functional Calculus’, The Journal of Symbolic Logic 14 (1949) 159–66.CrossRefGoogle Scholar
  5. [5]
    L. Henkin, ‘Completeness in the Theory of Types’, The Journal of Symbolic Logic 15(1950) 81–91.CrossRefGoogle Scholar
  6. [6]
    L. Henkin, ‘Banishing the Rule of Substitution for Functional Variables’, The Journal of Symbolic Logic 18 (1953) 201–208.CrossRefGoogle Scholar
  7. [7]
    K. J. J. Hintikka, ‘Two Papers on Symbolic Logic’, Acta Philosophica Fennica 8 (1955).Google Scholar
  8. [8]
    H. Leblanc, ‘A simplified account of validity and implication’, The Journal of Symbolic Logic 33 (1968) 231–235.CrossRefGoogle Scholar
  9. [9]
    H. Leblanc, ‘A Simplified Strong Completeness Proof for QC=’, forthcoming.Google Scholar
  10. [10]
    H. Leblanc, ‘Three generalizations of a theorem of Beth’s’, forthcoming.Google Scholar
  11. [11]
    W. V. O. Quine, Set Theory and its Logic, Cambridge, 1963.Google Scholar
  12. [12]
    K. Schütte, ‘Syntactical and semantical properties of simple type theory’, The Journal of Symbolic Logic 25 (1960) 305–26.CrossRefGoogle Scholar


  1. 1.
    See [8], [9], and [10].Google Scholar
  2. 2.
    Parameters and variables will play here the roles respectively assigned elsewhere to free variables and bound ones. By using two runs of letters per type, we avoid some of the difficulties that would otherwise be involved in giving a correct account of substitution (of terms) for free variables. Neither our parameters nor our variables are to be associated with relations of more than one argument; as in [11], such relations may be simulated using the well-known Wiener-Kuratowski techniques.Google Scholar
  3. 3.
    Define the simultaneous replacement of P 1,…,P n by Q 1,…, Qn in A as A(R 1/P 1) (…) (Rn/Pn) (Q 1/R 1) (…) (Qn/Rn), where R 1,…, R n are the first n parameters foreign to A and different from Q 1,…,Qn.Google Scholar
  4. 4.
    The technique of the papers of Leblanc cited earlier has been revised here to make the relation ‘is isomorphic to’ an equivalence relation among sets of wffs of T. Note that if G contains no parameters (in particular, if ΆG is empty), every set isomorphic to G is identical with G by our definitions (since f is here the empty function). We shall, by the way, refer to f itself as anisomorphism, if it meets the conditions laid down in the text.Google Scholar
  5. 5.
    We presume ‘&’,‘⋀’, ‘≡’, and ‘∃’ defined in the customary manner. Note that only sentences are axioms.Google Scholar
  6. 6.
    We might dispense with the braces and colon as primitive signs, following rather Quine’s example in [11] by defining P∈X:A as A(P/X) and X:A∈K as (∃Y)((Z) (Z∈Y≡A(Z/X))&Y∈K). In that case A7 could be replaced by the axiom (scheme) of Comprehension, (3 X) (Y) (Y ∈ X ≡ A), where X is not free in A. However, because of the crucial role played by abstracts in our account of a general truth-value function for T, we prefer to have P∈X:A and X:A∈K count as genuine wffs of T (rather than as mere definitional rewrites)Google Scholar
  7. 7.
    If X is not free in A, A (K/X) is not of course just A. Google Scholar
  8. 8.
    This is the familiar axiom of Extensionality. It may of course be dropped (as it is, e.g., in [12]), turning T into a theory of attributes rather than of classes. If A9 is dropped, then in the semantical account of Section 4, (v) must also be dropped.Google Scholar
  9. 9.
    The trick of counting (X) A (X/P) as an axiom when A is an axiom stems from [3].Google Scholar
  10. 10.
    Analogous moves will show that the biconditional in question can do duty for A9.Google Scholar
  11. 11.
    This proof borrows from [6], p. 203.Google Scholar
  12. 12.
    Note that a general truth-value function is not “recursive” in the sense that the truth- values of longer sentences be invariably determined by the truth-values of shorter ones; cf. the observation of p. 97.Google Scholar
  13. 13.
    The ambiguity of our use of‘t’ for ‘true’ as well as for an unspecified type is, of course, harmlessly resolved in context.Google Scholar
  14. 14.
    The above account of general implication and validity adapts to T the suggestion of Professor Hintikka to Leblanc acknowledged at the outset. Cf. [9] on the matter.Google Scholar
  15. 15.
    Our account below borrows significantly from [5], [4], and from Section 53 of [2].Google Scholar
  16. 16.
    We are partially indebted to Professor John Corcoran for this way of putting the matter.Google Scholar
  17. 17.
    In view of the Godel result cited on p. 77, completeness proofs (and hence the possibility of sharp syntactic characterization of semantical concepts which such proofs afford) are out of the question when we turn to the standard model-theoretic semantics for T. Accordingly, although the account below summarizes what we take to be intended by the standard model theory for T, as do corresponding accounts in [5] and (for the second-order calculus) in [2], the standards involved seem to us as little secure as is the gold standard nowadays.Google Scholar
  18. 18.
    We have long since lost interest in ill-formed formulas, which frees the letter ‘S’ to refer (henceforth) to arbitrary sets; we use ‘s’, and on occasion ‘q’ and ‘r’, for the same purpose.‘G’ continues to refer to sets of sentences. Google Scholar
  19. 19.
    U(S) is thus the type-theoretic (standard)universe over S, while each of the Г t (S) is the collection of all type-theoretic entities of level t. On the intended interpretation, Г 0 (S) - i.e., S itself - is of course a collection of individuals, which do not themselves have further members. (U(S), naturally, is unmentionable according to the canons of simple type theory itself.)Google Scholar
  20. 20.
    For the remainder of this section, we leave most of the details in carrying out proofs to the reader.Google Scholar
  21. 21.
    I.e., v 0 contains exactly one parameter from each equivalence class. One may, of course, specify a unique v0 for any α by requiring that each equivalence class be represented by its alphabetically first member.Google Scholar
  22. 22.
    We distinguishq from its illustrious member, despite the reluctance which he has showed in [11] and elsewhere to do so.Google Scholar
  23. 23.
    The reader who thinks this unduly profligate may, if he wishes, decrease temporarily the number of parameters of T for each given type to finite size; in order to preserve the uniformity of our account of a general truth-value function forT, however, we shall not do so.Google Scholar
  24. 24.
    The question which the corollary answers was put to us by Professor Nuel BelnapGoogle Scholar

Copyright information

© D. Reidel Publishing Company, Dordrecht, Holland 1970

Authors and Affiliations

  • H. Leblanc
    • 1
    • 2
  • R. K. Meyer
    • 1
    • 2
  1. 1.Temple UniversityUSA
  2. 2.Indiana UniversityUSA

Personalised recommendations