We extend the characterization of extremal valued fields given in [2] to the missing case of valued fields of mixed characteristic with perfect residue field. This leads to a complete characterization of the tame valued fields that are extremal. The key to the proof is a model theoretic result about tame valued fields in mixed characteristic. Further, we prove that in an extremal valued field of finite p-degree, the images of all additive polynomials have the optimal approximation property. This fact can be used to improve the axiom system that is suggested in [8] for the elementary theory of Laurent series fields over finite fields. Finally we give examples that demonstrate the problems we are facing when we try to characterize the extremal valued fields with imperfect residue fields. To this end, we describe several ways of constructing extremal valued fields; in particular, we show that in every ℵ1 saturated valued field the valuation is a composition of extremal valuations of rank 1.

In [13], M. Tokarz specified some infinite family of consequence operations among all ones associated with the relevant logic RM or with the extensions of RM and proved that each of them admits a deduction theorem scheme. In this paper, we show that the family is complete in a sense that if C is a consequence operation with CRM ≤ C and C admits a deduction theorem scheme, then C is equal to a consequence operation specified in [13]. In algebraic terms, this means that the only quasivarieties of Sugihara algebras with the relative congruence extension property are the quasivarieties corresponding, via the algebraization process, to the consequence operations specified in [13].

Kleene [5] mentions two ways of extending the constructive ordinals. The first is by relativizing the set O of notations for the constructive ordinals, using fundamental sequences which are partial recursive in O. In this way we obtain the set OO which provides notations for the ordinals less than ω1O. Continuing the process, the sequence O, OO, , … and the corresponding ordinals are obtained. A second possibility is to define (constructive) higher number classes in which partial recursive functions are used at limit ordinals to provide an “accessibility” mapping from a previously defined number class. The relationship between the ordinals obtained by the two methods of extension has been an open problem. Methods developed in this article are used to show that the two ways of extending the constructive ordinals are equivalent, provided the sets of notations for the higher number classes satisfy certain natural conditions. Equivalence is obtained, not only with respect to ordinals, but also with respect to the forms of the sets of notations for the higher number classes. Specifically, the fundamental fact that the sets of notations for the constructive ordinals are complete Π11 sets generalizes to suitably defined higher number classes. As an application we prove that the ordinals of the Addison and Kleene [1] constructive third number class are exactly the ordinals less than ω1O and the set of notations for their third number class is recursively isomorphic to OO.

In the paper Mathematics of infinity, Martin-Löf extends his intuitionistic type theory with fixed “choice sequences”. The simplest, and most important instance, is given by adding the axioms

to the type of natural numbers. Martin-Löf's type theory can be regarded as an extension of Heyting arithmetic (HA). In this note we state and prove Martin-Löf's main result for this choice sequence, in the simpler setting of HA and other arithmetical theories based on intuitionistic logic (Theorem A). We also record some remarkable properties of the resulting systems; in general, these lack the disjunction property and may or may not have the explicit definability property. Moreover, they represent all recursive functions by terms.

The language of propositional modal logic is extended by the introduction of sequents. Validity of a modal sequent on a frame is defined, and modal sequent-axiomatic classes of frames are introduced. Through the use of modal algebras and general frames, a study of the properties of such classes is begun.

One of the most interesting concepts arising from the study of L(V∞), the lattice of r.e. subspaces of a fully effective vector space of infinite dimension (cf. [6], [7] or [10]), was that of a supermaximal subspace. Supermaximal subspaces of V∞ were those with the fewest possible r.e. superspaces, that is, we say M ∈ L(L∞) is supermaximal if dim(V∞/M) = ∞ and for all Q ∈ L(V∞) with Q ⊇ M, either dim(Q/M) < ∞ or Q = V∞. These spaces were particularly interesting because they had no natural analogue in L(ω), the lattice of r.e. sets. Later Metakides and Nerode [8], Baldwin [1] and the author [2] found that supermaximal substructures occurred in more general settings. In particular, they were found to occur in L(F∞), the lattice of r.e. algebraically closed subfields of F∞ (a recursively presented field of infinite transcendence degree) (cf. [3]). The main tool in these later papers was the concept of a Steinitz (closure) system with recursive dependence (cf. [1], [2], [4] or [8]). We assume familiarity with the definitions and basic results of Metakides and Nerode [8], and only give a brief sketch of some nonstandard facts in §2. If the reader is not familiar with Steinitz systems he is advised to either obtain [1] or [2], or simply identify a Steinitz system (U, cl) with (V∞, *), that is, he should identify U with V∞, and cl(A) with A*, the subspace generated by A.

