This paper presents a new technique for handling modal logics with transitive frames, i.e. extensions of the modal system K4. In effect, the technique is based on the following fundamental result, to be obtained below in §3.

Given a formula φ, we can effectively construct finite frames 1, …, n which completely characterize the set of all transitive general frames refuting φ. More exactly, an arbitrary general frame refutes φ iff contains a (not necessarily generated) subframe such that (1) i, for some i ϵ {1, …, n}, is a p-morphic image of (after Fine [1985] we say is subreducible to i), (2) is cofinal in , and (3) every point in that is not in does not get into “closed domains” which are uniquely determined in i, by φ.

This purely technical result has, as it turns out, rather unexpected and profound consequences. For instance, it follows at once that if φ determines no closed domains in the frames 1, …, n associated with it, then the normal extension of K4 generated by φ has the finite model property and so is decidable. Moreover, every normal logic axiomatizable by any (even infinite) set of such formulas φ also has the finite model property. This observation would not possibly merit any special attention, were it not for the fact that the class of such logics contains almost all the standard systems within the field of K4 (at least all those mentioned by Segerberg [1971] or Bull and Segerberg [1984]), all logics containing S4.3, all subframe logics of Fine [1985], and a continuum of other logics as well.

An algorithm recognizing admissibility of inference rules in generalized form (rules of inference with parameters or metavariables) in the intuitionistic calculus H and, in particular, also in the usual form without parameters, is presented. This algorithm is obtained by means of special intuitionistic Kripke models, which are constructed for a given inference rule. Thus, in particular, the direct solution by intuitionistic techniques of Friedman's problem is found. As a corollary an algorithm for the recognition of the solvability of logical equations in H and for constructing some solutions for solvable equations is obtained. A semantic criterion for admissibility in H is constructed.

In [2], Juhasz and Shelah use a forcing argument to show that it is consistent with GCH that there is a 0-dimensional T2 topological space X of cardinality ℵ3 such that every partition of the triples of X into countably many pieces has a nondiscrete (in the topology) homogeneous set. In this paper we will show how to construct such a space using a simplified (ω2, 1)-morass with certain additional structure added to it. The additional structure will be a slight strengthening of a built-in ◊ sequence, analogous to the strengthening of ordinary ◊k to ◊S for a stationary set S ⊆ k.

Suppose 〈〈θα∣ ∝ ≤ ω2〉, 〈∝β∣α < β ≤ ω2〉〉 is a neat simplified (ω2, 1)-morass (see [3]). Let ℒ be a language with countably many symbols of all types, and suppose that for each α < ω2, α is an ℒ-structure with universe θα. The sequence 〈α∣α < ω2 is called a built-in ◊ sequence for the morass if for every ℒ-structure with universe ω3 there is some α < ω2 and some f ∈αω2 such that f(α) ≺ , where f(α) is the ℒ-structure isomorphic to α under the isomorphism f. We can strengthen this slightly by assuming that α is only defined for α ∈ S, for some stationary set S ⊆ ω2. We will then say that is a built-in ◊ sequence on levels in S if for every ℒ-structure with universe ω3 there is some α ∈ S and some f ∈ αω2 such that f(α) ≺ .

In an ω1-saturated nonstandard universe a cut is an initial segment of the hyperinlegers which is closed under addition. Keisler and Leth in [KL] introduced, for each given cut U, a corresponding U-topology on the hyperintegers by letting O be U-open if for any x ϵ O there is a y greater than all the elements in U such that the interval [x − y, x + y] ⊆ O. Let U be a cut in a hyperfinite time line , which is a hyperfinite initial segment of the hyperintegers. U is called a good cut if there exists a U-meager subset of of Loeb measure one. Otherwise U is bad. In this paper we discuss the questions of Keisler and Leth about the existence of bad cuts and related cuts. We show that assuming b > ω1, every hyperfinite time line has a cut with both cofinality and coinitiality uncountable. We construct bad cuts in a nonstandard universe under ZFC. We also give two results about the existence of other kinds of cuts.

