Hybrid languages are expansions of propositional modal languages which can refer to (or even quantify over) worlds. The use of strong hybrid languages dates back to at least [Pri67], but recent work (for example [BS98, BT98a, BT99]) has focussed on a more constrained system called H(↓, @). We show in detail that (↓, @) is modally natural. We begin by studying its expressivity, and provide model theoretic characterizations (via a restricted notion of Ehrenfeucht-Fraïssé game, and an enriched notion of bisimulation) and a syntactic characterization (in terms of bounded formulas). The key result to emerge is that (↓, @) corresponds to the fragment of first-order logic which is invariant for generated submodels. We then show that (↓, @) enjoys (strong) interpolation, provide counterexamples for its finite variable fragments, and show that weak interpolation holds for the sublanguage (@). Finally, we provide complexity results for (@) and other fragments and variants, and sharpen known undecidability results for (↓, @).

The Jensen covering lemma says that either L has a club class of indiscernibles, or else, for every uncountable set A of ordinals, there is a set B ∈ L with A ⊆ B and card (B) = card(A). One might hope to extend Jensen's covering lemma to richer core models, which for us will mean to inner models of the form L[] where is a coherent sequence of extenders of the kind studied in Mitchell-Steel [8], The papers [8], [12], [10] and [1] show how to construct core models with Woodin cardinals and more. But, as Prikry forcing shows, one cannot expect too direct a generalization of Jensen's covering lemma to core models with measurable cardinals.

Recall from [8] that if L[] is a core model and α is an ordinal, then either Eα = ∅, or else Eα is an extender over As in [8], we assume here that if Eα is an extender, then Eα is below superstrong type in the sense that the set of generators of Eα is bounded in (crit(Eα)). Let us say that L[] is a lower-part core model iff for every ordinal α, Eα is not a total extender over L[]. In other words, if L[] is a lower-part core model, then no cardinal in L[] is measurable as witnessed by an extender on . Other than the “below superstrong” hypothesis, we impose no bounds on the large cardinal axioms true in the levels of a lower-part core model.

We study the proof–theoretic strength and effective content of the infinite form of Ramsey's theorem for pairs. Let RTkn denote Ramsey's theorem for k–colorings of n–element sets, and let RT<∞n denote (∀k)RTkn. Our main result on computability is: For any n ≥ 2 and any computable (recursive) k–coloring of the n–element sets of natural numbers, there is an infinite homogeneous set X with X″ ≤T 0(n). Let IΣn and BΣn denote the Σn induction and bounding schemes, respectively. Adapting the case n = 2 of the above result (where X is low2) to models of arithmetic enables us to show that RCA0 + IΣ2 + RT22 is conservative over RCA0 + IΣ2 for Π11 statements and that RCA0 + IΣ3 + RT<∞2 is Π11-conservative over RCA0 + IΣ3. It follows that RCA0 + RT22 does not imply BΣ3. In contrast, J. Hirst showed that RCA0 + RT<∞2 does imply BΣ3, and we include a proof of a slightly strengthened version of this result. It follows that RT<∞2 is strictly stronger than RT22 over RCA0.

We show that for every c.e. degree a > 0 there exists an intrinsically c.e. relation on the domain of a computable structure whose degree spectrum is {0, a}. This result can be extended in two directions. First we show that for every uniformly c.e. collection of sets S there exists an intrinsically c.e. relation on the domain of a computable structure whose degree spectrum is the set of degrees of elements of S. Then we show that if α ∈ ω ∪ {ω} then for any α-c.e. degree a > 0 there exists an intrinsically α-c.e. relation on the domain of a computable structure whose degree spectrum {0, a}. All of these results also hold for m-degree spectra of relations.

We give a sound and complete axiomatization for the full computation tree logic. CTL*, of R-generable models. This solves a long standing open problem in branching time temporal logic.

This paper presents a new correctness criterion for marked Danos-Reginer graphs (D-R graphs, for short) of Multiplicative Cyclic Linear Logic MCLL and Abrusci's non-commutative Linear Logic MNLL.

As a corollary we obtain an affirmative answer to the open question whether a known quadratic-time algorithm for the correctness checking of proof nets for MCLL and MNLL can be improved to linear-time.

