This note is a sequel to the previous paper of mine which was entitled Identity, variables, and impredicative definitions and published in this Journal, vol. 21 (1956), pp. 225–245. That early paper served to call attention to the dependency of the set-theoretic paradoxes on the interpretation of the variables that may occur in the critical abstraction principle:

where K is a well-formed formula containing free occurrences of y but not those of x.

A partial reinterpretation of the variables occurring in the above formalization of the abstraction principle yields Frege's unsuccessful way out of Russell's antinomy:

with the same kind of K as above. Another gives us the alternative schema

where K+ is obtained from a K of the kind described above by replacing every well-formed part of the form (∃z)L by (∃z)(z≠x & L) and every well-formed part of the form (z)L by (z)(z≠x ⊃ L). Still a third choice of an interpretation yields the schema

where K+ is subject to the same conditions as in (1) and z1, z2, …, zk are all the free variables of (2). These three interpretations are only some of the most conspicuous ones among a multitude of possible ways of interpreting the variables that may occur in the abstraction principle.

Varieties like groups, rings, or Boolean algebras have the property that, in any of their members, the lattice of congruences is isomorphic to a lattice of more manageable objects, for example normal subgroups of groups, two-sided ideals of rings, filters (or ideals) of Boolean algebras. Abstract algebraic logic can explain these phenomena at a rather satisfactory level of generality: in every member A of a τ-regular variety the lattice of congruences of A is isomorphic to the lattice of deductive filters on A of the τ-assertional logic of . Moreover, if has a constant 1 in its type and is 1-subtractive, the deductive filters on A ∈ of the 1-assertional logic of coincide with the -ideals of A in the sense of Gumm and Ursini, for which we have a manageable concept of ideal generation.

However, there are isomorphism theorems, for example, in the theories of residuated lattices, pseudointerior algebras and quasi-MV algebras that cannot be subsumed by these general results. The aim of the present paper is to appropriately generalise the concepts of subtractivity and τ-regularity in such a way as to shed some light on the deep reason behind such theorems. The tools and concepts we develop hereby provide a common umbrella for the algebraic investigation of several families of logics, including substructural logics, modal logics, quantum logics, and logics of constructive mathematics.

We prove the following theorem. Let G be a connected simple bad group (i.e. of finite Morley rank, nonsolvable and with all the Borel subgroups nilpotent) of minimal Morley rank. Then the Borel subgroups of G are conjugate to each other, and if B is a Borel subgroup of G, then , NG(B) = B, and G has no involutions.

For a finite von Neumann algebra factor M, the projections form a modular ortholattice L(M). We show that the equational theory of L(M) coincides with that of some resp. all L(ℂn×n ) and is decidable. In contrast, the uniform word problem for the variety generated by all L(ℂn×n) is shown to be undecidable.

It is well known that Gödel's famous undecidability result may be viewed in the following strong form. Suppose we are given a specific presentation (i.e., a specific formulation in terms of axioms and rules of inference) of number theory. Then there exists an effective method which, when applied to a consistent axiomatizable extension of the theory yields an undecidable sentence of this extension. For distinct presentations the undecidable sentences obtained would be distinct. This is because the sentence constructed depends upon the notion of proof and hence ultimately upon the axioms and rules of inference—i.e., upon the specific presentation.

In this paper, using definability of types over indiscernible sequences as a template, we study a property of formulas and theories called “uniform definability of types over finite sets” (UDTFS). We explore UDTFS and show how it relates to well-known properties in model theory. We recall that stable theories and weakly o-minimal theories have UDTFS and UDTFS implies dependence. We then show that all dp-minimal theories have UDTFS.

Let Γ be a class of subsets of Baire space (ωω) closed under inverse images by continuous functions. We say such a Γ is continuously closed. Let , the class dual to Γ, consist of the complements relative to ωω of members of Γ. If Γ is not selfdual, i.e., , then let . A continuously closed nonselfdual class Γ of subsets of ωΓ is said to have the first separation property [2] if

