In this paper the canonical modal logics, a kind of complete modal logics introduced in K. Fine [4] and R. I. Goldblatt [5], will be characterized semantically using the concept of an ultrafilter extension, an operation on frames inspired by the algebraic theory of modal logic. Theorem 8 of R. I. Goldblatt and S. K. Thomason [6] characterizing the modally definable Σ⊿-elementary classes of frames will follow as a corollary. A second corollary is Theorem 2 of [4] which states that any complete modal logic defining a Σ⊿-elementary class of frames is canonical.

The main tool in obtaining these results is the duality between modal algebras and general frames developed in R. I. Goldblatt [5]. The relevant notions and results from this theory will be stated in §2. The concept of a canonical modal logic is introduced and motivated in §3, which also contains the above-mentioned theorems. In §4, a kind of appendix to the preceding discussion, preservation of first-order sentences under ultrafilter extensions (and some other relevant operations on frames) is discussed.

The modal language to be considered here has an infinite supply of proposition letters (p, q, r, …), a propositional constant ⊥ (the so-called falsum, standing for a fixed contradiction), the usual Boolean operators ¬ (not), ∨ (or), ∨ (and), → (if … then …), and ↔ (if and only if)—with ¬ and ∨ regarded as primitives—and the two unary modal operators ◇ (possibly) and □ (necessarily)— ◇ being regarded as primitive. Modal formulas will be denoted by lower case Greek letters, sets of formulas by Greek capitals.

Vaught's “*-transform method” is applied to derive a global definability theorem of M. Makkai from a classical theorem of Lusin.

The language LA(Ⅎ) is formed by adding the quantifier Ⅎx, “few x”, to the infinitary logic LA on an admissible set A. A complete axiomatization is obtained for models whose universe is the set of ordinals of A and where Ⅎx is interpreted as there exist A-finitely many x. For well-behaved A, every consistent sentence has a model with an A-recursive diagram. A principal tool is forcing for LA(Ⅎ).

We improve a general theorem of J. A. Makowsky which characterizes, for a wide class of languages, those sentences θ such that both Mod(θ) and Mod(¬θ) are closed under unions of chains.

In order to prove that the Scott's interpolation theorem fails in Lω1ω, H. Africk proved the following lemma in [1]. (See [1] for notations.)

Africk's Lemma. Suppose that and . Then every -sentence in Lω1ω is equivalent to a sentence of the form and a sentence of the form , where Ai,j, Bi,j, are Fj-sentences and there are only countable distinct Ai,j or Bi,j together.

But this lemma is false as is shown in the following: Suppose that Z = {0,1}, Fj = {Pk,j}k⊂ω and . Let A be the sentence ⋀k⊂ω(∀xPk,0(x) ∨ ∀xPk,1(x)). If Africk's Lemma is true, then there are countably many Fj-sentences , such that A is equivalent to Since is countable, there are only countably many distinct pairs (Ai,0, Ai,1). So, we get a countable set {(Bi,0, Bi,1)}i⊂ω, such that A is equivalent to ⋁ik⊂ω(Bk,0 ∧ Bk,1). Since Bk,0 ∧ Bk,1 → ∀xPk,0(x) ∨ ∀xPk,1 is l-valid(i.e. valid in all first-order structures of cardinality 1) for every k ϵ ω, we have that either Bk,0 → ∀xPk,0(x) is 1-valid or Bk,0 → ∀xPk,1(x) is 1-valid. Let I be the set of all the k ϵ ω such that Bk,0 → ∀xPk,0(x) is 1-valid and the first-order structure defined by , , if k ϵ I and , if k ∉ I.

This paper compares the strength of two sorts of sentences of PA (classical first-order arithmetic with induction): reflection principles and sentences that may be called iterated consistency assertions.

Let Bew(x) be the standard provability predicate for PA, and for any sentence S of PA, let ⌈S⌉ be the numeral for the Gödel number of S. The reflection principle for S is the sentence Bew(⌈S⌉) → S, and a reflection principle is simply the reflection principle for some sentence. Nothing false (in the standard model for PA) is provable in PA, and therefore every reflection principle is true. Löb's theorem asserts that S is provable (in PA) if the reflection principle for S is provable.

