In Ockhamist branching-time logic [Prior 67], formulas are meant to be evaluated on a specified branch, or history, passing through the moment at hand. The linguistic counterpart of the manifoldness of future is a possibility operator which is read as ‘at some branch, or history (passing through the moment at hand)’. Both the bundled-trees semantics [Burgess 79] and the 〈moment, history〉 semantics [Thomason 84] for the possibility operator involve a quantification over sets of moments. The Ockhamist frames are (3-modal) Kripke structures in which this second-order quantification is represented by a first-order quantification. The aim of the present paper is to investigate the notions of modal definability, validity, and axiomatizability concerning 3-modal frames which can be viewed as generalizations of Ockhamist frames.

This is Part 1 of a paper on fibred semantics and combination of logics. It aims to present a methodology for combining arbitrary logical systems Li, i ∈ I, to form a new system LI. The methodology ‘fibres’ the semantics i of Li into a semantics for LI, and ‘weaves’ the proof theory (axiomatics) of Li into a proof system of LI. There are various ways of doing this, we distinguish by different names such as ‘fibring’, ‘dovetailing’ etc, yielding different systems, denoted by etc. Once the logics are ‘weaved’, further ‘interaction’ axioms can be geometrically motivated and added, and then systematically studied. The methodology is general and is applied to modal and intuitionistic logics as well as to general algebraic logics. We obtain general results on bulk, in the sense that we develop standard combining techniques and refinements which can be applied to any family of initial logics to obtain further combined logics.

The main results of this paper is a construction for combining arbitrary, (possibly not normal) modal or intermediate logics, each complete for a class of (not necessarily frame) Kripke models. We show transfer of recursive axiomatisability, decidability and finite model property.

Some results on combining logics (normal modal extensions of K) have recently been introduced by Kracht and Wolter, Goranko and Passy and by Fine and Schurz as well as a multitude of special combined systems existing in the literature of the past 20–30 years. We hope our methodology will help organise the field systematically.

The history of the Gentzenization of relevant logics goes back to Kripke [17], who in 1959 Gentzenized R→ and went on to prove its decidability. Formulae were separated by commas on the left side of the turnstile, the commas just representing nested implications. Kripke employed just a singleton formula to the right of the turnstile. He also considered adding negation, as well as other connectives, but it was not until 1961 that Belnap and Wallace, in [5], Gentzenized and proved its decidability, though their Gentzenization employed commas on both sides of the turnstile. Subsequently, in 1966, the logic R without distribution, now called LR (for lattice R), was Gentzenized in a similar style by Meyer in [20]. He also went on to show decidability for LR by extending Kripke's argument. Later, in 1969, Dunn Gentzenized R+ (published in [1], pp. 381–391) using two structural connectives (commas and semicolons) to the left of the turnstile, and with a single formula to the right. Here, the commas represent conjunction and the semicolons represent an intensional conjunction, called “fusion”. This is all nicely set out in McRobbie [19], where he also introduces left-handed Gentzenizations and analytic tableaux for a number of fragments of relevant logics. In 1979, further work on distributionless logic was done by Grishin, in a series of papers, including [16], in which he produced a Gentzenization of quantified RW without distribution (which we will call LRWQ), and used it to prove the decidability of this quantified logic.

Transitive extensional well founded relations provide an intuitionistic notion of ordinals which admits transfinite induction. However these ordinals are not directed and their successor operation is poorly behaved, leading to problems of functoriality.

We show how to make the successor monotone by introducing plumpness, which strengthens transitivity. This clarifies the traditional development of successors and unions, making it intuitionistic; even the (classical) proof of trichotomy is made simpler. The definition is, however, recursive, and, as their name suggests, the plump ordinals grow very rapidly.

Directedness must be defined hereditarily. It is orthogonal to the other four conditions, and the lower powerdomain construction is shown to be the universal way of imposing it.

We treat ordinals as order-types, and develop a corresponding set theory similar to Osius' transitive set objects. This presents Mostowski's theorem as a reflection of categories, and set-theoretic union is a corollary of the adjoint functor theorem. Mostowski's theorem and the rank for some of the notions of ordinal are formulated and proved without the axiom of replacement, but this seems to be unavoidable for the plump rank.

The comparison between sets and toposes is developed as far as the identification of replacement with completeness, and there are some suggestions for further work in this area.

Each notion of set or ordinal defines a free algebra for one of the theories discussed by Joyal and Moerdijk, namely joins of a family of arities together with an operation s satisfying conditions such as x ≤ sx, monotonicity or s(x ∨ y) ≤ sx ∨ sy.

Finally we discuss the fixed point theorem for a monotone endofunction s of a poset with least element and directed joins. This may be proved under each of a variety of additional hypotheses. We explain why it is unlikely that any notion of ordinal obeying the induction scheme for arbitrary predicates will prove the pure result.

We establish constructive refinements of several well-known theorems in elementary model theory. The additive group of the real numbers may be embedded elementarily into the additive group of pairs of real numbers, constructively as well as classically.