The set C is said to separate A and B. The class Γ is said to have the second separation property [3] if

We shall assume the axiom of determinateness and show that if Γ is a continuously closed class of subsets of ωω and then

(1) Γ has the first separation property iff does not have the second separation property, and

(2) either Γ or has the second separation property.

Of course, (1) and (2) taken together imply that Γ and cannot both have the first separation property.

We give an exponential lower bound on number of proof-lines in the proof system K of modal logic, i.e., we give an example of K-tautologies ψ1, ψ2, … s.t. every K-proof of ψi must have a number of proof-lines exponential in terms of the size of ψi. The result extends, for the same sequence of K-tautologies, to the systems K4, Gödel–Löb's logic, S andS4. We also determine some speed-up relations between different systems of modal logic on formulas of modal-depth one.

We introduce the notion of “semi-r.e.” for subsets of ω, a generalization of “semirecursive” and of “r.e.”, and the notion of “weakly semirecursive”, a generalization of “semi-r.e.”. We show that A is weakly semirecursive iff, for any n numbers x1, …,xn, knowing how many of these numbers belong to A is equivalent to knowing which of these numbers belong to A. It is shown that there exist weakly semirecursive sets that are neither semi-r.e. nor co-semi-r.e. On the other hand, we exhibit nonzero Turing degrees in which every weakly semirecursive set is semirecursive. We characterize the notion “A is weakly semirecursive and recursive in K” in terms of recursive approximations to A. We also show that if a finite Boolean combination of r.e. sets is semirecursive then it must be r.e. or co-r.e. Several open questions are raised.

The comprehension principle of second order arithmetic asserts the existence of certain species (sets) corresponding to properties of natural numbers. In the intuitionistic theory of sequences of natural numbers there is an analoguous principle, implicit in Brouwer's writing and explicitly stated by Kripke, which asserts the existence of certain sequences corresponding to statements. The justification of this principle, Kripke's Schema, makes use of the concept of the so-called creative subject. For more information the reader is referred to Troelstra [5].

Kripke's Schema reads

There is a weaker version

The idea to reduce species to sequences via Kripke's schema occurred several years ago (cf. [2, p. 128], [5, p. 104]). In [1] the reduction technique was applied in the construction of a model for HAS.

On second thought, however, I realized that there is a straightforward, simpler way to exploit Kripke's schema, avoiding models altogether. The idea to present this material separately was forced on the author by C. Smorynski.

Consider a second order arithmetic with both species and sequence variables. By KS we have

(for convenience we restrict ourselves in KS to 0-1-sequences). An application of AC-NF gives

Of course ξ is not uniquely determined. This is the key to the reduction of full second order arithmetic, or HAS, to a theory of sequences.

We now introduce a translation τ to eliminate species variables. It is no restriction to suppose that the formulae contain only the sequence variables ξ1, ξ3, ξ5, …

Note that by virtue of the definition of τ the axiom of extensionality is automatically verified after translation. The translation τ eliminates the species variables and leaves formulae without species variables invariant.

Let L be a first order language containing a binary relation symbol <.

Definition. Suppose ℳ is an L-structure and < is a total ordering of the domain of ℳ. ℳ is ordered minimal (-minimal) if and only if any parametrically definable X ⊆ ℳ can be represented as a finite union of points and intervals with endpoints in ℳ.

