In [4], I introduced a quasi-Boolean algebra, and showed that in a formal system of simple type theory, from which the cut rule is omitted, wffs form a quasi-Boolean algebra, and that the cut-elimination theorem can be formulated in algebraic language. In this paper we use the result of [4] to prove the cut-elimination theorem in simple type theory. The theorem was proved by M. Takahashi [2] in 1967 by using the concept of Schütte's semivaluation. We use maximal ideals of a quasi-Boolean algebra instead of semivaluations.

The logical system we are concerned with is a modification of Schütte's formal system of simple type theory in [1] into Gentzen style.

Inductive definition of types.

0 and 1 are types.

If τ1, …, τn are types, then (τ1, …, τn) is a type.

Basic symbols.

a1τ, a2τ, … for free variables of type τ.

x1τ, x2τ, … for bound variables of type τ.

An arbitrary number of constants of certain types.

An arbitrary number of function symbols with certain argument places.

We shall prove that if a model of cardinality κ can be expanded to a model of a sentence ψ of by adding a suitable predicate in more than κ ways, then, it has a submodel of power μ which can be expanded to a model of ψ in > μ ways provided that λ, κ, μ satisfy suitable conditions.

In this paper a converse of Barwise's completeness theorem is proved by cut-elimination considerations applied to inductive definitions. We show that among the transitive sets T satisfying some weak closure conditions (closure under primitive-recursive set-functions is more than enough), only the unions of admissible sets satisfy Barwise's completeness theorem in the form stating that if φ ∊ T is a sentence which has a derivation (in the universe) then φ has a derivation in T. See §1 for the origin of the problem in Barwise's paper [Ba].

Stated quite briefly the proof is as follows (a step-by-step account including relevant definitions is given in the body of the paper):

Let T be a transitive prim.-rec. closed set, and let is nonempty, transitive and closed under pairs}. For each let κ(A) be the supremum of closure ordinals of first-order positive operators on subsets of A (first-order with respect to By Theorem 1 of [BGM], it is enough to prove that rank(T) in order to obtain that T is a union of admissible sets. (The rank of a set is defined by rank(x) = supy ∊ x (rank(y) + 1); since T is prim.-rec. closed, rank(T) = smallest ordinal not in T.)

Let We show how to find in T (in fact, in Lω(A)) a derivable sentence τ that has no derivation D such that rank(D) ≤ α. Thus, if τ is to have a derivation in T, rank(T) > α. α is arbitrary (< κ(A)), so rank(T) ≥ κ(A). Q.E.D.

Permutation methods for proving relative consistency results were first applied to Quine's set theory NF by Dana Scott [5]. He showed that the sentence (∃x)(x = {x}), which asserts the existence of individuals in Quine's sense, and its negation are each consistent relative to NF. In this paper Scott's method is shown to apply to any extension T of NF whose axioms are invariant in a certain sense. (Every stratified sentence is invariant, as are many interesting unstratified sentences, such as Rosser's Counting Axiom and the sentence which asserts that every Cantorian set is strongly Cantorian.) We also use this method to prove a number of interesting relative consistency results for such extensions T of NF.

Our main result (Theorem 2.4) asserts that it is consistent relative to T to assume that every well ordering of a strongly Cantorian set is order isomorphic to the well ordering by ∈ of a von Neumann ordinal. (The restriction to strongly Cantorian sets is necessary.) Therefore, although one cannot develop within NF a satisfactory theory of von Neumann ordinals, due to the many unstratified formulas which arise, our result shows that one can consistently assume as rich a theory as is allowed by the extent to which T provides for strongly Cantorian sets. This seems to be the first such “positive” consistency result for NF, and we think that the permutation method will yield others.

