Hostname: page-component-78c5997874-lj6df Total loading time: 0 Render date: 2024-11-10T04:15:35.506Z Has data issue: false hasContentIssue false
  • English
  • Français

A homogeneous system for formal logic1

Published online by Cambridge University Press:  12 March 2014

R. M. Martin
R. M. Martin*
Affiliation:
Yale University
Get access Rights & Permissions [Opens in a new window]

Extract

Two more or less standard methods exist for the systematic, logical construction of classical mathematics, the so-called theory of types, due in the main to Russell, and the Zermelo axiomatic set theory. In systems based upon either of these, the connective of membership, “ε”, plays a fundamental role. Usually although not always it figures as a primitive or undefined symbol.

Following the familiar simplification of Russell's theory, let us mean by a logical type in the strict sense any one of the following: (i) the totality consisting exclusively of individuals, (ii) the totality consisting exclusively of classes whose members are exclusively individuals, (iii) the totality consisting exclusively of classes whose members are exclusively classes whose members in turn are exclusively individuals, and so on. Any entity from (ii) is said to be one type higher than any entity from (i), any entity from (iii), one type higher than any entity from (ii), and so on. In systems based upon this simplified theory of types, the only significant atomic formulae involving “ε” are those asserting the membership of an entity in an entity one type higher. Thus any expression of the form “(x∈y)” is meaningless except where “y” denotes an entity of just one type higher than the type of the entity denoted by “x” It is by means of general type restrictions of this kind that the Russell and other paradoxes are avoided.

Type
Research Article
Information
The Journal of Symbolic Logic , Volume 8 , Issue 1 , 19 March 1943 , pp. 1 - 23
Copyright
Copyright © Association for Symbolic Logic 1943

Access options

Get access to the full version of this content by using one of the access options below. (Log in options will check for institutional or personal access. Content may require purchase if you do not have access.)

Footnotes

1

A part of the material of this paper was contained in a thesis, of the same title, presented for the degree Doctor of Philosophy in Yale University, 1941. The author wishes to thank Professor Frederic B. Fitch for many invaluable criticisms and suggestions, and to express his appreciation to the University of Virginia for a duPont research grant during the session 1941–42.

References

2 Cf. Russell, B., Mathematical logic as based on the theory of types, American Journal of mathematics, vol. 30 (1908), pp. 222–262CrossRefGoogle Scholar, and Whitehead, A. N. and Russell, Bertrand, Principia mathematica, 2nd edn., Cambridge, England, 1925–27.Google Scholar For a now classical system based upon the simplified theory of types, see Gödel, K., Über formal unentsekeidbare Sätze der Principia Mathematica und verwandter Systeme I, Monatshefte für Mathematik und Physik, vol. 38 (1931), pp. 173–198CrossRefGoogle Scholar, especially pp. 176–8.

3 Zermelo, E., Untersuchungen über die Grundlagen der Mengenlehre I, Mathematische Annalen, vol. 65 (1908), pp. 261–281CrossRefGoogle Scholar, and Über Grenzzahlen und Mengenbereiche, Fundamenta mathematicae, vol. 16 (1903), pp. 29–47. Cf. also von Neumann, J., Eine Axiomatisierung der Mengenlehre, Journal für die reine und angewandte Mathematik, vol. 154 (1925), pp. 219–240Google Scholar (and Berichtigung, ibid., vol. 155 (1926), p. 128), and Die Axiomatisierung der Mengenlehre, Mathematische Zeitschrift, vol. 27 (1928), pp. 609–752; Bernays, P., A system of axiomatic set theory, this Journal, vol. 2(1937), pp. 65–77Google Scholar, and vol. 6(1941), pp. 1–17, and vol. 7(1942), pp. 65–89; Gödel, K.The consistency of the continuum hypothesis, Princeton, N. J., 1941, especially pp. 3–34.Google Scholar

4 Cf. Hilbert, D. and Ackermann, W., Grundzüge der theoretischen Logik, 2nd edn., Berlin 1938, pp. 45–99.CrossRefGoogle Scholar

5 Cf. A. Tarski, Appendix E to Woodger's, J. H.The axiomatic method in biology (Cambridge, England, 1937), pp. 161–172Google Scholar; also Leonard, H. S. and Goodman, N., The calculus of individuals and its uses, this Journal, vol. 5 (1940), pp. 45–55.Google Scholar

6 Cf. e.g., Hilbert and Ackermann, loc. cit.; von Neumann, J., Zur Hilbertschen Beweistheoric, Mathematische Zeitschrift, vol. 26 (1927), pp. 1–46CrossRefGoogle Scholar; and Church, A., A set of postulates for the foundation of logic, Annals of mathematics, ser. 2 vol. 33 (1932), pp. 346–366.CrossRefGoogle Scholar

7 Cf. Quine, W. V., Logic based upon inclusion and abstraction, this Journal, vol. 2 (1937), see p. 146Google Scholar, and Mathematical logic, New York 1940, pp. 33–37.