In any ordered structure every finite union of points and intervals is definable. Thus the -minimal structures are the ones with no unnecessary definable sets. If T is a complete L-theory we say that T is strongly (-minimal if and only if every model of T is -minimal.

The theory of real closed fields is the canonical example of a strongly -minimal theory. Strongly -minimal theories were introduced (in a less general guise which we discuss in §6) by van den Dries in [1]. Extending van den Dries' work, Pillay and Steinhorn (see [3], [4] and [2]) developed an extensive structure theory for definable sets in strongly -minimal theories, generalizing the results for real closed fields. They also established several striking analogies between strongly -minimal theories and ω-stable theories (most notably the existence and uniqueness of prime models). In this paper we will examine the construction of models of strongly -minimal theories emphasizing the problems involved in realizing and omitting types. Among other things we will prove that the Hanf number for omitting types for a strongly -minimal theory T is at most (2∣T∣)+, and characterize the strongly -minimal theories with models order isomorphic to (R, <).

Let ℝ be an o-minimal expansion of (ℝ, <, +) and (ϕ k )kЄℕ be a sequence of positive real numbers such that limtk →+∞ f (ϕ k )/ϕ k +1 = 0 for every f: ℝ → ℝ definable in ℜ (Such sequences always exist under some reasonable extra assumptions on ℜ, in particular, if ℜ is exponentially bounded or if the language is countable.) Then (ℜ, (S)) is d-minimal. where S ranges over all subsets of cartesian powers of the range of ϕ.

If two nonstandard models of complete arithmetic are elementarily embedded in a third, then their intersection may be considerably smaller than either of them; indeed, the intersection may be only the standard model. For example, if D and E are nonprincipal ultrafilters on ω, then the nonstandard models D-prod and E-prod (where is the standard model) have canonical elementary embeddings into D-prod (E-prod , and the intersection of their images is easily seen to be the (canonical image of the) standard model. In this paper, we shall prove that, under certain conditions, this phenomenon will not occur. Our main result (Theorem 3) is that the intersection of countably many pairwise cofinal models is itself cofinal with these models, provided that at least one of them is generated by a single element. (Precise definitions will be given below.)

The theorems in this paper were first formulated in terms of ultrafilters, then rephrased (using the methods of Chapter III of [1]) as statements about ultra-powers of , and finally generalized to their present form. Since the theorems and their proofs are now entirely model-theoretic, they are presented here separately from the study of ultrafilters in which they originated. That study, including applications of the present results, will appear in [2].

Let L be the first-order language whose n-place relation symbols are all the relations R ⊆; ωn and whose n-place function symbols are all the functions f: ωn → ω. Let be the standard model for L; its universe is ω and every nonlogical symbol of L denotes itself. Let be an elementary extension of . The relation (or function) denoted by R (or f) in will be called *R (or *f).

In 1978 Shelah introduced a new class of theories, called simple (see [Shi]) which properly contained the class of stable theories. Shelah generalized part of the theory of forking to the simple context. After approximately 15 years of neglecting the general theory (although there were works by Hrushovski on finite rank with a definability assumption, as well as deep results on specific simple theories by Cherlin, Hrushovski, Chazidakis, Macintyre and Van den dries, see [CH], [CMV], [HP1], [HP2], [ChH]) there was a breakthrough, initiated with the work of Kim ([K1]). Kim proved that almost all the technical machinery of forking developed in the stable context could be generalized to simple case. However, the theory of multiplicity (i.e., the description of the (bounded) set of non forking extensions of a given complete type) no longer holds in the context of simple theories. Indeed, by contrast to simple theories, stable theories share a strong amalgamation property of types, namely if p and q are two “free” complete extensions over a superset of A, and there is no finite equivalence relation over A which separates them, then the conjunction of p and q is consistent (and even free over A.) In [KP] Kim and Pillay proved a weak version of this property for any simple theory, namely “the Independence Theorem for Lascar strong types”. This was a weaker version both because of the requirement that the sets of parameters of the types be mutually independent, as well as the use of Lascar strong types instead of the usual strong types. A very fundamental and interesting problem is whether the independence theorem can be proved for any simple theory, using only the usual strong types. In 1997 Buechler proved ([Bu]) the strong-type version of the independence theorem for an important subclass of simple theories, namely the class of low theories (which includes the class of stable theories and the class of supersimple theories of finite D-rank.)

A well-known result, going back to the twenties, states that, under some reasonable assumptions, any logic can be characterized as the set of formulas satisfied by a matrix 〈, F〉, where is an algebra of the appropriate type, and F a subset of the domain of , called the set of designated elements. In particular, every quasi-classical modal logic—a set of modal formulas, containing the smallest classical modal logic E, which is closed under the inference rules of substitution and modus ponens—is characterized by such a matrix, where now is a modal algebra, and F is a filter of . If the modal logic is in fact normal, then we can do away with the filter; we can study normal modal logics in the setting of varieties of modal algebras. This point of view was adopted already quite explicitly in McKinsey and Tarski [8]. The observation that the lattice of normal modal logics is dually isomorphic to the lattice of subvarieties of a variety of modal algebras paved the road for an algebraic study of normal modal logics. The algebraic approach made available some general results from Universal Algebra, notably those obtained by Jónsson [6], and thereby was able to contribute new insights in the realm of normal modal logics [2], [3], [4], [10].

The requirement that a modal logic be normal is rather a severe one, however, and many of the systems which have been considered in the literature do not meet it. For instance, of the five celebrated modal systems, S1–S5, introduced by Lewis, S4 and S5 are the only normal ones, while only SI fails to be quasi-classical. The purpose of this paper is to generalize the algebraic approach so as to be applicable not just to normal modal logics, but to quasi-classical modal logics in general.

We give two examples. T0 has nine countable models and a nonprincipal 1-type which contains infinitely many 2-types. T1, has four models and an inessential extension T2 having infinitely many models.

We show how two iterated products of selection functions can both be used in conjunction with system T to interpret, via the dialectica interpretation and modified realizability, full classical analysis. We also show that one iterated product is equivalent over system T to Spector’s bar recursion, whereas the other is T-equivalent to modified bar recursion. Modified bar recursion itself is shown to arise directly from the iteration of a different binary product of ‘skewed’ selection functions. Iterations of the dependent binary products are also considered but in all cases are shown to be T-equivalent to the iteration of the simple products.

In this paper, we show that non-well-founded sets can be defined constructively by formalizing Hallnäs' limit definition of these within Martin-Löfs theory of types. A system is a type W together with an assignment of and to each ∝ ∈ W. We show that for any system W we can define an equivalence relation =w such that ∝ =w ß ∈ U and =w is the maximal bisimulation. Aczel's proof that CZF can be interpreted in the type V of iterative sets shows that if the system W satisfies an additional condition (*), then we can interpret CZF minus the set induction scheme in W. W is then extended to a complete system W* by taking limits of approximation chains. We show that in W* the antifoundation axiom AFA holds as well as the axioms of CFZ−.

J. R. Shoenfield conjectured in a talk at the Berkeley Model Theory Symposium (1963) that, if b and d are non-zero recursively enumerable (r.e.) degrees such that b < d then there exists an r.e. degree c such that c < d and b U c = d. G. E. Sacks echoed this conjecture at the end of [3]. In this paper the conjecture is disproved. We construct r.e. degrees b, d such that 0 < b < d and such that for no r.e. degree c is it true that c < d and b U c = d. We are grateful to G. E. Sacks for suggesting this problem.

One of the purposes of this paper is to prove a partial Schur-Zassenhaus Theorem for groups of finite Morley rank.

Theorem 2. Let G be a solvable group of finite Morley rank. Let π be a set of primes, and let H ⊲ G a normal π-Hall subgroup. Then H has a complement in G.

This result has been proved in [1] with the additional assumption that G is connected, and thought to be generalized in [2] by the authors of the present article. Unfortunately in the last section of the latter paper there is an irrepairable mistake. Here we give a new proof of the Schur-Zassenhaus Theorem using the results of [2] up to the last section and a new result that we are going to state below.

The second author has shown in [11] that a nilpotent ω-stable group is the central product of a divisible subgroup and a subgroup of bounded exponent, generalizing a well-known result of Angus Macintyre about abelian groups [8]. One could ask a similar question for solvable groups: are they a product of two subgroups, one divisible, one of bounded exponent? One is allowed to be hopeful because of the well-known decomposition of the connected solvable algebraic groups over algebraically closed fields as the product of the unipotent radical and a torus.