Summer Meeting of the Association for Symbolic Logic
S OF PAPERS 283 constituents of r and D have the same order in H that they have in r and D respectively; and where A is non-empty iff A is a propositional variable. There is provable for LI an appropriate Elimination Theorem (Haupsatz): if r, A I F A and (D, T I F C are theorems of LI, then so also is H, T* I C, where all and only the constituents of r and D appear in H, and have the same order in H which they have in r and (D respectively; and where T must contain A, A is nonempty iff A is a propositional variable, and T* is the result of replacing A by A throughout T. The proof is by induction on rank and degree as in Gentzen. With the help of the Elimination Theorem, it is easily shown that LI is equivalent to the pure implicational fragment of E as defined above. Remarks: (1) The interpretation of Al, A2, . . ., A. I B is not that the conjunction of Al, A2, . . ., A. entails B; this statement has rather the stronger sense that Al entails that A2 entails that ... A. entails B. (2) In accordance with (1), LI has no rule permitting addition of arbitrary constituents, nor any rule permitting arbitrary permutation of constituents though some of the functions of the usual rule of permutation are carried in the statement of the rule for implication on the left. (3) As yet no decision procedure for LI has been found; the usual methods depend on the presence of the converse of the rule of contraction, which fails for LI. (4) The condition that I F A -+ B only if A and B have some propositional variable in common can be taken as a partial explication of the intuitive demand for relevance as between antecedent and consequent of an entailment. LI satisfies this condition. (5) The usual rules for conjunction and disjunction may be added to L., an Elimination Theorem being provable for the system so defined; but for this system the distributivity principles for conjunction and disjunction (present in E) are not forthcoming. P. C. GILMORE. An alternative to set theory. Because the concept of set is so simple and yet so powerful, its convenience for mathematicians is overwhelming. The concept, however, must be limited by ad hoc restrictions if the set theoretic paradoxes are to be avoided. An alternative to set theory is proposed which is as simple in conception as naive set theory and yet which is not troubled by its inherent contradictions. In place of a universe of sets and the membership relation over the universe there appears a universe of symbols and an epsilon and nu relation over the universe. Symbols such as '1', '2', '3', 'even', '<', '+', etc., can be understood to be members of the universe of symbols. The sentence '2 is even' is understood to assert that the symbol '2' is epsilon related to the symbol 'even', and the sentence '3 is not even' is understood to assert that the symbol '3' is nu related to 'even'. Thus sentences '3 is even' and '3 is not even' are not negations of one another although, accepting (x) (y)-(x E y & x v y) as true, each implies the negation of the other. Relations and functions are conceptually much simpler in the new theory than in set theory. '<', for example, is a relation symbol because, although nothing is epsilon or nu related to it, there are symbols epsilon or nu related to the concatenation of it with other symbols. Thus '2' is epsilon related to ' <3' and nu related to ' < 1'. Similarly '(1 + 1)' is a symbol which is epsilon related to ' <3' and nu related to '< 1'. Although the problem of the consistency of axiomatic theories motivated by the new theory is no less difficult than with axiomatic set theories, nevertheless greater confidence can be given to the new theory than to set theory since the paradoxes which are inherent in the concept of set are avoided in the new theory. Thus despite that there can be no set of all sets which are not members of themselves, there can be a symbol R for which (x) ((x E R =x v x) & (x v R -x E x)) is true, although it necessarily follows that (~.R E R & -'-R v R) is true also. 284 ABSTRACTS OF PAPERS G. KREISEL. Inessential extensions of Heyting's arithmetic by means of functionals of finite type. Let T denote the system given by G6del in Dialectica 47/48 (1958), pp. 283-284; T, is obtained by adding to the non-logical axioms of T an intuitionistic predicate calculus of type w and the induction schema for all formulae in the extended notation. Tlc is obtained from T, by adding the axioms of choice (x)(3y) V(x, y) (3 Y) (x) -V[x, Y(x)] for all finite types of x and y and a? in the notation of T1. F' is G6del's translation l.c. of F, extended to Ti(TiC), F* is the author's translation of F, given in para. 3.52 on p. 112 of Constructivity in Mathematics (1959), which we