The word problem for groups was first formulated by M. Dehn [1], who gave a solution for the fundamental groups of a closed orientable surface of genus g ≧ 2. In the following years solutions were given, for example, for groups with one defining relator [2], free groups, free products of groups with a solvable word problem and, in certain cases, free products of groups with amalgamated subgroups [3], [4], [5]. During the period 1953–1957, it was shown independently by Novikov and Boone that the word problem for groups is recursively undecidable [6], [7]; granting Church's Thesis [8], their work implies that the word problem for groups is effectively undecidable.

In [1] (p. 131 et seq) Professor A. N. Prior suggests a calculus of functions of propositions in which the range of the function variables is not restricted to truth functions.1 If f, g, … etc. represent such variables and we have quantification over all variables we can introduce propositional identity by definition as (ƒ)(ƒp ⊃ ƒq) Alternatively identity may be primitive with the usual axioms and schemata (v.e.g. [4] p. 190 et seq). We shall refer to such systems as ‘functorial calculi’2 (abbreviated as FC).

In [1], p. 171, Sacks asks (question (Q5)) whether there is a recursively enumerable degree of unsolvability d such that for all n ≧ 0. Sacks points out that the set of conditions which d must satisfy is not arithmetical. For this reason he suggests that a proof of (Q5) might require some new combinatorial device. The purpose of this note is to show how (Q5) may be proved simply by extending the methods of [l].2

A Turing Machine (TM) is an abstract, synchronous, deterministic computer with a finite number of internal states. It operates on the set of infinite words, or tapes, over some finite alphabet, scanning exactly one symbol of the tape at a time. (Only a 2-symbol alphabet, consisting of “0” and “|”, will be considered here, and the scanned symbol of a tape will be distinguished by an underscore.) depending upon its internal state and the symbol under scan, it can perform one or more of the following operations: replace the scanned symbol with a new symbol, focus its attention on an adjacent square, and transfer control to a new state.

In [1], page 85, Quine states: “… ponentials of logically true statements are logically true.” It is perhaps of some interest that this assertion is not completely precise as can be seen from counterexamples. One simple example is the following:

Let L be some language in which ‘c’ and ‘b’ are atomic sentential constants. Let ‘c’ be false and ‘b’ true. Suppose that L includes parentheses and the material conditional ‘⊃’ as logical notation, but that ‘b’, at least, counts as extra-logical.

Plusieurs auteurs ont déjà considéré l'ultraproduit et l'ultrapuissance en prenant certaines, et non forcément toutes les fonctions qui, à chaque indice i, associent un élément de la base de la relation de rang i (voir par exemple [6]). La généralisation ici considérée, appelée ultraproduit complet (voir §3) est définie à l'aide des isomorphismes locaux. On y retrouve l'essentiel de la théorie de l'ultraproduit classique avec évidemment des exemples plus variés.

In [2], Fischer has shown the existence of a bounded-truth-table degree of unsolvability which contains a collection of many-one degrees which has, under many-one reducibility, the order type, ω, of the positive integers. In [1; pg. 124], Dekker and Myhill give a construction which shows that the many-one degree of any simple set contains a collection of one-one degrees of simple sets which has, under one-one reducibility, the order type (ω + ω*) ·ω. A basic result of recursive function theory (due to Myhill) is that the creative sets form a many-one degree which consists of a single one-one degree (i.e. a single recursive isomorphism type).

It is well known that the recursive sets form three many-one degrees. Two of these, the degrees of the empty set and of the set of all integers, consist of single one-one degrees.

In [5] it was shown that to complete Herbrand's argument for his Fundamental Theorem (see [6]) a weak analyzing function for certain applications of the rules of passage is needed. The following theorem describes such a function. (We use the terminology and notation of [5] except that, for each schema S and each p ≧ 1, we shall write D(S,p) rather than DSp for the domain of order p generated by S. In addition, we shall say that an element of D(S, p) is of order k, 1 ≦ k ≦ p, if it belongs to D(S, k) but not to D(S,k—1).)

An implication A ⊃ B is said to be null in case A is false in all instances. This note describes several formal systems for first-order predicate logic and arithmetic in which null implications do not occur. In fact, the most restrictive systems avoid the occurrences of any formulas which represent null predicates. The precise sense of this avoidance is explained below.

An intuitionistic negation is a statement of the form A ⊃ F where F is a contradiction. The absence of null implications among true statements entails the absence of intuitionistic negations, and hence systems described here might be called negationless intuitionistic systems.

The matrix defining Łukasiewicz's three-valued logic, constructed in 1920 and described at length in [1], is the following:

This matrix was axiomatized in 1931 by Wajsberg (see [6]), who showed that the following axioms together with the rules of substitution and modus ponens were sufficient:

Markov's [2] notion of Normal Algorithm (NA), with which we assume familiarity, is the simplest of the better known ways of expressing the concept of algorithmicity. An NA consists of an ordered finite list of replacement formulae

The dots in parentheses indicate that a given replacement formula may be either simple (P → Q), or terminal (P → .Q). No restrictions are imposed on the lengths of the Pi and Qi in the replacement formulae, and the only rule of order of application is a priority rule to the effect that of several replacement formulae applicable to a word W at a given step, the earliest one is used.

In this note is proved the following:

Theorem. Iƒ A × B is universal and one oƒ A, B is r.e. then one of A, B is universal.

Let α, τ be 1-argument recursive functions such that x goes to (σ(χ), τ(χ)) is a (1–1) map of the natural numbers onto all ordered pairs of natural numbers. A set A of natural numbers is called universal if every r.e. set is (many-one) reducible to A; A × B is called universal if the set

It is well known that the modal calculus S4 has infinitely many non-equivalent formulae in a single proposition letter (in standard terminology, infinitely many modal functions), whilst S5 has only finitely many. However, the situation regarding the intermediate modal calculi S4.2, S4.3, and Prior's Diodorean tense-logic D does not seem to have been settled. In this note we show that each of these systems, together with a certain proper supersystem D* of D, has infinitely many modal functions.

This is in contrast with the fact that in the intermediate propositional logics KC and LC, which correspond under the McKinsey-Tarski translations to S4.2 and S4.3, there are only finitely many non-equivalent formulae in a single proposition letter.2

In [1], McCall and I offered an axiomatization of the implicational fragment of the 3-valued Łukasiewiczian system defined in [2]. The following axiom schemata sufficed, together with the rule of modus ponens.1

In this paper, a simple inductive characterization of the ordinal numbers is stated and developed. The characterization forms the basis for a set of axioms for ordinal theory and also for several short explicit definitions of the ordinals. The axioms are shown to be sufficient for ordinal theory, and, subject to suitable existence assumptions, each of the definitions is shown to imply the axioms.

The present results apply to the familiar von Neumann version of the ordinals, but the methods used are easily adapted to other versions.