8 The outside pair of parentheses in an expression of the form ‘(X ⊃ Y)’, ‘(X v Y)’, ‘(X ˙ Y)’, or ‘(X ≡ Y)’ will be said to be determined by the main occurrence of “⊃”, “v”, “˙”, or “≡” respectively in that context. Let all pairs of parentheses determined by occurrences of “⊃”, “v”, “˙”, or “≡” (with the exception of the outside pair of parentheses contained in the positive scope of a binding occurrence of an H-variable) be either dropped or supplanted by dots, colons, etc., according to the familiar conventions. Cf., e.g., Principia, vol. 1, pp. 9–11. Here however an equal number of dots will always flank an occurrence of a connective “⊃”, “v”, or “≡”. Also for perspicuity each of these connectives will always be flanked by at least one pair of dots and none will require fewer dots than another. Thus ‘X ˙ ⊃ ˙ Y ˙ v ˙ Z’ will never appear, but will be written ‘X : ⊃ : Y ˙ v ˙ Z’ The “˙” connective will in certain cases be supplanted by a colon, by three dots, etc., in familiar fashion. Thus we shall write ‘X : Y ˙ v ˙ Z’, not of course ‘X ˙ Y ˙ v ˙ Z’. Also the use of dots will be extended to the “∼” as well. Thus we shall write ‘∼ : X ˙ Y’ not ‘∼ (X ˙ Y)’, except of course where this latter is the scope of a binding occurrence of an H-variable. Also the number of dots (if any) immediately following “∼” in the context ‘∼ X’ will always be one greater than the number of dots flanking (or constituting, as in the case of “˙”) a connective in X. Also in the case where ‘∼ X’ occurs on either side of a connective, the number of dots required for that connective will be one greater than the number of dots required for that occurrence of “∼” Thus we shall write ‘X ˙: ⊃ :. ∼ : X ˙ Y’, not ‘X : ⊃ : ∼ : X ˙ Y’. Also the outside pair of parentheses contained in contexts of the form ‘(a ⊂ b)’ will be dropped except here ‘(a ⊂ b)’ is the positive scope of a binding occurrence of an H-variable.

9 The outer parentheses contained in contexts of the form ‘(a = b)’ will be dropped except where ‘(a = b)’ is the positive scope of a binding occurrence of an H-variable. This convention will also hold for all H-formulae stipulated by subsequently introduced definienda.

10 Cf., e.g., W. V. Quine, Mathematical logic, pp. 79–80; or Church, A., The calculi of lambda-conversion, Princeton, N. J., 1941, p. 8.Google Scholar

11 Let the conventions for the omission and retention of parentheses be extended in such a way that the outside parentheses contained in the positive abstract scope of an abstract binding occurrence of an H-variable be retained.

12 This additional stipulation gives us a notationally unique definiendum for X, only of course where some κ places in which a 1, …, a n occur freely in X have been picked out in advance.

13 Cf. Definition in Tarski, A., Zur Grundlegung der Booleschen Algebra, Fundamenta mathematicae, vol. 24 (1935), sée p. 191CrossRefGoogle Scholar; and Definition 1.4 in Appendix E to J. H. Woodger, loc. cit., p. 163.

14 Peano, G., Sul concetto di numero, Rivista di matematica, vol. 1 (1891), pp. 87–102Google Scholar, 256–267; also Formulaire de mathématiques, 5 vols., Turin, 1895–1908.

15 Explicit mention of use made of D1.l through D2 will be omitted in the proofs. Also we shall frequently pass from expressions such as ‘b ⊂ a ˙ ⊃ ˙ b⊂a’ as e.g. in the proof of the next theorem-schema, T1.21, to ‘b ε Unit ˙ b⊂a : ⊃ : b⊂a’ without explicit mention of D4.1 or D5. Other definitions will also be used tacitly in this way, and throughout no mention will be made of the frequent use of D4.1.

16 Hereafter as here reference to R3 will be understood as indicating reference to R1, R2, or R3 as required. Thus e.g. in the proof of T1.3, mention of R3 actually refers to both Rl and R3.

17 Mention of D6.1 through D7 will occasionally be omitted. Thus e.g. as here we may pass from ‘a⊂a’ without mention of D6.2, or from ‘a = b ˙ ≡ ˙ b = a’ to ‘N = b ˙ ≡ ˙ b = N’ without mention of D7.

18 Cf. Huntington, E. V., Sets of independent postulates for the algebra of logic, Transactions of the American Mathematical Society, vol. 5 (1904), pp. 288–309.CrossRefGoogle Scholar

19 It will be noticed that we pass here from ‘(x) (xεNCind ‘a ˙ ≡ ˙ xεNCind ‘c)’ to ‘NCind ‘a = NCind ‘c’ by means of D17 without mention of D15.1. D17, D18, and D19 will frequently be used in this way, involving a tacit use of certain of the other definitions. Also we shall frequently pass from a theorem-schema containing an expression of the form F to a corresponding theorem-schema containing e.g. an expression of the form “I” or ‘NCind ‘a’ in all places where there are (free) occurrences of F originally, without mention of D5, D9, D15.1, or D19.

20 For a related theory of descriptions, see Quine, W. V., Mathematical logic, pp. 146–149.Google Scholar

21 For the fundamental ideas embodied in this theory of recursive functions, see Rosser, J. B., On the consistency of Quine's New foundations for mathematical logic, this Journal, vol. 4 (1939), see p. 21Google Scholar, especially T30 through T38. Rosser's “[xyz]εA” corresponds roughly with the present ‘(F,G,H) *K (0,G,0)’. Cf. also Hilbert, D. and Bernays, P., Grundlagen der Mathematik, Berlin, vol. 1, 1934, pp. 286–382Google Scholar, 383–468, and vol. 2, 1939, pp. 392–421.