¹ The present paper gives in more detailed form, and with some important improvements, the results reported in a paper entitled Toward a basic logic, read on Dec. 28, 1940, at Philadelphia at a joint meeting of the Association for Symbolic Logic and the A.A.A.S. Much of the general discussion included in the Philadelphia paper, however, has been omitted here. For a summary of the latter paper, see this Journal, vol. 6 (1941), p. 39. The present paper has benefited from the helpful comments made by the referee on a previous draft of it. The author's indebtedness to the writings of Curry, Church, Rosser, Quine, Carnap, Tarski, and other workers in this field, should be obvious.

² For references to some of Curry's and Rosser's main papers on combinatory logic see Curry, H. B., A revision of the fundamental rules of combinatory logic, this Journal, vol. 6 (1941), pp. 41–53Google Scholar, also an article by Curry that immediately follows the latter. The present system is also very similar to systems that have been proposed by Alonzo Church. See, for example, the system described on pp. 65 and 66 of his book, The calculi of lambda-conversion, Annals of Mathematics studies no. 6, Princeton University Press, Princeton, 1941.

³ These sentences are to be thought of as already “interpreted,” that is, as already understood as regards their meanings. In syntactical investigations a calculus is usually treated in abstraction from the meanings of its sentences.

⁴ An alternative (and in some respects preferable) method would be to define the class of K-sentences not as U itself but as a proper subclass of the class U. This could be done by a recursive definition somewhat as follows: Expressions of the form ‘(=ƒa)’ are K-sentences so is ‘(εaƒ); if (ƒ(ga)’ is a K-sentence so is ‘(oƒga)’; and so on (paralleling the rules in 3.1). Then it could be said that if ‘(ƒa)’ is a K-sentence, ‘(ƒa)’ expresses the proposition that a is a member of ƒ. Similarly it could be said that if ‘(gab)’ is a K-sentence, ‘(gab)’ expresses the proposition that a bears the dyadic relation g to b.

⁵ We may refer to ‘(ab)’ as the “combination” of ‘a’ with ‘b’, and to (ab) as the “application” of a to b.

⁶ The interpretation of these symbols should be clear from the use made of them. Briefly, however, the interpretation is as follows: ‘=’ means identity, ‘ε’ means class membership. ‘o’ means the triadic relation of ƒ to g to a such that the application of g to a is a member of ƒ. ‘έ’ means the triadic relation of a to ƒ to b such that g bears to b the dyadic relation ƒ, ‘ό’ means the tetradic relation of ƒ to g to a to b such that the application of g to a bears to b the dyadic relation ƒ. ‘W’ means the dyadic relation of ƒ to a such that a bears to itself the dyadic relation ƒ. ‘&’ means prepositional conjunction. ‘V’ means propositional alternation. ‘E’ means the class of existent (non-empty) classes. ‘*’ means the triadic relation of ƒ to a to b such that a bears to b the proper ancestral of the dyadic relation ƒ. Observe that ‘o’ and ‘ό’ are analogous to Curry's ‘B’, while ‘ε’ and ‘έ’ are analogous to Curry's ‘(CI)’, which is Rosser's ‘T’ Finally ‘W’ and ‘E’ are respectively analogous to Curry's ‘W’ and ‘Σ’.

⁷ It is to be understood that U-expressions used as variables are to be so chosen in each case that they occur nowhere except where indicated by the context.

⁸ A “U-calculus” is a calculus which is a subclass of U.

⁹ See Rosser, Barkley, An informal exposition of proofs of Gödel's theorems and Church's theorem, this Journal, vol. 4 (1939), pp. 53–60.Google Scholar

¹⁰ Supposing, of course, that U has been assigned an adequate supply of interpreted symbols.

¹¹ Observe the important part played by ‘W’ in the following discussion. Cp. the author's paper, A system of formal logic without an analogue to the Curry W-operator, this Journal, vol. 1 (1936), pp. 92–100. In that paper the Russell paradox is avoided by omitting the W-operator, in this paper by omitting negation.