In an ω-saturated nonstandard universe a cut is an initial segment of the hyperintegers which is closed under addition. Keisler and Leth in [KL] introduced, for each given cut U, a corresponding U-topology on the hyperintegers by letting O be U-open if for any x ϵ O there is a y greater than all the elements in U such that the interval [x − y,x + y] ⊆ O. Let U be a cut in a hyperfinite time line , which is a hyperfinite initial segment of the hyperintegers. A subset B of is called a U-Lusin set in if B is uncountable and for any Loeb-Borel U-meager subset X of , B ⋂ X is countable. Here a Loeb-Borel set is an element of the σ-algebra generated by all internal subsets of : In this paper we answer some questions of Keisler and Leth about the existence of U-Lusin sets by proving the following facts. (1) If U = x/N = {y ϵ : ∀n ϵ ℕ(y < x/n)} for some x ϵ , then there exists a U-Lusin set of power κ if and only if there exists a Lusin set of the reals of power κ. (2) If U ≠ x/N but the coinitiality of U is ω, then there are no U-Lusin sets if CH fails. (3) Under ZFC there exists a nonstandard universe in which U-Lusin sets exist for every cut U with uncountable cofinality and coinitiality. (4) In any ω2-saturated nonstandard universe there are no U-Lusin sets for all cuts U except U = x/N.

Let be the least cardinal θ such that MAθ fails, (i.e. MA) implies that is regular. Models for regular with are easy to get (see [Ku1]). Fremlin and Miller proved that cof() > ω [Fr, 41C(d)]. The question of whether it is consistent that be singular was solved, in the affirmative, by Kunen [Ku1]. Kunen used a (θ, θ) strong gap in (ω)/Fin, whose splitting partial order is c.c.c. He showed that if cof(θ) = ω1, and P is a c.c.c. partial order of cardinality < θ that may destroy the strong gap, then there exists another c.c.c. partial order Q, which does not destroy the strong gap, and such that ⊩Q “P is not c.c.c”. One then gets Kunen's model by iterating c.c.c. partial orders of cardinality < θ, without destroying the strong (θ, θ) gap. It is unknown whether it is consistent to have ω1 < cof() < .

Clearly, there exists a c.c.c. partial order Q with ∣Q∣ = , such that (Q) = (see (1.1)). A partial order P is σ-centered iff P is the union of countably many centered subsets, where a subset A ⊆ P is centered iff p ≤ q. Clearly, a σ-centered partial order is c.c.c. Bell and Szymański proved that (σ-centered) is regular (see [Be] or [Fr, 14C], and [Fr, 21K] or [vD, 3.1(e)]). This implies that if P is a σ-centered partial order, and is singular, then (P) > . In particular, if is singular, then Q is not σ-centered and all c.c.c. partial orders of cardinality < have a Baire number (1.1) strictly greater than . It was suggested in [Ku1] to try and use Q(T) (1.2), where T is a tree with no ω1-branches, to get models with singular . It is well known that when T is such a tree, the forcing Q(T) is c.c.c. [BMR], ∣Q(T)∣ = ∣T∣, and if T is not special, then n(Q(T)) ≤ ∣T∣.

In this paper we discuss an interpretation of intuitionistic type theory in many-sorted arithmetic with so-called conditional application. Via the formulas-as-types correspondence the arithmetical system in turn can be embedded in ML, resulting in a characterization of strong Σ-elimination by an axiom of conditional choice.

We prove that there exists a function f which reduces a given subset P of an internal set X of an ω1 saturated nonstandard universe to the set WF of well-founded trees possessing properties similar to those possessed by the standard part map. We use f to define the Lusin-Sierpiński index of points in X, and prove the basic properties of that index using the classical properties of the Lusin-Sierpiński index. An example of a but not set is given.