In classical logic a collection of sets of statements (or equivalently, a property of sets of statements) is called a consistency property if it meets certain simple closure conditions (a definition is given in §2). The simplest example of a consistency property is the collection of all consistent sets in some formal system for classical logic. The Model Existence Theorem then says that any member of a consistency property is satisfiable in a countable domain. From this theorem many basic results of classical logic follow rather simply: completeness theorems, the compactness theorem, the Lowenheim-Skolem theorem, and the Craig interpolation lemma among others. The central position of the theorem in classical logic is obvious. For the infinitary logic the Model Existence Theorem is even more basic as the compactness theorem is not available; [8] is largely based on it.

In this paper we define appropriate notions of consistency properties for the first-order modal logics S4, T and K (without the Barcan formula) and for intuitionistic logic. Indeed we define two versions for intuitionistic logic, one deriving from the work of Gentzen, one from Beth; both have their uses. Model Existence Theorems are proved, from which the usual known basic results follow. We remark that Craig interpolation lemmas have been proved model theoretically for these logics by Gabbay ([5], [6]) using ultraproducts. The existence of both ultra-product and consistency property proofs of the same result is a common phenomena in classical and infinitary logic. We also present extremely simple tableau proof systems for S4, T, K and intuitionistic logics, systems whose completeness is an easy consequence of the Model Existence Theorems.

The abstraction principle is

for K any formula not involving x. This is well known to be inconsistent and in [1] Hintikka proposed two modified versions of (0) which we briefly describe. First, he suggested

where K is any formula not involving x, and K+ is obtained from K by replacing subformulae of the form ∃zL by ∃z(z ≠ x ∧ L) and those of the form ∀zL by ∀z(z ≠ x → L), etc. The second version is

where K+ is a formula of the type described for (1) and z1 …, zk are all the free variables in (2).

This paper contains some observations on models for A2-second-order arithmetics. It arose from unsuccessful attempts to prove the Conjecture 1 (see at the end of the paper). Two partial solutions are given in this paper. We also give a sketch of a new proof of a classical result of descriptive set-theory referred to in [3]. Unless otherwise specified the word “model” means “ω-model for second-order arithmetics with the axiom scheme of choice,” i.e., “ω-model of A2” in the terminology of [3]. We say that a model M1 is shorter than M2 iff there is in M2 a relation A which is a well-ordering in M2 such that every relation B which is a well-ordering in M1 is similar to an initial segment of A. We denote by M0 the principal model of A2, i.e., a model which has only standard integers and contains all sets of integers.

This paper is concerned with the hyderdegrees of elements of uncountable Borel subsets of ωω. The Borel subsets of ωω are the so-called Δ11 subsets of ωω, which are the subsets of ωω that are Δ11 in some parameter f: ω → ω.

The results of this paper were inspired by two earlier results about the hyperdegrees of elements of Σ11 subsets of ωω. The first is known as the Gandy basis theorem, and asserts that the collection of functions of strictly lower hyperdegree than the hyperjump form a basis for the Σ11 subsets of ωω (see Rogers [3, p. 421]). The second is that there exists an uncountable Σ11 subset of ωω no element of which is hyperarithmetic in any other. The latter is credited to Feferman in Harrison [1], and appears there as Corollary 2.7, p. 537.

Two questions arise. Can we find other basis theorems if we replace Σ11 by Δ11 in Gandy's result? Can we replace Σ11 by Δ11 in Feferman's result?

We simultaneously answer the first positively, and the second negatively by proving that any hyperdegree, in which the hyperjump is hyperarithmetic, forms a basis for the Δ11 subsets of ωω with no hyperarithmetic elements. We conjecture that this holds also for uncountable Δ11 subsets of ωω. This conjecture is open despite the recent claim in Notices of the American Mathematical Society, vol. 19 (1972), p. A616, Abstract 696-02-10.

The Arithmetical Hierarchy Theorem of Kleene [1] states that in the complete theory of the standard model of arithmetic there is for each positive integer r a Σr0 formula which is not equivalent to any Πr0 formula, and a Πr0 formula which is not equivalent to any Πr0 formula. A Πr0 formula is a formula of the form

where φ has only bounded quantifiers; Πr0 formulas are defined dually.