We consider Borel sets of finite rank A ⊆ ∧ω where cardinality of Λ is less than some uncountable regular cardinal . We obtain a “normal form” of A, by finding a Borel set Ω, such that A and Ω continuously reduce to each other. In more technical terms: we define simple Borel operations which are homomorphic to ordinal sum, to multiplication by a countable ordinal, and to ordinal exponentiation of base , under the map which sends every Borel set A of finite rank to its Wadge degree.

Slaman and Wehner have constructed structures which distinguish the computable Turing degree 0 from the noncomputable degrees, in the sense that the spectrum of each structure consists precisely of the noncomputable degrees. Downey has asked if this can be done for an ordinary type of structure such as a linear order. We show that there exists a linear order whose spectrum includes every noncomputable degree, but not 0. Since our argument requires the technique of permitting below a set, we include a detailed explantion of the mechanics and intuition behind this type of permitting.

Call a set A n-correctable if every set Turing reducible to A via a Turing machine that on any input makes at most n queries is Turing reducible to A via a Turing machine that on any input makes at most n-queries and on any input halts no matter what answers are given to its queries. We show that if a c.e. set A is n-correctable for some n ≥ 2, then it is n-correctable for all n. We show that this is the optimal such result by constructing a c.e. set that is 1-correctable but not 2-correctable. The former result is obtained by examining the logical closure properties of c.e. sets that are 2-correctable.

The purpose of this paper is to present a kind of boundedness lemma for direct limits of coarse structural mice, and to indicate some applications to descriptive set theory. For instance, this allows us to show that under large cardinal or determinacy assumptions there is no prewellorder ≤ of length such that for some formula ψ and parameter z

if and only if

It is a peculiar experience to write up a result in this area. Following the work of Martin, Steel, Woodin, and other inner model theory experts, there is an enormous overhang of theorems and ideas, and it only takes one wandering pebble to restart the avalanche. For this reason I have chosen to center the exposition around the one pebble at 1.7 which I believe to be new. The applications discussed in section 2 involve routine modifications of known methods.

A detailed introduction to many of the techniques related to using the Martin-Steel inner model theory and Woodin's free extender algebra is given in the course of [1]. Certainly a familiarity with the Martin-Steel papers, [5] and [6], is a prerequisite, as is some knowledge of the free extender algebra. Probably anyone interested in this paper will already know the necessary descriptive set theory, most of which can be found in [4]. Discussion of earlier results in this direction can be found in [3] or [2].

This paper discusses a sequence of extensions of NFU, Jensen's improvement of Quine's set theory “New Foundations” (NF) of [16].

The original theory NF of Quine continues to present difficulties. After 60 years of intermittent investigation, it is still not known to be consistent relative to any set theory in which we have confidence. Specker showed in [20] that NF disproves Choice (and so proves Infinity). Even if one assumes the consistency of NF, one is hampered by the lack of powerful methods for proofs of consistency and independence such as are available for use with ZFC; very clever work has been done with permutation methods, starting with [18] and [5], and exemplified more recently by [14], but permutation methods can only be applied to show the consistency or independence of unstratified sentences (see the definition of NFU below for a definition of stratification). For example, there is no method available to determine whether the assertion “the continuum can be well-ordered” is consistent with or independent of NF. There is one substantial independence result for an assertion with nontrivial stratified consequences, using metamathematical methods: this is Orey's proof of the independence of the Axiom of Counting from NF (see below for a statement of this axiom).

We mention these difficulties only to reassure the reader of their irrelevance to the present work. Jensen's modification of “New Foundations” (in [13]), which was to restrict extensionality to sets, allowing many non-sets (urelements) with no elements, has almost magical effects.

Working in Z + KP, we give a new proof that the class of hereditarily finite sets cannot be proved to be a set in Zermelo set theory, extend the method to establish other failures of replacement, and exhibit a formula Φ(λ, a) such that for any sequence ⟨Aλ ∣ λ a limit ordinal⟩ where for each λ. Aλ ⊆ λ2, there is a supertransitive inner model of Zermelo containing all ordinals in which for every λAλ = {a ∣ Φ(λ, a)}.

A first-order sentence is quasi-modal if its class of models is closed under the modal validity preserving constructions of disjoint unions, inner substructures and bounded epimorphic images.

