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 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.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
Bibliography
E. W. Beth, The Foundations of Mathematics, Amsterdam 1959.
A. Church, Introduction to Mathematical Logic, vol. I, Princeton 1956.
F. B. Fitch, ‘Intuitionistic Modal Logic with Quantifiers’, Portugaliae Mathematica 7 (1948)113–118.
L. Henkin, ‘The Completeness of the First-Order Functional Calculus’, The Journal of Symbolic Logic 14 (1949) 159–66.
L. Henkin, ‘Completeness in the Theory of Types’, The Journal of Symbolic Logic 15(1950) 81–91.
L. Henkin, ‘Banishing the Rule of Substitution for Functional Variables’, The Journal of Symbolic Logic 18 (1953) 201–208.
K. J. J. Hintikka, ‘Two Papers on Symbolic Logic’, Acta Philosophica Fennica 8 (1955).
H. Leblanc, ‘A simplified account of validity and implication’, The Journal of Symbolic Logic 33 (1968) 231–235.
H. Leblanc, ‘A Simplified Strong Completeness Proof for QC=’, forthcoming.
H. Leblanc, ‘Three generalizations of a theorem of Beth’s’, forthcoming.
W. V. O. Quine, Set Theory and its Logic, Cambridge, 1963.
K. Schütte, ‘Syntactical and semantical properties of simple type theory’, The Journal of Symbolic Logic 25 (1960) 305–26.
References
See [8], [9], and [10].
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.
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.
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.
We presume ‘&’,‘⋀’, ‘≡’, and ‘∃’ defined in the customary manner. Note that only sentences are axioms.
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)
If X is not free in A, A (K/X) is not of course just A.
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.
The trick of counting (X) A (X/P) as an axiom when A is an axiom stems from [3].
Analogous moves will show that the biconditional in question can do duty for A9.
This proof borrows from [6], p. 203.
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.
The ambiguity of our use of‘t’ for ‘true’ as well as for an unspecified type is, of course, harmlessly resolved in context.
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.
Our account below borrows significantly from [5], [4], and from Section 53 of [2].
We are partially indebted to Professor John Corcoran for this way of putting the matter.
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.
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.
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.)
For the remainder of this section, we leave most of the details in carrying out proofs to the reader.
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.
We distinguishq from its illustrious member, despite the reluctance which he has showed in [11] and elsewhere to do so.
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.
The question which the corollary answers was put to us by Professor Nuel Belnap
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 1970 D. Reidel Publishing Company, Dordrecht, Holland
About this chapter
Cite this chapter
Leblanc, H., Meyer, R.K. (1970). Truth-Value Semantics for the Theory of Types. In: Lambert, K. (eds) Philosophical Problems in Logic. Synthese Library, vol 29. Springer, Dordrecht. https://doi.org/10.1007/978-94-010-3272-8_4
Download citation
DOI: https://doi.org/10.1007/978-94-010-3272-8_4
Publisher Name: Springer, Dordrecht
Print ISBN: 978-94-010-3274-2
Online ISBN: 978-94-010-3272-8
eBook Packages: Springer Book Archive