Published online by Cambridge University Press: 12 March 2014
The purpose of this paper is to construct a non-finitary system of logic S, based on the theory of types, in which classical quantification theory holds without restriction and the axiom of reducibility holds with such slight restriction as is perhaps unlikely to interfere with the construction of classical mathematics. The system will be shown to be consistent.
For purposes of orientation, a rough description of the ontology of the system will first be given. The ‘individuals’ are expressions built up in the following way: ‘0’ is an individual, and if ϕ and ψ are individuals, so is ˹*ϕψ˺. The usual apparatus of truth functional connectives and quantifiers is employed, and one primitive four place predicate ‘S’. ˹Sϕψχω˺ says that ϕ is the result of writing ψ for all occurrences of χ in ω, where ϕ, ψ, χ and ω may be formulae, individuals, or members of a wider category called ‘expressions’ which includes individuals, formulae, and other things as well. (At first sight this looks like a confusion of use and mention, but the formation rules and rules of inference are so phrased that no ambiguity arises.)
The individuals are divided into types concentrically, so that type 0 has them all as members and type n includes type m for m > n. There is no highest type, but we shall find it convenient from the point of view of exposition to construct an infinity of ‘auxiliary’ systems Q(k), restricted to types ≦ k, before presenting the system S.
1 This very fruitful construction is due to L. Chwistek, see e.g. The limits of science, New York, Harcourt Brace and Company, 1948, p. 86Google Scholar.
2 L. Chwistek, op. cit., pp. 182, 188.
3 Fitch, F. B., An extension of basic logic, this Journal, vol. 13 (1948), pp. 95–106Google Scholar. Theorem 3:2.
4 L. Chwistek, op. cit., p. 167 and pp. 94–5 respectively.
5 We do not really need this emendation in the present connection, since by our definition of classes the members of a class must be of type 2 at least. Hence ‘Typ?’ would serve as well as ‘Typ’ in 6.7. Nonetheless it is of interest to observe that ‘Typ’ can be defined quite generally in the Q(k)'s, and it may well be of use in further investigations.
6 L. Chwistek, op. cit., pp. 171, 183.
7 Tarski, A., Einfuhrung in die mathematische Logik, Vienna, Julius Springer, 1937CrossRefGoogle Scholar, Ch. VIII.
8 But it seems very unlikely that analysis needs a principle of extensionality. See e.g. F. B. Fitch, op. cit., pp. 104–6 and The Heine-Borel theorem in extended basic logic, this Journal, vol. 14 (1949), pp. 9–15Google Scholar; also L. Chwistek, op. cit., p. 133 and the reference given there, and Hilbert, D. and Bernays, P., Grundlagen der Mathematik, vol. II, Berlin, Julius Springer, 1939, pp. 461–3, 468–9Google Scholar.