We study the model theory of fields k carrying a henselian valuation with real closed residue field. We give a criteria for elementary equivalence and elementary inclusion of such fields involving the value group of a not necessarily definable valuation. This allows us to translate theories of such fields to theories of ordered abelian groups, and we study the properties of this translation. We also characterize the first-order definable convex subgroups of a given ordered abelian group and prove that the definable real valuation rings of k are in correspondence with the definable convex subgroups of the value group of a certain real valuation of k.

Assuming determinacy, the model L[T2] does not depend on the choice of T2.

In Part I, we produced a Gentzenization L6LBQ of the distributionless relevant logic LBQ, which contained just the one structural connective ‘:’ and no structural rules. We compared it with the corresponding “right-handed” system and then proved interpolability and decidability of LBQ. Knowledge of Part I is presupposed.

In Part II of this paper, we will establish Gentzenizations, with appropriate interpolation and decidability results, for the further distributionless logics LDWQ, LTWQo, LEWQot, LRWQ, LRWKQ and LRQ, using essentially the same methods as were used for LBQ in Part I. LRWQ has been Gentzenized by Grishin [2], but the interpolation result is new and the decidability result is proved by a substantial simplification of his method. LR has been Gentzenized and shown to be decidable by Meyer in [5], by extending a method of Kripke in [3], and McRobbie has proved interpolation for it in [4], but here the Gentzenization and interpolation results are extended to quantifiers.

We axiomatize these logics as follows. The primitives and formation rules are as before, except that LTWQ and LEWQ require the extra primitive ‘o’, a 2-place connective (called ‘fusion’), and LEWQ also requires ‘t’, a sentential constant.

We show that the theory ATR0 is equivalent to a second-order generalization of the theory . As a result, ATR0 is conservative over for arithmetic sentences, though proofs in ATR0 can be much shorter than their counterparts.

Inspired by Pohlers' proof-theoretic analysis of KPω we give a straightforward non-metamathematical proof of the (well-known) classification of the provably total functions of PA, PA + TI(⊰ ↾) (where it is assumed that the well-ordering ⊰ has some reasonable closure properties) and KPω. Our method relies on a new approach to subrecursion due to Buchholz, Cichon and the author.

We establish cut-free left-handed Gentzenizations for a range of major relevant logics from B through to R, all with distribution. B is the basic system of the Routley-Meyer semantics (see [15], pp. 287–300) and R is the logic of relevant implication (see [1], p. 341). Previously, the contractionless logics DW, TW, EW, RW and RWK were Gentzenized in [3], [4] and [5], and also the distributionless logics LBQ, LDWQ, LTWQo, LEWQot, LRWQ, LRWKQ and LRQ in [6] and [7]. This paper provides Gentzenizations for the logics DJ, TJ, T and R, with various levels of contraction, and for the contractionless logic B, which could not be included in [4] using the technique developed there. We also include the Gentzenization of TW in order to compare it with that in [4]. The Gentzenizations that we obtain here for DW and RW are inferior to those already obtained in [4], but they are included for reference when constructing other systems. The logics EW and E present a difficulty for our method and are omitted. For background to the Gentzenization of relevant logics, see [6], and for motivation behind the logics involved, see [6], [1] and [15]. Because of the number of properties that are brought to bear in obtaining these systems, we prefer to consider Gentzenizations for particular logics rather than for arbitrary bunches of axioms.

The inverse of the distance between two structures ≢ of finite type τ is naturally measured by the smallest integer q such that a sentence of quantifier rank q − 1 is satisfied by but not by . In this way the space Strτ of structures of type τ is equipped with a pseudometric. The induced topology coincides with the elementary topology of Strτ. Using the rudiments of the theory of uniform spaces, in this elementary note we prove the convergence of every Cauchy net of structures, for any type τ.

The purpose of this note is to clarify two points about the topos Lif, introduced in [13] as a generalization of Lifschitz' realizability ([9, 12]). Lif is a subtopos of Hyland's Effective topos ([1]). The points I want to make are:

Remark 1. Lif is the largest subtopos of satisfying the axiom (O):

where denotes partial recursive application, and “∈ Tot” means that e and f range over codes for total recursive functions. One may read (O) as the statement “The union of two -sets is again a -set”. That is, let be a subtopos of . Then (O) is true in for the standard interpretation (the variables range over the natural numbers object of , etc.) if and only if the inclusion ↣ factors through the inclusion Lif ↣ .

Remark 2. Like , Lif contains at least two weakly complete internal full subcategories, thus providing us with more models of polymorphism and other impredicative type theories.

The principle (O) has some standing in the history of constructive mathematics:

- H. Friedman has proved that (O) is equivalent to a formulation of intuitionistic completeness of the intuitionistic predicate calculus for Tarskian semantics; see [8]. This is not to imply that this result is of immediate relevance to Lif: Friedman works in a system of analysis, a theory of lawless sequences with an axiom of “open data” for arithmetical formulas, which at least for the domain of all functions from N to N fails in Lif. However, there might exist a “nonstandard model” of arithmetic and a corresponding system of analysis, in which we may be able to carry out his proof.

- Moreover, Remark 2 entails that Lif should provide us with models of synthetic domain theory (for an exposition, see [3]), and one with the nice property that the dual of one of the axioms (axiom 7 in [3]) comes for free, by (O).

This paper was inspired by Lerman [15] in which he proved various properties of upper bounds for the arithmetical degrees. We discuss the complementation property of upper bounds for the arithmetical degrees. In Lerman [15], it is proved that uniform upper bounds for the arithmetical degrees are jumps of upper bounds for the arithmetical degrees. So any uniform upper bound for the arithmetical degrees is not a minimal upper bound for the arithmetical degrees. Given a uniform upper bound a for the arithmetical degrees, we prove a minimal complementation theorem for the upper bounds for the arithmetical degrees below a. Namely, given such a and b < a which is an upper bound for the arithmetical degrees, there is a minimal upper bound for the arithmetical degrees c such that b ∪ c = a. This answers a question in Lerman [15]. We prove this theorem by different methods depending on whether a has a function which is not dominated by any arithmetical function. We prove two propositions (see §1), of which the theorem is an immediate consequence.

Our notation is almost standard. Let A ⊕ B = {2n∣n ∈ A} ∪ {2n + 1∣n + 1∣n ∈ B} for any sets A and B. Let ω be the set of nonnegative natural numbers.

Let κ be an uncountable cardinal and the edges of a complete graph with κ vertices be colored with ℵ0 colors. For the Erdős-Rado theorem implies that there is an infinite monochromatic subgraph. However, if , then it may be impossible to find a monochromatic triangle. This paper is concerned with the latter situation. We consider the types of colorings of finite subgraphs that must occur when the edges of the complete graph on vertices are colored with ℵ0 colors. In particular, we are concerned with the case ℵ1 ≤ κ ≤ ℵω.

The study of these color patterns (known as identities) has a history that involves the existence of compactness theorems for two cardinal models [2]. When the graph being colored has size ℵ1, the identities that must occur have been classified by Shelah [4]. If the graph has size greater than or equal to ℵω the identities have also been classified in [3]. The number of colors is fixed at ℵ0 as it is the natural place to start and the results here can be generalized to situations where more colors are used.

There is one difference that we now make explicit. When countably many colors are used we can define the following coloring of the complete graph on vertices. First consider the branches in the complete binary tree of height ω to be vertices of a complete graph.

This paper is a continuation of Zakharyaschev [25], where the following basic results on modal logics with transitive frames were obtained:

• With every finite rooted transitive frame and every set of antichains (which were called closed domains) in two formulas α (, , ⊥) and α(, ) were associated. We called them the canonical and negation free canonical formulas, respectively, and proved the Refutability Criterion characterizing the constitution of their refutation general frames in terms of subreduction (alias partial p-morphism), the cofinality condition and the closed domain condition.

• We proved also the Completeness Theorem for the canonical formulas providing us with an algorithm which, given a modal formula φ, returns canonical formulas α(i, i), ⊥), for i = 1,…, n, such that

if φ is negation free then the algorithm instead of α(i, i, ⊥) can use the negation free canonical formulas α(i, i). Thus, every normal modal logic containing K4 can be axiomatized by a set of canonical formulas.

In this Part we apply the apparatus of the canonical formulas for establishing a number of results on the decidability, finite model property, elementarity and some other properties of modal logics within the field of K4.

Our attention will be focused on the class of logics which can be axiomatized by canonical formulas without closed domains, i.e., on the logics of the form

Adapting the terminology of Fine [11], we call them the cofinal subframe logics and denote this class by . As was shown in Part I, almost all standard modal logics are in .

Ackermann proved termination for a special order of reductions in Hilbert's epsilon substitution method for the first order arithmetic. We establish termination for arbitrary order of reductions.

An epistemic formalization of arithmetic is constructed in which certain non-trivial metatheoretical inferences about the system itself can be made. These inferences involve the notion of provability in principle, and cannot be made in any consistent extensions of Stewart Shapiro's system of epistemic arithmetic. The system constructed in the paper can be given a modal-structural interpretation

The Sacks Density Theorem [7] states that the Turing degrees of the recursively enumerable sets are dense. We show that the Density Theorem holds in every model of P− + BΣ2. The proof has two components: a lemma that in any model of P− + BΣ2, if B is recursively enumerable and incomplete then IΣ1 holds relative to B and an adaptation of Shore's [9] blocking technique in α-recursion theory to models of arithmetic.

We study the cardinal invariants of measure and category after adding one random real. In particular, we show that the number of measure zero subsets of the plane which are necessary to cover graphs of all continuous functions may be large while the covering for measure is small.