Recently, Gitik, Kanovei and the first author proved that for a classical Prikry forcing extension the family of the intermediate models can be parametrized by /finite. By modifying the standard Prikry tree forcing we define a Prikry-type forcing which also singularizes a measurable cardinal but which is minimal, i.e., there are no intermediate models properly between the ground model and the generic extension. The proof relies on combining the rigidity of the tree structure with indiscernibility arguments resulting from the normality of the associated measures.

We introduce the safe recursive set functions based on a Bellantoni–Cook style subclass of the primitive recursive set functions. We show that the functions computed by safe recursive set functions under a list encoding of finite strings by hereditarily finite sets are exactly the polynomial growth rate functions computed by alternating exponential time Turing machines with polynomially many alternations. We also show that the functions computed by safe recursive set functions under a more efficient binary tree encoding of finite strings by hereditarily finite sets are exactly the quasipolynomial growth rate functions computed by alternating quasipolynomial time Turing machines with polylogarithmic many alternations.

We characterize the safe recursive set functions on arbitrary sets in definability-theoretic terms. In its strongest form, we show that a function on arbitrary sets is safe recursive if and only if it is uniformly definable in some polynomial level of a refinement of Jensen's J-hierarchy, relativized to the transitive closure of the function's arguments.

We observe that safe recursive set functions on infinite binary strings are equivalent to functions computed by infinite-time Turing machines in time less than ωω. We also give a machine model for safe recursive set functions which is based on set-indexed parallel processors and the natural bound on running times.

We take a fixed countable model M0, and we look at the structure of and number of its countable elementary extensions (up to isomorphism over M0). Assuming that S(M0) is countable, we prove that if N is a weakly minimal extension of , and if then there is an elementary embedding of N into M over M0), then N is homogeneous over M0. Moreover the condition that ∣S(M0)∣ = ℵ0 cannot be removed. Under the hypothesis that M0 contains no infinite set of tuples ordered by a formula, we prove that M0 has infinitely many countable elementary extensions up to isomorphism over M0. A preliminary result is that all types over M0 are definable, and moreover is definable over M0 if and only if is definable over M0 (forking symmetry). We also introduce a notion of relative homogeneity, and show that a large class of elementary extensions of M0 are relatively homogeneous over M0 (under the assumptions that M0 has no order and S(M0) is countable).

I will now discuss the background to and motivation behind the results in this paper, and also the place of this paper relative to other conjectures and investigations. To simplify notation let T denote the complete diagram of M0. First, our result that if M0 has no order then T has infinitely many countable models is related to the following conjecture: any theory with a finite number (more than one) of countable models is unstable.

We are concerned here with the set theory given in [1], which we call BL (Bernays-Levy). This theory can be given an elegant syntactical presentation which allows most of the usual axioms to be deduced from the reflection principle. However, it is more convenient here to take the usual Von Neumann-Bernays set theory [3] as a starting point, and to regard BL as arising from the addition of the schema

where S is the formal definition of satisfaction (with respect to models which are sets) and ┌φ┐ is the Gödel number of φ which has a single free variable X.

We study the relationship between the semistationary reflection principle and stationary reflection principles. We show that for all regular cardinals λ ≥ ω2 the semistationary reflection principle in the space [λ]ω implies that every stationary subset of ≔ {α ∈ λ ∣ cf(α) = ω} reflects. We also show that for all cardinals λ ≥ ω3 the semistationary reflection principle in [λ]ω does not imply the stationary reflection principle in [λ]ω.

