Philosophical Problems in Logic pp 77-101 | Cite as

# Truth-Value Semantics for the Theory of Types

- 2 Citations
- 113 Downloads

## Abstract

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 called*valid 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.

## Keywords

Alphabetical Order Parametric Extension Semantic Characterization Extensionality Axiom Simple Type Theory## Preview

Unable to display preview. Download preview PDF.

## Bibliography

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

## References

- 1.See [8], [9], and [10].Google Scholar
- 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.Define the simultaneous replacement of
*P*_{1},…,*P*_{n}by*Q*_{1},…, Q*n*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.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 an*isomorphism*, if it meets the conditions laid down in the text.Google Scholar - 5.We presume ‘&’,‘⋀’, ‘≡’, and ‘∃’ defined in the customary manner. Note that only sentences are axioms.Google Scholar
- 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.
- 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.
- 10.Analogous moves will show that the biconditional in question can do duty for A9.Google Scholar
- 11.This proof borrows from [6], p. 203.Google Scholar
- 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.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.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.Our account below borrows significantly from [5], [4], and from Section 53 of [2].Google Scholar
- 16.We are partially indebted to Professor John Corcoran for this way of putting the matter.Google Scholar
- 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.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.
*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.For the remainder of this section, we leave most of the details in carrying out proofs to the reader.Google Scholar
- 21.I.e.,
*v*_{0}contains exactly one parameter from each equivalence class. One may, of course, specify a unique v_{0}for any α by requiring that each equivalence class be represented by its alphabetically first member.Google Scholar - 22.We distinguish
*q*from its illustrious member, despite the reluctance which he has showed in [11] and elsewhere to do so.Google Scholar - 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 for*T*, however, we shall not do so.Google Scholar - 24.The question which the corollary answers was put to us by Professor Nuel BelnapGoogle Scholar