In 1947 E. Post [28] and A. A. Markov [18] independently proved the undecidability of the word problem (or the problem of deducibility of relations) for semigroups. In 1968 V. L. Murskil [23] proved the undecidability of the identity problem (or the problem of deducibility of identities) in semigroups.

If we slightly generalize the statement of these results we can state many related results in the literature and state our new results proved here. Let V denote either a (Birkhoff) variety of semigroups or groups or a pseudovariety of finite semigroups. By a very well-known theorem a (Birkhoff) variety is defined by equations or equivalently closed under substructure, surmorphisms and all products; see [7]. It is also well known that V is a pseudovariety of finite semigroups iff V is closed under substructure, surmorphism and finite products, or, equivalently, determined eventually by equations w1 = w1′, w2 = w2′, w3 = w3′,… (where the finite semigroup S eventually satisfies these equations iff there exists an n, depending on S, such that S satisfies Wj = Wj′ for j ≥ n). See [8] and [29]. All semigroups form a variety while all finite semigroups form a pseudovariety.

We now consider a table (see the next page). In it, for example, the box denoting the “word” (identity) problem for the psuedovariety V” means, given a finite set of relations (identities) E and a relation (identity) u = ν, the problem of whether it is decidable that E implies u = ν inside V.

Ever since Cantor, we have known that the reals and the rationals are not isomorphic (as equality structures, i.e., sets). Logically speaking, however, they are not all that different; in first-order classical logic they are elementarily equivalent, since the theory of infinite sets is complete. The same holds for ℝ and ℚ as ordered sets; again the theory of dense linear order without end points is complete.

From an intuitionistic point of view these matters are more complicated; e.g., the theory of equality of ℚ is decidable, whereas the one of ℝ patently is not. This, in a roundabout way, shows that ℚ and ℝ are not isomorphic; of course, there is no need for such a detour, as Cantor's original proof [2] is intuitionistically correct, and Brouwer's new proof [1] is another alternative intuitionistic argument.

In view of the fact that ℚ and ℝ behave so strikingly differently with respect to first-order logic, one is easily tempted to look for elementary equivalences among the subsets of ℝ. Until quite recently most model theoretic investigations of intuitionistic theories made use of special (artificial) notions of “model”, e.g., Kripke models, sheaf models,…; but there is no prima facie reason why one should not practice model theory much the same way as traditional model theorists do. That is to say on the basis of a naive set theory, or, in our case, of naive intuitionistic mathematics.

This paper uses the method of (k, p)-isomorphisms of Fraïssé, and it is briefly shown that one half of the Fraïssé theorem holds intuitionistically.

Let KP− be the theory resulting from Kripke-Platek set theory by restricting Foundation to Set Foundation. Let G: V → V (V ≔ universe of sets) be a Δ0-definable set function, i.e. there is a Δ0-formula φ(x, y) such that φ(x, G(x)) is true for all sets x, and V ⊨ ∀x∃!yφ(x, y). In this paper we shall verify (by elementary proof-theoretic methods) that the collection of set functions primitive recursive in G coincides with the collection of those functions which are Σ1-definable in KP− + Σ1-Foundation + ∀x∃!yφ(x, y). Moreover, we show that this is still true if one adds Π1-Foundation or a weak version of Δ0-Dependent Choices to the latter theory.

In an ω1-saturated nonstandard universe a cut is an initial segment of the hyperintegers which is closed under addition. Keisler and Leth in [KL] introduced, for each given cut U, a corresponding U-topology on the hyperintegers by letting O be U-open if for any x ϵ O there is a y greater than all the elements in U such that the interval [x − y, x + y] ⊆ O. Let U be a cut in a hyperfinite time line , which is a hyperfinite initial segment of the hyperintegers. The U-monad topology of is the quotient topology of the U-topological space modulo U. In this paper we answer a question of Keisler and Leth about the U-monad topologies by showing that when is κ-saturated and has cardinality κ,(1) if the coinitiality of U1, is uncountable, then the U1,-monad topology and the U2-monad topology are homcomorphic iff both U1, and U2 have the same coinitiality; and (2) can produce exactly three different U-monad topologies (up to homeomorphism) for those U's with countable coinitiality. As a corollary can produce exactly four different U-monad topologies if the cardinality of is ω1.

