This paper presents three generalizations of the Second Incompleteness Theorem of Gödel (see [2]) which apply to a broader class of formal systems than previous generalizations (as, e.g., the generalization in [1]).

The content of all three of our results is that it is versions of the third derivability condition of Hilbert and Bernays (see p. 286 of [3]) which are crucial to Gödel's theorem. The second derivability condition plays some role in certain logics, but even there, only in the far weaker form of a definability condition (see Theorem 2).

The elimination of the first derivability condition allows the application of the Consistency Theorem to cut-free logics which cannot prove that they are closed under cut.

It is Theorem 1 which will probably have primary interest for readers who are not concerned with technical proof theory or with foundations, for it treats logics with quantifiers, and in that case one can dispose entirely of the first and second derivability conditions. The derivation of this result requires a “new twist” on old arguments. Specifically, we use a new variation on the standard self-referential lemma (this is Lemma 5.1 of [l]) to obtain a somewhat different self-referential construction than has previously been employed (this is our lemma in §2 below). With this new construction, we consider the sentence φ which “expresses” the fact: “My negation is provable.” Then, using hypotheses associated with Gödel's First Incompleteness Theorem, one shows that ⊢¬φ is impossible in a consistent logic. Finally, using only a version of the third Hilbert-Bernays derivability condition, one shows that the provability of the consistency statement implies ⊢¬φ, and hence that consistency is unprovable.

Let α be an admissible ordinal and let L be the first order language with equality and a single binary relation ≤. The elementary theory of the α-degrees is the set of all sentences of L which are true in the universe of the α-degrees when ≤ is interpreted as the partial ordering of the α-degrees. Lachlan [6] showed that the elementary theory of the ω-degrees is nonaxiomatizable by proving that any countable distributive lattice with greatest and least members can be imbedded as an initial segment of the degrees of unsolvability. This paper deals with the extension of these results to α-recursion theory for an arbitrary countable admissible α > ω. Given α, we construct a set A with α-degree a such that every countable distributive lattice with greatest and least member is order isomorphic to a segment of α-degrees {d ∣ a ≤αd≤αb} for some α-degree b. As in [6] this implies that the elementary theory of the α-degrees is nonaxiomatizable and hence undecidable.

A is constructed in §2. A is a set of integers which is generic with respect to a suitable notion of forcing. Additional applications of such sets are summarized at the end of the section. In §3 we define the notion of a tree and construct a particular tree T0 which is weakly α-recursive in A. Using T0 we can apply the techniques of [6] and [2] to α-recursion theory. In §4 we reduce our main results to three technical lemmas concerning systems of trees. These lemmas are proved in §5.

The purpose of this paper is to give an axiom system for quantum logic. Here quantum logic is considered to have the structure of an orthomodular lattice. Some authors assume that it has the structure of an orthomodular poset.

In finding this axiom system the implication algebra given in Finch [1] has been very useful. Finch shows there that this algebra can be produced from an orthomodular lattice and vice versa.

Definition. An orthocomplementation N on a poset (partially ordered set) whose partial ordering is denoted by ≤ and which has least and greatest elements 0 and 1 is a unary operation satisfying the following:

(1) the greatest lower bound of a and Na exists and is 0,

(2) a ≤ b implies Nb ≤ Na,

(3) NNa = a.

Definition. An orthomodular lattice is a lattice with meet ∧, join ∨, least and greatest elements 0 and 1 and an orthocomplementation N satisfying

where a ≤ b means a ∧ b = a, as usual.

Definition. A Finch implication algebra is a poset with a partial ordering ≤, least and greatest elements 0 and 1 which is orthocomplemented by N. In addition, it has a binary operation → satisfying the following:

An orthomodular lattice gives a Finch implication algebra by defining → by

A Finch implication algebra can be changed into an orthomodular lattice by defining the meet ∧ and join ∨ by

The orthocomplementation is unchanged in both cases.

The partial order structure of degrees of unsolvability represented by continuous type-2 functional is a proper extension of the partial order structure of type-1 degrees.

