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.

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.

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 τ.

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.

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.

The monadic second-order theory of trees allows quantification over elements and over arbitrary subsets. We classify the class of trees with respect to the question: does a tree T have a definable choice function (by a monadic formula with parameters)? A natural dichotomy arises where the trees that fall in the first class don't have a definable choice function and the trees in the second class have even a definable well ordering of their elements. This has a close connection to the uniformization problem.

Models of normal open induction are those normal discretely ordered rings whose nonnegative part satisfy Peano's axioms for open formulas in the language of ordered semirings. (Where normal means integrally closed in its fraction field.)

In 1964 Shepherdson gave a recursive nonstandard model of open induction. His model is not normal and does not have any infinite prime elements.

In this paper we present a recursive nonstandard model of normal open induction with an unbounded set of infinite prime elements.

In this paper we mainly study preservation theorems for two fragments of the infinitary languages Lκκ, with κ regular, without the equality symbol: the universal Horn fragment and the universal strict Horn fragment. In particular, when κ is ω, we obtain the corresponding theorems for the first-order case.

The universal Horn fragment of first-order logic (with equality) has been extensively studied; for references see [10], [7] and [8]. But the universal Horn fragment without equality, used frequently in logic programming, has received much less attention from the model theoretic point of view. At least to our knowledge, the problem of obtaining preservation results for it has not been studied before by model theorists. In spite of this, in the field of abstract algebraic logic we find a theorem which, properly translated, is a preservation result for the strict universal Horn fragment of infinitary languages without equality which, apart from function symbols, have only a unary relation symbol. This theorem is due to J. Czelakowski; see [5], Theorem 6.1, and [6], Theorem 5.1. A. Torrens [12] also has an unpublished result dealing with matrices of sequent calculi which, properly translated, is a preservation result for the strict universal Horn fragment of a first-order language. And in [2] of W. J. Blok and D. Pigozzi we find Corollary 6.3 which properly translated corresponds to our Corollary 19, but for the case of a first-order language that apart from its function symbols has only one κ-ary relation symbol, and for strict universal Horn sentences. The study of these results is the basis for the present work. In the last part of the paper, Section 4, we will make these connections clear and obtain some of these results from our theorems. In this way we hope to make clear two things: (1) The field of abstract algebraic logic can be seen, in part, as a disguised study of universal Horn logic without equality and so has an added interest. (2) A general study of universal Horn logic without equality from a model theoretic point of view can be of help in the field of abstract algebraic logic.

We give a solution stated in the title to problem 3 of part 1 of the problems listed in the book of Eklof and Mekler [2], p. 453. There, in pp. 241-242, this is discussed and proved in some cases. The existence of strongly λ-free ones was proved earlier by the criteria in [5] and [3]. We can apply a similar proof to a large class of other varieties in particular to the variety of (non-commutative) groups.

We prove:

Theorem. A complete first order theory in a countable language which is strictly stable, trivial and which admits finite coding hasnonisomorphic countable models.

Combined with the corresponding result or superstable theories from [4] our result confirms the Vaught conjecture for trivial theories which admit finite coding.

The study of infinitary Boolean operations was undertaken by the early researchers of descriptive set theory soon after Suslin's discovery of the important operation. The first attempt to lay down their theory in a systematic fashion was the work of Kantorovich and Livenson [5], where they call these the analytical operations. Earlier, Hausdorff had introduced the δs operations — essentially same as the monotoneω-ary Boolean operations, and Kolmogorov, independently of Hausdorff, had discovered the same objects, which were used in his study of the R operator.

The ω-ary Boolean operations turned out to be closely related to most of the classical hierarchies over a fixed Polish space X, including, e. g., the Borel hierarchy (), the difference hierarchies of Hausdorff (Dη()), the C-hierarchy (Cξ) of Selivanovski, and the projective hierarchy (): for each of these hierarchies, every level can be expressed as the range of an ω-ary Boolean operation applied to all possible sequences of open subsets of X. In the terminology of Dougherty [3], every level is “open-ω-Boolean” (if and are collections of subsets of X and I is any set, is said to be -I-Boolean if there exists an I-ary Boolean operation Φ such that = Φ, i. e. is the range of Φ restricted to all possible I-sequences of sets from ). If in addition, the space X has a basis consisting of clopen sets, then the levels of the above hierarchies are also “clopen-ω-Boolean.”

If T has only countably many complete types, yet has a type of infinite multiplicity then there is a c.c.c. forcing notion such that, in any -generic extension of the universe, there are non-isomorphic models M1 and M2 of T that can be forced isomorphic by a c.c.c. forcing. We give examples showing that the hypothesis on the number of complete types is necessary and what happens if ‘c.c.c’ is replaced by other cardinal-preserving adjectives. We also give an example showing that membership in a pseudo-elementary class can be altered by very simple cardinal-preserving forcings.

In [1], we established Gentzenizations for a good range of relevant logics with distribution, but, in the process, we added inversion rules, which involved extra structural connectives, and also added the sentential constant t. Instead of eliminating them, we used conservative extension results to relate them back to the original logics. In [4], we eliminated the inversion rules and t and established a much simpler Gentzenization for the weak sentential relevant logic DW, and also for its quantificational extension DWQ, but a restriction to normal formulae (defined below) was required to enable these results to be proved. This method was quite general and hope was expressed about extending it to other relevant logics.

In this paper, we develop an innovative method, which makes essential use of this restriction to normality, to establish two simple Gentzenizations for the normal formulae of the slightly weaker logic B, and then extend the method to other sentential contraction-less logics. To obtain the first of these Gentzenizations, for the logics B and DW, we remove the two branching rules (F&) and (T∨), together with the structural connective ‘,’, to simplify the elimination of the inversion rules and t. We then eliminate the rules (T&) and (F∨), thus reducing the Gentzen system to one containing only ˜ and → and their four associated rules, and reduce the remaining types of structures to four simple finite types. Subsequently, we re-introduce (T&) and (F∨), and also (F&) and (T∨), to obtain the second Gentzenization, which contains ‘,’ but no structural rules.

We prove that there exists a noncappable enumeration degree strictly below 0e′.

We show that the Π20 enumeration degrees are not dense. This answers a question posed by Cooper.

It is unprovable that every complete subalgebra of a countably closed complete Boolean algebra is countably closed.