It is shown that all members of the proper class of canonical structures of a modal logic Λ have the same quasi-modal first-order theory ΨΛ. The models of this theory determine a modal logic Λe which is the largest sublogic of Λ to be determined by an elementary class. The canonical structures of Λe also have ΨΛ as their quasi-modal theory.

In addition there is a largest sublogic Λe of Λ that is determined by its canonical structures, and again the canonical structures of Λe have ΨΛ are their quasi-modal theory. Thus . Finally, we show that all finite structures validating Λ are models of ΨΛ, and that if Λ is determined by its finite structures, then ΨΛ is equal to the quasi-modal theory of these structures.

Pure Type Systems. PTSs, introduced as a generalisation of the type systems of Barendregt's lambda-cube, provide a foundation for actual proof assistants, aiming at the mechanic verification of formal proofs. In this paper we consider simplifications of some of the rules of PTSs. This is of independent interest for PTSs as this produces more flexible PTS-like systems, but it will also help, in a later paper, to bridge the gap between PTSs and systems of Illative Combinatory Logic.

First we consider a simplification of the start and weakening rules of PTSs. which allows contexts to be sets of statements, and a generalisation of the conversion rule. The resulting Set-modified PTSs or SPTSs, though essentially equivalent to PTSs, are closer to standard logical systems.

A simplification of the abstraction rule results in Abstraction-modified PTSs or APTSs. These turn out to be equivalent to standard PTSs if and only if a condition (*) holds. Finally we consider SAPTSs which have both modifications.

An infinite structure is said to be minimal if each of its definable subset is finite or cofinite. Modifying Hrushovski's method we construct minimal, non strongly minimal structures with arbitrary finite dimensions. This answers negatively to a problem posed by B. I Zilber.

In this paper first order theories for nonmonotone inductive definitions are introduced, and a proof-theoretic analysis for such theories based on combined operator forms à la Richter with recursively inaccessible and Mahlo closure ordinals is given.

We consider the following question of Kunen:

Does Con(ZFC + ∃M a transitive inner model and a non-trivial elementary embedding j: M → V)

imply Con(ZFC + ∃ a measurable cardinal)?

We use core model theory to investigate consequences of the existence of such a j: M → V. We prove, amongst other things, the existence of such an embedding implies that the core model K is a model of “there exists a proper class of almost Ramsey cardinals”. Conversely, if On is Ramsey, then such a j. M are definable.

We construe this as a negative answer to the question above. We consider further the consequences of strengthening the closure assumption on j to having various classes of fixed points.

In this paper, we show by a proof-theoretical argument that in a logic without structural rules, that is in noncommutative linear logic with exponentials, every formula A for which exchange rules (and weakening and contraction as well) are admissible is provably equivalent to? A. This property shows that the expressive power of “noncommutative exponentials” is much more important than that of “commutative exponentials”.

Five types of constructions are introduced for non-prioritized belief revision, i.e., belief revision in which the input sentence is not always accepted. These constructions include generalizations of entrenchment-based and sphere-based revision. Axiomatic characterizations are provided, and close interconnections are shown to hold between the different constructions.

A hyperimaginary is an equivalence class of a type-definable equivalence relation on tuples of possibly infinite length. The notion was recently introduced in [1], mainly with reference to simple theories. It was pointed out there how hyperimaginaries still remain in a sense within the domain of first order logic. In this paper we are concerned with several issues: on the one hand, various levels of complexity of hyperimaginaries, and when hyperimaginaries can be reduced to simpler hyperimaginaries. On the other hand the issue of what information about hyperimaginaries in a saturated structure M can be obtained from the abstract group Aut(M).

In Section 2 we show that if T is simple and canonical bases of Lascar strong types exist in Meq then hyperimaginaries can be eliminated in favour of sequences of ordinary imaginaries. In Section 3, given a type-definable equivalence relation with a bounded number of classes, we show how the quotient space can be equipped with a certain compact topology. In Section 4 we study a certain group introduced in [5], which we call the Galois group of T, develop a Galois theory and make the connection with the ideas in Section 3. We also give some applications, making use of the structure of compact groups. One of these applications states roughly that bounded hyperimaginaries can be eliminated in favour of sequences of finitary hyperimaginaries. In Sections 3 and 4 there is some overlap with parts of Hrushovski's paper [2].