We prove that a combinatorial consequence of the negation of the PCF conjecture for intervais, involving free subsets relative to set mappings, is not implied by even the strongest known large cardinal axiom.

This paper is a sequel to our earlier paper [2] entitled Saturation and simple extensions of models of Peano arithmetic. Among other things, we will answer some of the questions that were left open there. In §1 we consider the question of whether there are lofty models of PA which have no recursively saturated, simple extensions. We are still unable to answer this question; but we do show in that section that these models are precisely the lofty models which are not recursively saturated and which are κ-like for some regular κ. In §2 we use diagonal methods to produce minimal models of PA in which the standard cut is recursively definable, and other minimal models in which the standard cut is not recursively definable. In §3 we answer two questions from [2] by exhibiting countable models of PA which, in the terminology of this paper, are uniformly ω-lofty but not continuously ω-lofty and others which are continuously ω-lofty but not recursively saturated. We also construct a model (assuming ◇) which is not recursively saturated but every proper, simple cofinal extension of which is ℵ1-saturated. Finally, in §4 we answer another question from [2] by proving that for regular κ ≥ ℵ1; every κ-saturated model of PA has a κ-saturated proper, simple extension which is not κ +-saturated.

Our notation and terminology are quite standard. Anything unfamiliar to the reader and not adequately denned here is probably defined in §1 of [2]. All models considered are models of Peano arithmetic.

This paper deals with locales and their spaces of points in intuitionistic analysis or, if you like, in (Grothendieck) toposes. One of the important aspects of the problem whether a certain locale has enough points is that it is directly related to the (constructive) completeness of a geometric theory. A useful exposition of this relationship may be found in [1], and we will assume that the reader is familiar with the general framework described in that paper.

We will consider four formal spaces, or locales, namely formal Cantor space C, formal Baire space B, the formal real line R, and the formal function space RR being the exponential in the category of locales (cf. [3]). The corresponding spaces of points will be denoted by pt(C), pt(B), pt(R) and pt(RR). Classically, these locales all have enough points, of course, but constructively or in sheaves this may fail in each case. Let us recall some facts from [1]: the assertion that C has enough points is equivalent to the compactness of the space of points pt(C), and is traditionally known in intuitionistic analysis as the Fan Theorem (FT). Similarly, the assertion that B has enough points is equivalent to the principle of (monotone) Bar Induction (BI). The locale R has enough points iff its space of points pt(R) is locally compact, i.e. the unit interval pt[0, 1] ⊂ pt(R) is compact, which is of course known as the Heine-Borel Theorem (HB). The statement that RR has enough points, i.e. that there are “enough” continuous functions from R to itself, does not have a well-established name. We will refer to it (not very imaginatively, I admit) as the principle (EF) of Enough Functions.

Modifying the methods of Z. Adamowicz's paper Herbrand consistency and bounded arithmetic [3] we show that there exists a number n such that ⋃mSm (the union of the bounded arithmetic theories Sm) does not prove the Herbrand consistency of the finitely axiomatizable theory S3n

We show that in the language of { ≤ }. the Π3-fragment of the first order theory of the -enumeration degrees is undecidable. We then extend this result to show that the Π3-theory of any substructure of the enumeration degrees which contains the -degrees is undecidable.

Reverse mathematics uses subsystems of second order arithmetic to determine which set existence axioms are required to prove particular theorems. Surprisingly, almost every theorem studied is either provable in RCA0 or equivalent over RCA0 to one of four other subsystems: WKL0, ACA0, ATR0 or – CA0. Of these subsystems, – CA0 has the fewest known equivalences. This article presents a new equivalence of – C0 which comes from ordered group theory.

One of the fundamental problems about ordered groups is to classify all possible orders for various classes of orderable groups. In general, this problem is extremely difficult to solve. Mal'tsev [1949] solved a related problem by showing that the order type of a countable ordered group is ℤαℚε where ℤ is the order type of the integers, ℚ is the order type of the rationals, α is a countable ordinal, and ε is either 0 or 1. The goal of this article is to prove that this theorem is equivalent over RCA0 to – CA0.