The Linear Prefix Theorem in [3] is an analogous result for predicate logic. Consider the first order predicate logic L with identity symbol, countably many n-placed relation symbols for each n, and no constant or function symbols. A prefix is a finite sequence

of quantifier symbols ∃ and ∀, for example ∀∃∀∀∀∃. By a Q formula we mean a formula of L of the form

where v1, …, vr are distinct variables and φ has no quantifiers. A sentence is a formula with no free variables. The Linear Prefix Theorem is as follows.

Linear Prefix Theorem. Let Q and q be two different prefixes of the same length r. Then there is a Q sentence which is not logically equivalent to any q sentence.

Moreover, for each s there is a Q formula with s free variables which is not logically equivalent to any q formula with s free variables.

For example, there is an ∀∃∀∀∀∃ sentence which is not logically equivalent to any ∀∃∃∀∀∃ sentence, and vice versa. Recall that in arithmetic two consecutive ∃'s or ∀'s can be collapsed; for instance all ∀∃∀∀∀∃ and ∀∃∃∀∀∃ formulas are logically equivalent to Π40 formulas. But the Linear Prefix Theorem shows that in predicate logic the number of quantifiers in each block, as well as the number of blocks, counts.

In this paper I shall argue that the presumption of infinitude may be excised from the area of mathematics known as natural number theory with no substantial loss. Except for a few concluding remarks, I shall restrict my concern in here arguing the thesis to the business of constructing and developing a first-order axiomatic system for arithmetic (called ‘FA’ for finite arithmetic) that contains no theorem to the effect that there are infinitely many numbers.

The paper will consist of five parts. Part I characterizes the underlying logic of FA. In part II ordering of natural numbers is developed from a restricted set of axioms, induction schemata are proved and a way of expressing finitude presented. A full set of axioms are used in part III to prove working theorems on comparison of size. In part IV an ordinal expression is defined and characteristic theorems proved. Theorems for addition and multiplication are derived in part V from definitions in terms of the ordinal expression of part IV. The crucial final constructions of part V present a new method of replacing recursive characterizations by strict definitions.

In view of our resolution not to assume that there are infinitely many numbers, we shall have to deal with the situation where singular arithmetic terms of FA may fail to refer. For I know of no acceptable and systematic way of avoiding such situations. As a further result, singular-term instances of universal generalizations of FA are not to be inferred directly from the generalizations themselves. Nevertheless, (i) (x)(y)(x + y = y + x), for example, and all its instances are provable in FA.

In this paper we consider decision problems for subclasses of Kr, the class of those formulas of pure quantification theory whose matrices are conjunctions of binary disjunctions of signed atomic formulas. If each of Q1, …, Qn is an ∀ or an ∃, then let Q1 … Qn be the class of those closed prenex formulas with prefixes of the form (Q1x1)… (Qnxn). Our results may then be stated as follows:

Theorem 1. The decision problem for satisfiability is solvable for the class ∀∃∀ ∩ Kr.

Theorem 2. The classes ∀∃∀∀ ∩ Kr and ∀∀∃∀ ∩ Kr are reduction classes for satisfiability.

Maslov [11] showed that the class ∃…∃∀…∀∃…∃ ∩ Kr is solvable, while the first author [1, Corollary 4] showed ∃∀∃∀ ∩ Kr and ∀∃∃∀ ∩ Kr to be reduction classes. Thus the only prefix subclass of Kr for which the decision problem remains open is ∀∃∀∃…∃∩ Kr.

The class ∀∃∀ ∩ Kr, though solvable, contains formulas whose only models are infinite (e.g., (∀x)(∃u)(∀y)[(Pxy ∨ Pyx) ∧ (¬ Pxy ∨ ¬Pyu)], which can be satisfied over the integers by taking P to be ≥). This is not the case for Maslov's class ∃…∃∀…∀∃…∃ ∩ Kr, which contains no formula whose only models are infinite ([2] [5]).

Theorem 1 was announced in [1, Theorem 4], but the proof sketched there is defective: Lemma 4 (p. 17) is incorrectly stated. Theorem 2 was announced in [9].

