Margaris has shown1 that for every triple 〈s,t,m〉 of integers such that 1 ≦ s < t < m it is possible to construct a formalisation of an m-valued propositional calculus satisfying the following conditions: I. Every statement which takes only truth-values belonging to the set {1, …,s} is provable. II. Every provable statement takes only truth-values belonging to the set {1, …, t}. III. There exist statements Pk, Qk which take only truth-values belonging to the set {1, …, k) and neither of which takes only truth-values belonging to the set {1, …, k—1} such that Pk is provable and Qk is unprovable (k = s+1, …, t). The systems of Margaris are all functionally incomplete and he appears to suggest2 that it is impossible to construct functionally complete systems having the required properties.

Let a be an admissible ordinal and let ∧ ≤ α be a limit ordinal. A sequence of a-r.e. degrees is said to be ascending, simultaneous and of length ∧ if (i) there is an α-recursive function t: α × ∧ → α such that, for all ϒ < ∧, A ϒ = {t(σ, ϒ)∣ σ < α} is of degree a ϒ; (ii) if ϒ < ⊤ < ∧, then a ϒ ≤α a τ and (iii) for all ϒ < ∧, there is a ⊤ > ϒ with a ϒ, >α a ϒ. Lerman [4] showed that such an exists for every ∧ ≤ α. An upper bound a of is an α-r.e. degree in which every element of is α-recursive. a is minimal if there is no α-r.e. degree b <α a which is also an upper bound of . Sacks [6] proved that every ascending sequence of simultaneously ω-r.e. degrees of length ω cannot have 0ω′, the complete ω-r.e. degree, as a minimal upper bound. In contrast, Cooper [2] showed that there exists an ascending sequence of simultaneously ω-r.e. degrees of length to having a minimal upper bound which is an ω-r.e. degree. In this paper we investigate the behavior of ascending sequences of simultaneously α-r.e. degrees for admissible ordinals α > ω. Call α Σ∞-admissibIe if it is Σ n -nadmissible for all n. Let Φ(∧) say: No ascending sequence of simultaneously α-r.e. degrees of length ∧ can have 0α′, the complete α-r.e. degree, as a minimal upper bound. Our main result in this paper is:

Let α be either a constructible cardinal with σ2ci(α) < α or Σ∞-admissible. Then σ2cf(α) is the least ordinal ν for which every ∧ ≤ α of cofinality ν (over L α) can satisfy Φ(∧).

In [1] Ludwik Borkowski takes a quantifier symbol ‘Q1’ (e.g., the familiar ‘∀’) to permit definition of another quantifier symbol ‘Q1’ if, where ‘f’ is a singulary predicate variable, there exists a formula A of QC1—a first-order quantificational calculus (without identity and individual constants) having ‘Q1’ as its one primitive quantifier symbol—such that: (1) under the intended interpretations of ‘Q1’ and ‘Q1’ the biconditional (Q1X)f(X) = A is valid, (2) no individual variable occurs free in A, and (3) A contains no propositional variable, and no predicate variable other than ‘f.’

In [7] it is shown that if Σ is a type omitted in the structure = ω, +, ·, < and complete with respect to Th() then Σ is omitted in models of Th() of all infinite powers. The proof given there extends readily to other models of P. In this paper the result is extended to models of ZFC. For pre-tidy models of ZFC, the proof is a straightforward combination of the methods in [7] and in Keisler and Morley ([9], [6]). For other models, the proof involves forcing. In particular, it uses Solovay and Cohen's original forcing proof that GB is a conservative extension of ZFC (see [2, p. 105] and [5, p. 77]).

The method of proof used for pre-tidy models of set theory can be used to obtain an alternate proof of the result for This new proof yields more information. First of all, a condition is obtained which resembles the hypothesis of the “Omitting Types” theorem, and which is sufficient for a theory T to have a model omitting a type Σ and containing an infinite set of indiscernibles. The proof that this condition is sufficient is essentially contained in Morley's proof [9] that the Hanf number for omitting types is so the condition will be called Morley's condition.

If T is a pre-tidy theory, Morley's condition guarantees that T will have models omitting Σ in all infinite powers.

We introduce and study (weakly) semi-equational theories, generalizing equationality in stable theories (in the sense of Srour) to the NIP context. In particular, we establish a connection to distality via one-sided strong honest definitions; demonstrate that certain trees are semi-equational, while algebraically closed valued fields are not weakly semi-equational; and obtain a general criterion for weak semi-equationality of an expansion of a distal structure by a new predicate.

We refine results of Gannon [6, Theorem 4.7] and Simon [22, Lemma 2.8] on convergence of Morley sequences. We then introduce the notion of eventual$NIP$, as a property of a model, and prove a variant of [15, Corollary 2.2]. Finally, we give new characterizations of generically stable types (for countable theories) and reinforce the main result of Pillay [17] on the model-theoretic meaning of Grothendieck’s double limit theorem.

We present sound and complete sequent calculi for the modal mu-calculus with converse modalities, aka two-way modal mu-calculus. Notably, we introduce a cyclic proof system wherein proofs can be represented as finite trees with back-edges, i.e., finite graphs. The sequent calculi incorporate ordinal annotations and structural rules for managing them. Soundness is proved with relative ease as is the case for the modal mu-calculus with explicit ordinals. The main ingredients in the proof of completeness are isolating a class of non-wellfounded proofs with sequents of bounded size, called slim proofs, and a counter-model construction that shows slimness suffices to capture all validities. Slim proofs are further transformed into cyclic proofs by means of re-assigning ordinal annotations.

Strengthening a theorem of Hjorth this paper gives a new characterization of which Polish groups admit compatible complete left invariant metrics. As a corollary it is proved that any Polish group without a complete left invariant metric has a continuous action on a Polish space whose associated orbit equivalence relation is not essentially countable.

In 1930, A. Heyting first specified a formal system for part of intuitionistic mathematics. Although his rules were presumably motivated by the “intended interpretation” or meaning of the logical symbols, over the years a number of other possible interpretations have been discovered for which the rules are also valid. In particular, one might mention the realizablity interpretation of Kleene, the (Dialectica) interpretation of Gödel, and various semantic interpretations, such as Kripke models. (Each of these has several variants or close relatives.) Each such interpretation can be regarded as defining precisely a certain “notion of constructivity”, the study of which may illuminate the still rather vague notions which underlie the intended interpretation; or, if one doubts that there is a single interpretation “intended” by all constructivist mathematicians, the study of precisely defined interpretations may help to delineate and distinguish the possibilities.

In the last few years, Heyting's systems have been vastly extended, in order to encompass the large and growing body of constructive mathematics. Several kinds of new systems have been put forward and studied. The present author has extended the various realizability interpretations to several of these systems [B1], [B2] and drawn a number of interesting applications. The mathematical content of the present paper is an interpretation in the style of Godel's Dialectica interpretation, but applicable to the new systems put forward by Feferman [Fl]. The original motivation for this work was to obtain certain metamathematical applications: roughly speaking, Markov's rule and its variants.

We give upper and lower bounds for the consistency strength of the failure of a combinatorial principle introduced by Jensen. Square on singular cardinals.