In Section 2, we give the basic definitions and notation for RCA0, ACA0 and CA0 as well as for ordered groups. For more information on reverse mathematics, see Friedman, Simpson, and Smith [1983] or Simpson [1999] and for ordered groups, see Kokorin and Kopytov [1974] or Fuchs [1963]. Our notation will follow these sources. In Section 3, we show that – CA0 suffices to prove Mal'tsev's Theorem and the reversal is done over RCA0 in Section 4.

Relevance logic began in an attempt to avoid the so-called fallacies of relevance. These fallacies can be in implicational form or in deductive form. For example, Lewis's first paradox can beset a system in implicational form, in that the system contains as a theorem the formula (A & ∼A) → B; or it can beset it in deductive form, in that the system allows one to deduce B from the premisses A, ∼A.

Relevance logic in the tradition of Anderson and Belnap has been almost exclusively concerned with characterizing a relevant conditional. Thus it has attacked the problem of relevance in its implicational form. Accordingly for a relevant conditional → one would not have as a theorem the formula (A & ∼A) → B. Other theorems even of minimal logic would also be lacking. Perhaps most important among these is the formula (A → (B → A)). It is also a well-known feature of their system R that it lacks the intuitionistically valid formula ((A ∨ B) & ∼A) → B (disjunctive syllogism).

But it is not the case that any relevance logic worth the title even has to concern itself with the conditional, and hence with the problem in its implicational form. The problem arises even for a system without the conditional primitive. It would still be an exercise in relevance logic, broadly construed, to formulate a deductive system free of the fallacies of relevance in deductive form even if this were done in a language whose only connectives were, say, &, ∨ and ∼. Solving the problem of relevance in this more basic deductive form is arguably a precondition for solving it for the conditional, if we suppose (as is reasonable) that the relevant conditional is to be governed by anything like the rule of conditional proof.

Work in the setting of the recursively enumerable sets and their Turing degrees. A set X is low if X′, its Turing jump, is recursive in ∅′ and high if X′ computes ∅″. Attempting to find a property between being low and being recursive, Bickford and Mills produced the following definition. W is deep, if for each recursively enumerable set A, the jump of A ⊕ W is recursive in the jump of A. We prove that there are no deep degrees other than the recursive one.

Given a set W, we enumerate a set A and approximate its jump. The construction of A is governed by strategies, indexed by the Turing functionals Φ. Simplifying the situation, a typical strategy converts a failure to recursively compute W into a constraint on the enumeration of A, so that (W ⊕ A)′ is forced to disagree with Φ(−;A′). The conversion has some ambiguity; in particular, A cannot be found uniformly from W.

We also show that there is a “moderately” deep degree: There is a low nonzero degree whose join with any other low degree is not high.

It is known that both S4 and the Intuitionistic prepositional calculus Int are P-SPACE complete. This guarantees that there is a polynomial translation from each system into the other.

However, no sound and faithful polynomial translation from S4 into Int is commonly known. The problem of finding one was suggested by Dana Scott during a very informal gathering of logicians in February 2005 at UCLA. Grigori Mints then brought it to my attention, and in this paper I present a solution. It is based on Kripke semantics and describes model-checking for S4 using formulas of Int.

A simple translation from Int into S4, the Gödel-Tarski translation, is wellknown; given a formula φ of Int, one obtains by prefixing □ to every subformula. For example,

.

That the translation is sound and faithful can be seen by considering topological semantics, which assign open sets both to □-formulas of S4 and arbitrary formulas of Int; the interpretation of φ and turn out to be identical. See Tarski's paper [6] for details. Gödel's original paper can be found in [3].

In [2], Friedman and Flagg present a kind of inverse to Gödel-Tarski. Given a formula φ of S4 and a finite set of formulas Γ of Int, for each ε ∈ Γ one gets an intuitionistic formula given recursively by