In this paper, I present a modified and extended version of combinatory logic. Schönfinkel originated the study of combinatory logic (in [2]), but its development is primarily due to H. B. Curry. In the present paper, I will make use of both the symbolism (with some modification) and the results of Curry, as found in [1].

What is novel about my version of combinatory logic is a kind of combinators which I call discriminators. These combinators discriminate between different symbols, and yield values which are determined by the symbols which are their arguments. If the normal combinators investigated by Curry are considered as functions taking (combinations of) symbols as arguments and yielding symbols as values, these combinators can rearrange and cancel their arguments or introduce new symbols.

One of the basic results in the theory of λ-conversion is the Church-Rosser Theorem, which says that, using certain rules for conversion and reduction of λ-formulae, any two interconvertible formulae can both be reduced to one formula. (I will not explain this in detail, as λ-conversion is described fully in Church's [2], where the Church-Rosser Theorem is Theorem 7 XXVII; see also Chapter 4 of Curry and Feys' [3].) The first part of the present paper contains an abstract form of this theorem.

Let G be a separated (Hausdorff) topological group and let *G be an enlargement of G (see [8]). Thus, *G (i) possesses the same formal properties as G in the sense explained in [8], and (ii) every set of subsets {Aν } of G with the finite intersection property—i.e. such that every nonempty finite subset of {Aν } has a nonempty intersection—satisfies ∩*Aν ≠ ø, where the *Aν are the extensions of the Aν in *G, respectively.

In this paper we consider some axiomatic systems of set theory related to the system NF (New Foundations) of Quine. In particular we discuss the possible relations of cardinality between a finite set x and its subset class SC(x) = {y | y ∩ x} and also between x and its unit set class USC(x) = {{y} | y ε x}. Specker [5] has shown that in NF the cardinal of a finite set x can never be the same as the cardinal of SC(x).

In this paper a new property of theories, called effective retractability is introduced and used to obtain a characterization for the degrees of subtheories of arithmetic and set theory. By theory we understand theory in standard formalization as defined by Tarski [10]. The word degree refers to the Kleene-Post notion of degree of recursive unsolvability [2]. By the degree of a theory we mean, of course, the degree associated with its decision problem via Gödel numbering.

By language we understand a lower predicate calculus with identity and (perhaps) relation and function symbols. It is convenient to allow for more than one sort of variable. Now each individual constant (if there are any) is of a specified sort, the formal expressions R(t1, … tn), f(t1,…, tn) are well formed only if the terms t1, …, tn are of specified sorts determined by the relation symbol R and the function symbol f, and the term f(t1, …, tn) (if well formed) is of a sort determined by f. We admit s = t as well formed, no matter what the sorts of s and t.

It has been known for some time that there is a primitive recursive permutation of the nonnegative integers whose inverse is recursive but not primitive recursive. For example one has this result apparently for the first time in Kuznecov [1] and implicitly in Kent [2] or J. Robinson [3], who shows that every singularly recursive function ƒ is representable as

where A, B, C are primitive recursive and B is a permutation.

The uniform halting problem (UH) can be stated as follows.

Give a decision procedure which for any given Turing machine (TM) will decide whether or not it has an immortal instantaneous description (ID).

An ID is called immortal if it has no terminal successor. As it is generally the case in the literature (see e.g. Minsky [3, p. 118]) we assume that in an ID the tape must be blank except for some finite numbers of squares. If we remove this restriction the UH becomes the immortality problem (IP). The UH should not be confused with the initialised uniform halting problem (whether or not a TM has an immortal ID when started in a specified state) which can easily be shown to be undecidable (see e.g. Minsky [3, p. 151]).