A method is presented for constructing natural deduction-style systems for propositional relevant logics. The method consists in first translating formulas of relevant logics into ternary relations, and then defining deduction rules for a corresponding logic of ternary relations. Proof systems of that form are given for various relevant logics. A class of algebras of ternary relations is introduced that provides a relation-algebraic semantics for relevant logics.

The large cardinal-like properties of saturated ideals have been investigated by various authors, including Foreman [F], and Jech and Prikry [JP], among others. One of the most interesting consequences of a strongly compact cardinal is the following theorem of Solovay [So2]: if a strongly compact cardinal exists then the singular cardinal hypothesis holds above it. In this paper we discuss the question of relating the existence of saturated ideals and the singular cardinal hypothesis. We will show that the existence of “strongly” saturated ideals implies the singular cardinal hypothesis. As a biproduct we will present a proof of the above mentioned theorem of Solovay using generic ultrapowers. See Jech and Prikry [JP] for a nice exposition of generic ultrapowers. We owe a lot to the work of Foreman [F]. We would like to express our gratitude to Noa Goldring for many helpful comments and discussions.

Throughout this paper we assume that κ is a strongly inaccessible cardinal and λ is a cardinal >κ. By an ideal on κλ we mean a κ-complete fine ideal on Pκλ. For I an ideal on κλ let PI denote the poset of I-positive subsets of κλ.