It is well known that the hypothesis that all real numbers are constructible in the sense of Gödel [1] implies the existence of a Σ21 well-ordering of the Baire space [1, p. 67]. We are concerned with the converse to this theorem. From the assumption of the existence of a Σ21 well-ordering with total domain, we derive various consequences which in the presence of a nonconstructible real seem highly pathological. However, while several of these consequences are obviously absurd, none have as yet been disproven. Indeed some of the stranger consistency proofs of Jensen seem to indicate that there is a possibility that they may be consistent. I am referring to such results as existence of a model for ZF set theory in which the degrees of constructibility form a sequence of type ω + 1 with the (ω + 1)st degree being the only one which contains a nonconstructible real, and that degree being the degree of a Δ31 nonconstructible real.

In what follows we shall use the small Greek letters α, β, γ to range over the Baire space NN where N is the set of natural numbers. We assume that the reader is familiar with the use of trees to encode closed subsets of this space. The class Σ21 is the collection of all those subsets of the Baire space which can be defined by a formula which is Σ21 in a constructible parameter. Correspondingly Π21 will be taken to mean Π11 in a constructible parameter. The proof of the first lemma is left as an exercise. It involves nothing more than coding perfect sets by trees and then counting quantifiers.

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.

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.

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.

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 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.

Each of the various “large cardinal” axioms currently studied in set theory owes its inspiration to concrete phenomena in various fields. For example, the statement of the well-known compactness theorem for first-order logic can be generalized in various ways to infinitary languages to yield definitions of compact cardinals, and the reflection principles provable in ZF, when modified in the appropriate way, yields indescribable cardinals.

In this paper we concern ourselves with two kinds of large cardinals which are probably the two best known of those whose origins lie in model theory. They are the Rowbottom cardinals and the Jonsson cardinals.

Let us be more specific. A cardinal κ is said to be a Jonsson cardinal if every structure of cardinality κ has a proper elementary substructure of cardinality κ. (It is routine to see that only uncountable cardinals can be Jonsson. Erdös and Hajnal have shown [2] that for n < ω no ℵn is Jonsson. (In fact, they showed that if κ is not Jonsson then neither is the successor cardinal of κ and that, assuming GCH, no successor cardinal can be Jonsson.) Keisler and Rowbottom first showed that the existence of a Jonsson cardinal contradicts V = L.) The definition of a Rowbottom cardinal is only slightly more intricate. We assume for the moment that our similarity type has a designated one-place relation.

In this paper we prove that the word problem for division rings is recursively unsolvable. Our proof relies on the corresponding result for groups [7], [28], and makes essential use of P. M. Cohn's recent work [11], [13], [15], [16] on division rings.

The word problem for groups is usually formulated in terms of group presentations or finitely presented groups, as in [7], [24], [28], [30]. An equivalent formulation, in terms of the universal Horn sentences of group theory, is mentioned in [32]. This formulation makes sense for arbitrary first-order theories, and it is with respect to this formulation that we show that the word problem for division rings has degree 0′.

Let ω be the nonnegative integers. G. E. Sacks once asked whether there exists an infinite X ⊆ ω such that, for all Y ⊆ X, ω1Yω1 where ω1 is the first nonrecursive ordinal. In this note we negatively answer this question by giving a simple proof that for every infinite set X ⊆ ω there exists Y ⊆ X such that the first recursively inaccessible ordinal. This is accomplished by proving that Hα is hyper-arithmetic in Y whereHα is the αth hyperjump of the empty set ∅, defined in a suitable sense for all ordinals

Background information and undefined notation can be found in Rogers [11]. In particular, we write A ≤hB(A ≤T B) if A is hyperarithmetical (recursive) in B, and A ≡hB if A ≤hB and B ≤hA. We will say that a set A is hyperarithmetically (recursively) encodable if, for every infinite set X ⊆ ω, there exists Y ⊆ X such that A ≤hY (A ≤TY). For any set A (hyperdegree a) let A′ (a′) denote the hyperjump of A (a). Let 0 denote the hyperdegree of ∅. A function f majorizes a function g if f(n) ≥ g(n) for every n. E1 is the representing (type-2) functional of