Ackermann's set theory A* is usually formulated in the first order predicate calculus with identity, ∈ for membership and V, an individual constant, for the class of all sets. We use small Greek letters to represent formulae which do not contain V and large Greek letters to represent any formulae. The axioms of A* are the universal closures of

where all free variables are shown in A4 and z does not occur in the Θ of A2.

A+ is a generalisation of A* which Reinhardt introduced in [3] as an attempt to provide an elaboration of Ackermann's idea of “sharply delimited” collections. The language of A+ is that of A*'s augmented by a new constant V′, and its axioms are A1–A3, A5, V ⊆ V′ and the universal closure of

where all free variables are shown.

Using a schema of indescribability, Reinhardt states in [3] that if ZF + ‘there exists a measurable cardinal’ is consistent then so is A+, and using [4] this result can be improved to a weaker large cardinal axiom. It seemed plausible that A+ was stronger than ZF, but our main result, which is contained in Theorem 5, shows that if ZF is consistent then so is A+, giving an improvement on the above results.

Let T be a set of axioms for a classical theory TC (e.g. abelian groups, linear order, unary function, algebraically closed fields, etc.). Suppose we regard T as a set of axioms for an intuitionistic theory TH (more precisely, we regard T as axioms in Heyting's predicate calculus HPC).

Question. Is TH decidable (or, more generally, if X is any intermediate logic, is TX decidable)? In [1] we gave sufficient conditions for the undecidability of TH. These conditions depend on the formulas of T (different axiomatization of the same TC may give rise to different TH) and on the classical model theoretic properties of TC (the method did not work for model complete theories, e.g. those of the title of the paper). For details see [1]. In [2] we gave some decidability results for some theories: The problem of the decidability of theories TH for a classically model complete TC remained open. An undecidability result in this direction, for dense linear order was obtained by Smorynski [4]. The cases of algebraically closed fields and real closed fields and divisible abelian groups are treated in this paper. Other various decidability results of the intuitionistic theories were obtained by several authors, see [1], [2], [4] for details.

One more remark before we start. There are several possible formulations for an intuitionistic theory of, e.g. fields, that correspond to several possible axiomatizations of the classical theory. Other formulations may be given in terms of the apartness relation, such as the one for fields given by Heyting [5]. The formulations that we consider here are of interest as these systems occur in intuitionistic mathematics. We hope that the present methods could be extended to the (more interesting) case of Heyting's systems [5].

In this paper it is shown that, for any complete type Σ omitted in the structure , or in any expansion of having only countably many relations and operations, there is a proper elementary extension of (or of ) which omits Σ. This result (which was announced in [2]) is used to answer a question of Malitz on complete -sentences. The result holds also for countable families of types.

A type is a countable set of formulas with just the variable υ free. A structure is said to omit a type Σ if no element of satisfies all of the formulas of Σ. For example, omits the type Σω = {υ ≠ n: n ∈ ω}, since n fails to satisfy υ ≠ n. (Here n is the constant symbol standing for n.)

A type Σ is said to be complete with respect to a theory T if the set of sentences T ∪ Σ(e) generates a complete theory, where Σ(e) is the result of replacing υ by the new constant e in all of the formulas of Σ. The type Σω is clearly not complete with respect to Th(). (For any structure Th(), Th() is the set of all sentences true in .)

The jump a′ of a degree a is defined to be the largest degree recursively enumerable in a in the upper semilattice of degrees of unsolvability. We examine below some of the ways in which the jump operation is related to the partial ordering of the degrees. Fried berg [3] showed that the equation a = x′ is solvable if and only if a ≥ 0′. Sacks [13] showed that we can find a solution of a = x′ which is ≤ 0′ (and in fact is r.e.) if and only if a ≥ 0′ and is r.e. in 0′. Spector [16] constructed a minimal degree and Sacks [13] constructed one ≤ 0′. So far the only result concerning the relationship between minimal degrees and the jump operator is one due to Yates [17] who showed that there is a minimal predecessor for each non-recursive r.e. degree, and hence that there is a minimal degree with jump 0′. In §1, we obtain an analogue of Friedberg's theorem by constructing a minimal degree solution for a = x′ whenever a ≥ 0′. We incorporate Friedberg5s original number-theoretic device with a complicated sequence of approximations to the nest of trees necessary for the construction of a minimal degree. The proof of Theorem 1 is a revision of an earlier, shorter presentation, and incorporates many additions and modifications suggested by R. Epstein. In §2, we show that any hope for a result analogous to that of Sacks on the jumps of r.e. degrees cannot be fulfilled since 0″ is not the jump of any minimal degree below 0′. We use a characterization of the degrees below 0′ with jump 0″ similar to that found for r.e. degrees with jump 0′ by R. W. Robinson [12]. Finally, in §3, we give a proof that every degree a ≤ 0′ with a′ = 0″ has a minimal predecessor. Yates [17] has already shown that every nonzero r.e. degree has a minimal predecessor, but that there is a nonzero degree ≤ 0′ with no minimal predecessor (see [18]; or for the original unrelativized result see [10] or [4]).

The Fraenkel-Mostowski method has been widely used to prove independence results among weak versions of the axiom of choice. In this paper it is shown that certain statements cannot be proved by this method. More specifically it is shown that in all Fraenkel-Mostowski models the following hold:

1. The axiom of choice for sets of finite sets implies the axiom of choice for sets of well-orderable sets.

2. The Boolean prime ideal theorem implies a weakened form of Sikorski's theorem.

This paper is a survey and a synthesis of the various approaches to defining algebraic elements. Most of it is devoted to proving the following result.

Let T be a universal theory with the Amalgamation Property. Then for T the notions of algebraic element introduced by Robinson, Jónsson, and Morley are identical. Furthermore, they extend in a natural way the notion of algebraic element introduced by Park, and used by Lachlan and Baldwin and by Kueker.

In the course of proving this we shall construct the algebraic closure as a suitable injective hull and prove a unique factorisation theorem for algebraic predicates.

We shall also show (in §3) that if T is closed under products then algebraic elements all have degree 1. Thus in algebra, algebraic elements reduce to epimorphisms.

To demonstrate the remarkable stability of the notion we shall show (at the end of §5) that defining algebraic elements by infinitary formulas yields no new ones.

Let L be a language. The cardinality of the set of formulas of L is denoted by ∣L∣. An L-theory is a deductively closed set of L-sentences. We let denote the category of models of T and (L-structure) homomorphisms between them. If A is a substructure of B we write A ≤ B. We call u: A → B an injection if u is an isomorphism of A with a substructure of B, and let denote the subcategory of consisting of all injections.

With reservations, one can think of abstract algebra as the study of what consequences can be drawn from the axioms associated with certain concrete algebraic structures. Two important examples of such concrete algebraic structures are the integers and the rational numbers. The integers and the rational numbers have two properties which are not in general mirrored in the abstract axiom systems associated with them. That is, the integers and the rational numbers both have effectively computable metrics and their algebraic operations are effectively computable. The study of abstract algebraic systems which possess effectively computable algebraic operations has produced many interesting results. One can think of a computable algebraic structure as one whose elements have been labeled by the set of positive integers and whose operations are effectively computable. The formal definition of computable local integral domain will be given in §3. Some specific computable structures which have been studied are the integers, the rational numbers, and the rational numbers with p-adic valuation. Computable structures were studied in general by Rabin [12]. This paper concerns computable local integral domains as exemplified by the local integral domain Zp. Zp is the localization of the integers with respect to the maximal prime ideal generated by the positive prime p. We should note that the concept of local integral domain is not first order.

Let the ordered pair (Q, M) stand for a local ring, where Q is the local ring and M is the unique maximal prime ideal of Q. Since most of my results are proving the existence of certain effective procedures, the assumption that Q has a principal maximal ideal M (rather than M has n generators) greatly simplifies many of the proofs.