Definition. Let I be an ideal on κλ. We say that I is a bounding ideal if 1 ⊩-PI “δ(δ is regular cardinal ”.

We can show that if a normal ideal is “strongly” saturated then it is bounding.

Theorem 1. If 1 is an η-saturated normal ideal onκλ, where η is a cardinal <λsuch that there are fewer thanκmany cardinals betweenκand η (i.e. η < κ+κ), then I is bounding.

Proof. Let I be such an ideal on κλ. By the work of Foreman [F] and others, we know that every λ+-saturated normal ideal is precipitous. Suppose G is a generic filter for our PI. Let j: V → M be the corresponding generic elementary embedding. By a theorem of Foreman [F, Lemma 10], we know that Mλ ⊂ M in V[G]. By η-saturation, cofinalities ≥η are preserved; that is, if cfvα ≥ η, then cfvα = cfv[G]α. From j ↾ Vκ being the identity on Vκ and M being λ-closed in V[G], we conclude that cofinalities <κ are preserved. Therefore if cfvα ≠ cfv[G]α then κ ≤ cfvα < η.

Let B be the random real forcing. Miller [Mi] asked if there are ZFC models M ⊆ N such that forcing with BM over N adds a dominating real. A YES answer was provided by Judah and Shelah in [JS], where in a long and sophisticated construction they built such models. In this paper we prove that forcing with BV over VI, where I is the infinitely often equal real forcing of [Mi], adds a dominating real over VI. This greatly simplifies the YES answer to Miller's question. Moreover it turns out that B may be replaced here by E, the eventually different real forcing of [Mi]. This answers the second part of Miller's question. We also prove that both side by side products I × B and I × E add a Hechler dominating real over V.

In this section we establish the main result of the paper; namely, we prove that forcing over VI with either of the posets BV or EV adds a dominating real over VI.

First we recall the definitions of I and E from [Mi]. The infinitely often equal real forcing is the set

ordered by extension. Miller [Mi] proves that I is ωω bounding.

In this paper, we continue the line of investigation undertaken in [HR], with which we assume familiarity. For a comprehensive reference we refer the reader to [P]. The authors would like to thank each other for their light spirit and good humor.

Pillay and Prest [PP, Proposition 7.10] have shown that a module M of U-rank 1 which is not totally transcendental may be decomposed as M = Ml ⊕ Mu, where Ml, ⊨ Th(M) omits the unlimited type and Mu imbeds purely into a model of the unlimited part Tu, of T = Th(M). We devote the first section of this paper to a generalization of this result to the case when T has a regular generic and m-dim(M) = 1. (Note that m-dim(M) = 0 implies M is totally transcendental, in which case a general decomposition theorem was proved by Garavaglia [G].)

In this paper we give an introduction to categorical proof theory, and reinterpret, with improvements, Läuchli's work on abstract realizability restricted to propositional logic (but see [M1] for predicate logic). Partly to make some points of a foundational nature, we have included a substantial amount of background material. As a result, the paper is (we hope) readable with a knowledge of just the rudiments of category theory, the notions of category, functor, natural transformation, and the like. We start with an extended introduction giving the background, and stating what we do with a minimum of technicalities.

In three publications [L1, 2, 3] published in the years 1968, 1969 and 1972, J. Lambek gave a categorical formulation of the notion of formal proof in deductive systems in certain propositional calculi. The theory is also described in the recent book [LS]. See also [Sz].

The basic motivation behind Lambek's theory was to place proof theory in the framework of modern abstract mathematics. The spirit of the latter, at least for the purposes of the present discussion, is to organize mathematical objects into mathematical structures. The specific kind of structure we will be concerned with is category.

In Lambek's theory, one starts with an arbitrary theory in any one of several propositional calculi. One has the (formal) proofs (deductions) in the given theory of entailments A ⇒ B, with A and B arbitrary formulas. One introduces an equivalence relation on proofs under which, in particular, equivalent proofs are proofs of the same entailment; equivalence of proofs is intended to capture the idea of the proofs being only inessentially different. One forms a category whose objects are the formulas of the underlying language of the theory, and whose arrows from A to B, with the latter arbitrary formulas, are the equivalence classes of formal proofs of A ⇒ B.

We prove that a stable solvable group G which satisfies xn = 1 generically is of finite exponent dividing some power of n. Furthermore, G is nilpotent-by-finile.

A second result is that in a stable group of finite exponent, involutions either have big centralisers, or invert a subgroup of finite index (which hence has to be abelian).

We improve results of Marczewski, Frankiewicz, Brown, and others comparing the ω-ideals of measure zero, meager, Marczewski measure zero, and completely Ramsey null sets; in particular, we remove CH from the hypothesis of many of Brown's constructions of sets lying in some of these ideals but not in others. We improve upon work of Marczewski by constructing, without CH, a nonmeasurable Marczewski measure zero set lacking the property of Baire. We extend our analysis of ω-ideals to include the completely Ramsey null sets relative to a Ramsey ultrafilter and obtain all 32 possible examples of sets in some ideals and not others, some under the assumption of MA, but most in ZFC alone. We also improve upon the known constructions of a Marczewski measure zero set which is not Ramsey by using a set theoretic hypothesis which is weaker than those used by other authors. We give several consistency proofs: one concerning the relative sizes of the covering numbers for the meager sets and the completely Ramsey null sets; another concerning the size of non; and a third concerning the size of add. We also study those classes of perfect sets which are bases for the class of always first category sets.

This paper answers some questions of D. Ross in [R]. In §1, we show that some consequences of the ℵ1- or ℵ1-special model axiom in [R] cannot be proved by the κ-isomorphism property for any cardinal κ. In §2, we show that with one exception, the ℵ0-isomorphism property does imply the remaining consequences of the special model axiom in [R]. In §3, we improve a result in [R] by showing that the κ-special model axiom is equivalent to the ℵ0-special model axiom plus κ-saturation.