introduced by Tugué [13] (also Kleene [6]). Let be the smallest ordinal which is not the order type of any well-ordering recursive in E1. Information on can be found in Richter [9] and [10].

The theorem proved in this paper answers some transitivity questions (in the geometric sense) for the type free λ-calculus: Which objects can be mapped on all other objects? How much can an object do by applying it to other objects (see footnote 2)?

The main result is that, for closed terms of the λI-calculus, the following conditions are equivalent:

(a) M has a normal form.

(b) FM = I for some λI-term F.

(c) MN1 … Nn = I for some λI-terms N1 …, Nn.

By the same method it follows that if M is a closed term of the λK-calculus having a normal form, then for some λI-terms (sic) N1, …, Nn, MN1… Nn = I is provable in the λK-calculus.

The theorem of Böhm [2] states that if M1, M2 are terms of the λK-calculus having different βη-normal forms, then ∀A1, A2 ∃N1, …, NnMiN1 … Nn = Ai is provable in the λK-βη-calculus for i = 1, 2. As a consequence of this it was shown (implicitly) in [1, 3.2.20 1/2 (1)] that if M has a normal form, then for some λK-terms N1, …, Nn, MN1 … Nn =I is provable in the λK-calculus.

It was not clear that this also could be proved for the λK-calculus since the proof of the theorem of Böhm essentially made use of λK-terms.

We conjecture that, using the results of this paper, the full theorem of Böhm can be proved for the λI-calculus.

A standard enumeration of the recursively enumerable (r.e.) sets is an acceptable numbering {Wn}n∈N of the r.e. sets in the sense of Rogers [5, p. 41], together with a 1:1 recursive function f with range In his quest for nonrecursive incomplete r.e. sets Post [4] constructed a hypersimple set Hf, relative to a fixed but unspecified standard enumeration f. Although it was later shown that hyper-simplicity does not guarantee incompleteness, the ironic possibility remained that Post's own particular hypersimple set might be incomplete. We settle the question by proving that H, may be either complete or incomplete depending upon which standard enumeration f is used. In contrast, D. A. Martin has shown [3] that Post's simple set S [4, p. 298] is complete for any standard enumeration. Furthermore, what most modern recursion theorists would regard as the “natural” construction of a hypersimple set (which we give in §1) is also complete for any standard enumeration.

There are two conclusions to be drawn from these results. First, they substantiate the often repeated remark among recursion theorists that Post's hypersimple set construction is a precursor of priority constructions because priorities play a strong role, and because there is a great deal of “restraint” which tends to keep elements out of the set. Secondly, the results warn recursion theorists that more properties than might have been supposed depend upon which standard enumeration is chosen at the beginning of the construction of some r.e. set.

In my paper [1], with which I assume the reader is familiar, I defined an arithmetic theory of constructions ATC and gave an interpretation of intuitionistic arithmetic HA in ATC. I proved that, in a suitable sense, every formula provable in HA is also provable in ATC. I proved the converse of this result only for positive sentences. In the present paper I will prove in full generality that any formula of HA which is provable in ATC is already provable in HA. In a later paper I shall use this result to obtain new information about certain extensions of HA by addition of higher types.

Let A be a countable admissible set (as defined in [1], [3]). The language LA consists of all infinitary finite-quantifier formulas (identified with sets, as in [1]) that are elements of A. Notationally, LA = A ∩ Lω1ω. Then LA is a countable subset of Lω1ω, the language of all infinitary finite-quantifier formulas with all conjunctions countable. The set is the set of Lω1ω sentences defined in 2.2 below. The following theorem characterizes those A-Σ1 sets Φ of LA sentences that have uncountable models.

Main Theorem (3.1.). If Φ is an A-Σ1set of LA sentences, then the following are equivalent:

(a) Φ has an uncountable model,

(b) Φ has a model with a proper LA-elementary extension,

(c) for every , ⋀Φ → C is not valid.

This theorem was announced in [2] and is proved in §§3, 4, 5. Makkai's earlier [4, Theorem 1] implies that, if Φ determines countable structure up to Lω1ω-elementary equivalence, then (a) is equivalent to (c′) for all , ⋀Φ → C is not valid.

The requirement in 3.1 that Φ is A-Σ1 is essential when the set ω of all natural numbers is an element of A. For by the example of [2], then there is a set Φ LA sentences such that (b) holds and (a) fails; it is easier to show that, if ω ϵ A, there is a set Φ of LA sentences such that (c) holds and (b) fails.

In this paper we consider classes of quantificational formulas specified by restrictions on the number of atomic subformulas appearing in a formula. Little seems to be known about the decision problem for such classes, except that the class whose members contain at most two distinct atomic subformulas is decidable [2]. (We use “decidable” and “undecidable” throughout with respect to satisfiability rather than validity. All undecidable problems to which we refer are of maximal r.e. degree.) The principal result of this paper is the undecidability of the class of those formulas containing five atomic subformulas and with prefixes of the form ∀∃∀…∀. In fact, we show the undecidability of two sub-classes of this class: one (Theorem 1) consists of formulas whose matrices are in disjunctive normal form with two disjuncts; the other (Corollary 1) consists of formulas whose matrices are in conjunctive normal form with three conjuncts. (Theorem 1 sharpens Orevkov's result [8] that the class of formulas in disjunctive normal form with two disjuncts is undecidable.) A second corollary of Theorem 1 shows the undecidability of the class of formulas with prefixes of the form ∀…∀∃, containing six atomic subformulas, and in conjunctive normal form with three conjuncts. These restrictions to prefixes ∀∃∀…∀ and ∀…∀∃ are optimal. For by a result of the first author [5], any class of prenex formulas obtained by restricting both the number of atomic formulas and the number of universal quantifiers is reducible to a finite class of formulas, and so each such class is decidable; and the class of formulas with prefixes ∃…∃∀…∀ is, of course, decidable.

The first section of this paper is concerned with the intrinsic properties of elementary monadic logic (EM), and characterizations in the spirit of Lindström [2] are given. His proofs do not apply to monadic logic since relations are used, and intrinsic properties of EM turn out to differ in certain ways from those of the elementary logic of relations (i.e., the predicate calculus), which we shall call EL. In the second section we investigate connections between higher-order monadic and polyadic logics.

EM is the subsystem of EL which results by the restriction to one-place predicate letters. We omit constants (for simplicity) but take EM to contain identity. Let a type be any finite sequence (possibly empty) of one-place predicate letters. A model M of type has a nonempty universe ∣M∣ and assigns to each predicate letter P of a subset PM of ∣M∣.

Let us take a monadic logic L to be any collection of classes of models, called L-classes, satisfying the following:

1. All models in a given L-class are of the same type (called the type of the class).

2. Isomorphic models lie in the same L-classes.

3. If and are L-classes of the same type, then and are L-classes.

The system , proposed without a claim as to its consistency in [CLg, §15C], has turned out to entail a consequence which is extremely suspicious. For from the axiom ⊦LH it follows that

holds for arbitrary X; hence for X ≡ YH, where Y is a fixed-point combinator, we have

Whether or not this leads to an actual contradiction it would be interesting to know; but, no matter whether it does or not, (2) seems highly counterintuitive.

The aim of this note is to point out that a related system, here called , is demonstrably consistent and sufficient for all practical purposes served by , and at the same time to correct an error in [CLg, §15D2], which was discovered too late to be corrected on the proofs. This is formed from by dropping H from the list of θ's, and hence deleting ⊦LH and (1). The new system does not allow inferential rules to be converted into formulas with the same ease as does ; but if one is content with stating the results as rules, is adequate for all the main results deduced for in [CLg, §15C–D].