We shall suppose that the 0-ary propositional connectives ⊤ and ⊥ are taken as primitives in the formulation of PA. We define the iterated consistency assertions Conm by: Con0 = ⊤; Conm−1 = − Bew(⌈ − Conm⌉). Con1 may be taken to be the sentence of PA that expresses the consistency of PA; Conn−1, the sentence that expresses the consistency of PA ⋃ {Conn}.

Our starting point is the observation that Con1 is equivalent (in PA) to the reflection principle for ⊥. (The second incompleteness theorem thus follows in a well-known way from Löb's theorem: if PA is consistent, then ⊥ is not provable, the reflection principle for ⊥ is not provable, and the consistency of PA is not provable either.)

We are interested in studying the length of the shortest proof of a propositional tautology in various proof systems as a function of the length of the tautology. The smallest upper bound known for this function is exponential, no matter what the proof system. A question we would like to answer (but have not been able to) is whether this function has a polynomial bound for some proof system. (This question is motivated below.) Our results here are relative results.

In §§2 and 3 we indicate that all standard Hilbert type systems (or Frege systems, as we call them) and natural deduction systems are equivalent, up to application of a polynomial, as far as minimum proof length goes. In §4 we introduce extended Frege systems, which allow introduction of abbreviations for formulas. Since these abbreviations can be iterated, they eliminate the need for a possible exponential growth in formula length in a proof, as is illustrated by an example (the pigeonhole principle). In fact, Theorem 4.6 (which is a variation of a theorem of Statman) states that with a penalty of at most a linear increase in the number of lines of a proof in an extended Frege system, no line in the proof need be more than a constant times the length of the formula proved.

Various equivalents and weakenings of the combinatorial principle ◊ are considered. The paper contains both absolute results and consistency results. Also included is a new characterisation of the notion of a stationary subset of ω1.

A structure is recursive if the set of quantifier-free sentences in the complete diagram ⊿() of is recursive. It has been known for some time that every decidable theory has a recursive model. In fact, every decidable theory has a decidable model (that is a model such that ⊿() is recursive). In this paper we find other conditions which imply that a theory have a recursive model.

In §1 we study the relation between an ℵ0-categorical theory T having a recursive model and the complexity of the quantificational hierarchy of that theory. We let ∃0 denote the set of quantifier-free sentences, and let ∃n÷1 denote the set of sentences beginning with an existential quantifier and having n alternations of quantifiers. (∀n is defined analogously.) Then we show that if T is an arithmetical ℵ0-categorical theory such that T ⋂ ∃n÷2 is Σn÷10 for each n < ω, then T has a recursive model. We show that this is a best possible result by giving an example of a ⊿n÷20 ℵ0-categorical theory T such that T ⋂ ∃n÷1 is recursive yet T has no recursive model.

In §2 we consider the theory of trees. Ershov [1] had proved that every Σ10 theory of trees has a recursive model. We show this to be best possible by giving an example of a ⊿20 theory of trees which has no recursive model.

This paper is mainly concerned with describing complete theories of modules by decomposing them (up to elementary equivalence) into direct products of simpler modules. In §1, I give a decomposition theorem which works for arbitrary direct product theories T. Given such a T, I define T-indecomposable structures and show that every model of T is elementarily equivalent to a direct product of T-indecomposable models of T. In §2, I show that if R is a commutative ring then every R-module is elementarily equivalent to ΠMM where M ranges over the maximal ideals of R and M is the localization of at M. This is applied to prove that if R is a commutative von Neumann regular ring and TR is the theory of R-modules then the TR-indecomposables are precisely the cyclic modules of the form R/M where M is a maximal ideal. In §3, I use the decomposition established in §2 to characterize the ω1-categorical and ω-stable modules over a countable commutative von Neumann regular ring and the superstable modules over a commutative von Neumann regular ring of arbitrary cardinality. In the process, I also prove several general characterizations of ω-stable and superstable modules; e.g., if R is any countable ring, then an R-moduIe is ω-stable if and only if every R-module elementarily equivalent to it is equationally compact.

A commutative ring R with identity is called a local ring if R has only one maximal ideal. This is equivalent to saying that the sum of two nonunits is a non-unit. Therefore the theory of all commutative local rings is axiomatizible by a finite set of A2-sentences. A commutative local ring with identity is said to be an algebraically closed local ring if every finite system of polynomial equations and inequations in one or more variables with coefficients in R which has a solution in some commutative local extension of R already has a solution in R. Much work connected with algebraically closed structures of classes of rings has been done, for example by Cherlin [2], Macintyre [4] and Lipschitz and Saracino [3]. We want to show similar results for commutative local rings with identity. Our main results are the following:

Theorem. The theory of commutative local rings with identity has no model-companion.

The finitely generic and infinitely generic local rings are algebraically closed local rings.

Theorem. There is an A3 sentence which holds for all finitely generic local rings whose negation holds in every infinitely generic local ring.

If A is an admissible set, let HC(A) = {x∣x ∈ A and x is hereditarily countable in A}. Then HC(A) is admissible. Corollaries are drawn characterizing the “real parts” of admissible sets and the analytical consequences of admissible set theory.

Originally generalized quantifiers were introduced to specify that a given formula was true for “many x's” e.g. ⊨ Qxφ(x) iff card{x ∈ ∣∣ ∣ ⊨ φ[x]} ≥ ℵ0, ℵ1, or some fixed cardinal κ. In this paper we formalize the notion that φ{x) is true “for almost all x”. This is accomplished by referring to structures = (′, μ) where ′ is a first-order structure and μ is a measure of a suitable type on the universe of ′. We will prove that the language Lμ obtained from first-order logic by adjoining a quantifier Qμ, which ranges over the measure μ, is fully compact if we assume the existence of a proper class of measurable cardinals. As a corollary to the compactness theorem we obtain the recursive enumerability of the validities of Lμ. Finally, the Magidor-Malitz quantifiers Qkn (n ∈ ω) will be added to Lμ together with analogous quantifiers Qμm (m ∈ ω) to form Lκμ<ω,<ω, which is compact for sets of sentences of cardinality < κ, where κ is a measurable cardinal > ℵ0.

An alternate approach to formalizing “for almost all” has been recently developed by Barwise, Kaufmann and Makkai [1] who follow a suggestion of Shelah [5].

Matatyahu Rubin pointed out that the proof of Lemma 6.1 [2] works only for rings of prime or zero characteristic. This invalidates the characterization of semiprime rings with the descending chain condition on right or left ideals which admit elimination of quantifiers given in [2] and cited in the abstract [1]. Although the correct characterization is easy to derive, it is complex to state.

Let be the class of finite fields. Let be the class of 2 × 2 matrix rings over a field with a prime number of elements. Let be the class of rings of the form GF(pn) ⊕ GF(pk) such that either n = k or g.c.d.(n, k) = 1 and p is a prime. Let ′ be the class of algebraically closed fields. Let P denote the set of all prime numbers together with zero. Let be the set of all ordered pairs (f, Q) where Q is a finite subset of P and f: Q → ⋃ ⋃ ⋃ such that the characteristic of the ring f(q) is q. Finally, let be the class of rings of the form ⊕q∈Qf(q) for some (f,Q) in .

A corrected version of Theorem 6.2 [2] is

Theorem 1. Let R be a ring with the descending chain condition on left or right ideals and without nonzero trivial ideals. Then R admits elimination of quantifiers if only if R belong to.

The elementary calculus of binary relations as developed by Tarski in [5] may be thought of as a certain part of the first-order predicate calculus. Though less expressive, its theory (i.e. the set of its valid sentences) was shown to be undecidable by Tarski in [6]. Translated into algebraic logic this means that the equational theory of the class of relation algebras is undecidable. Similarly it can be proved that the same holds for the (sub-) class of proper relation algebras.

The idea in Tarski's proof is to describe a pairing function by which any quantifier prefix may be contracted. In this note we apply a different method to treat the case of finite structures. We prove the

Theorem. The equational theory of the class of finite proper relation algebras is undecidable.

This result was announced in [4]. The main tool is representing the graph of primitive recursive functions via the cardinalities in finite simple models of equations.