The system K′ of “extended basic logic” lacks a principle of extensionality. In this paper a system KE′ will be presented which is like K′ in many respects but which does possess a fairly strong principle of extensionality by way of rule 6.37 below. It will be shown that KE′ is free from contradiction. KE′ is especially well suited for formalizing the theory of numbers presented in my paper, On natural numbers, integers, and rationals. The methods used there can be applied even more directly here because of the freedom of KE′ from type restrictions, but the details of such a derivation of a portion of mathematics will not be presented in this paper. It is evident, moreover, that KE′ contains at least as much of mathematical analysis as does K′, and perhaps considerably more. The method of carrying out proofs in KE′ is closely similar to that used in my book Symbolic logic, and could be expressed in similar notation.

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.

The lambda calculus was conceived by Church, and to some extent by Curry (see [1] and [2]), as a general theory of functions, more precisely as a formalization of two basic functional concepts: application and abstraction. This claim to universality was impossible to maintain, for it soon became apparent that functions in the calculus are required to have properties which are by no means universal. Self-application is certainly a very special feature, but more relevant from our point of view is the existence of fixed points, which is definitely a nonuniversal property of functions. This situation was not ignored, but was considered rather as a form of inconsistency very much related to the paradoxes of set theory (for example, see the discussion of the paradoxical combinator in [2]).

More recently, the lambda calculus has been studied by people in computer science, and as a result the algorithmic nature of the system has been more explicitly recognized. Eventually, the right approach was taken by D. Scott (see [4] and [5]) who restricted the objects of the calculus to continuous functionals over complete lattices, which can be combined in structures where application and abstraction are properly interpreted. It soon became clear that complete lattices were not necessary, and more general structures were introduced. On the other hand the requirement of continuity was essential for the construction, and has remained a basic feature. It is one of the purposes of this paper to show that in the general situation continuity can be replaced by monotonicity.

The work of Scott was extended by Wadsworth [6], who gave a precise formulation of the operational semantics, and proved the equivalence to Scott's interpretation.

The object of this note is to classify the isomorphism types of all complete atomic proper relation algebras. In particular we find that the number of abstractly distinct complete atomic proper finite relation algebras of 2m elements is equal to the number of distinct partitions of the positive integer m into summands which are perfect squares.

A relation algebra is called complete atomic if its Boolean algebra is complete atomic. A proper relation algebra is a relation algebra whose elements are relations. Lyndon has recently proved, by constructing an appropriate finite relation algebra, that not every complete atomic relation algebra is isomorphic to a proper relation algebra.

Henceforth, let us consider a complete atomic proper relation algebra. The atoms {〈a, b〉}, {〈c, d〉} will be called connected if and only if {a, b} ⋂ {c, d} is not empty. Let the relation of connectedness over the set B of all atoms be denoted by ~. For brevity let B = {b1,b2, …}. The relation ~ is obviously reflexive and symmetric. But ~ is not transitive, since a, b, c, d distinct implies {〈a, 0〉} ~ {〈b, c〉}, {〈b, c〉} ~ {〈c, d〉}, and {〈a, b〉} ≁ {〈c, d〉}.

The fundamental role of the restricted calculus of predicates in applications of symbolic logic, and particularly in Hubert's Beweistheorie as summed up by Hilbert and Bernays, makes it important that this logical calculus should be accurately defined. The first standard formulation of the calculus was that of Hilbert and Ackermann's Grundzüge der theoretischen Logik. This employed (in the first three editions) a finite set of axioms and rules of derivation, with rules of substitution included. A reaction by Hilbert and Ackermann's successors to persistent difficulty encountered with the rules of substitution has been to omit these rules, and instead enlarge the set of axioms and the other rules of derivation so as to encompass all possible substitutions. Such an enlargement seems to me to be undesirable. As an alternative, this note is designed to put the original approach of Hilbert and Ackermann for once and for all on a sound basis.

One of the main results of Gödel [4] and [5] is that, if M is a transitive set such that 〈M, Є 〉 is a model of ZF (Zermelo-Fraenkel set theory) and α is the least ordinal not in M, then 〈Lα, Є 〉 is also a model of ZF.

In this note we shall use the Jensen uniformisation theorem to show that results analogous to the above hold for certain subsystems of ZF. The subsystems we have in mind are those that are formed by restricting the formulas in the separation and replacement axioms to various levels of the Levy hierarchy.

This is all done in §1. In §2 we proceed to establish the exact order relationships which hold among the ordinals of the minimal models of some of the systems discussed in §1. Although the proofs of these latter results will not require any use of the uniformisation theorem, we will find it convenient to use some of the more elementary results and techniques from Jensen's fine-structural theory of L. We thus provide a brief review of the pertinent parts of Jensen's works in §0, where a list of general preliminaries is also furnished.

We remark that some of the techniques which we use in the present paper have been used by us previously in [6] to prove various results about β-models of analysis. Since β-models for analysis are analogous to transitive models for set theory, this is not surprising.

Define to be the smallest cardinality of a function f: X→Y with I, X, Y, ⊆ 2ω such that there is no Borel function g ⊇ f. In this paper we prove that it is relatively consistent with ZFC to have b < where b is, as usual, smallest cardinality of an unbounded family in Ωω. This answers a question raised by Zapletal.

We also show that it is relatively consistent with ZFC that there exists X ⊆ 2ω such that the Borei order of X is bounded but there exists a relatively analytic subset of X which is not relatively coanalytic. This answers a question of Mauldin.