The starting point of this article is an old question asked by Feferman in his paper on Hancock's conjecture [6] about the strength of . This theory is obtained from the well-known theory ID1 by restricting fixed point induction to formulas that contain fixed point constants only positively. The techniques used to perform the proof-theoretic analysis of also permit to analyze its transfinitely iterated variants . Thus, we eventually know that

Given a weakly o-minimal theory T, the T-height of an element of a model of T is defined as a means of classifying the order of magnitude of the element. If T satisfies some easily met technical conditions, then this classification is coarse enough for a Wilkie-type inequality: given a set of elements of a model of T, each of which has a different T-height, the cardinality of this set is at most 1 plus the minimum cardinality of a set that generates the structure.

We prove that the definition of supersimplicity in metric structures from [7] is equivalent to an a priori stronger variant. This stronger variant is then used to prove that if T is a supersimple Hausdorff cat then so is its theory of lovely pairs.

The method of analytic tableaux is employed in many introductory texts and has also been used quite extensively as a basis for automated theorem proving. In this paper, we discuss the complexity of the system as a method for refuting contradictory sets of clauses, and resolve several open questions. We discuss the three forms of analytic tableaux: clausal tableaux, generalized clausal tableaux, and binary tableaux. We resolve the relative complexity of these three forms of tableaux proofs and also resolve the relative complexity of analytic tableaux versus resolution. We show that there is a quasi-polynomial simulation of tree resolution by analytic tableaux; this simulation is close to optimal, since we give a matching lower bound that is tight to within a polynomial.

When studying the model theory of

the first observation is that the integers can be defined as

Since ∂exp is subject to all of Gödel's phenomena, this is often also the last observation. After Wilkie proved that ℝexp is model complete, one could ask the same question for ∂exp, but the answer is negative.

Proposition 1.1. ∂expis not model complete

Proof. If ∂exp is model complete, then every definable set is a projection of a closed set. Since ∂ is locally compact, every definable set is Fσ. The same is true for the complement, so every definable set is also Gδ. But, since ℤ is definable, ℚ is definable and a standard corollary of the Baire Category Theorem tells us that ℚ is not Gδ.

Still, there are several interesting open questions about ∂exp.

• Is ℝ definable in ∂exp?

• (quasiminimality) Is every definable set countable or co-countable? (Note that this is true in the structure (∂, ℤ, +, ·) where we add a predicate for ℤ).

• (Mycielski) Is there an automorphism of ∂exp other than the identity and complex conjugation?1

A positive answer to the first question would tell us that ∂exp is essentially second order arithmetic, while a positive answer to the second would say that integers are really the only obstruction to a reasonable theory of definable sets.

A fascinating, novel approach to ∂exp is provided by Zilber's [6] pseudoexponentiation. Let L be the language {+, · E, 0, 1}.

We show, first, that the normalization procedure for S4 modal logic presented by Dag Prawitz in [5] does not work. We then develop a new natural deduction system for S4 classical modal logic that is logically equivalent to that of Prawitz, and we show that every derivation in this new system can be transformed into a normal derivation.

The main subject of the article is the finite submodel property for ℵ0-categorical structures, in particular under the additional assumptions that the structure is simple, 1-based and has trivial dependence. Here, a structure has the finite submodel property if every sentence which is true in the structure is true in a finite substructure of it. It will be useful to consider a couple of other finiteness properties, related to the finite submodel property, which are variants of the usual concept of saturation.

For the rest of the introduction we will assume that M is an ℵ0-categorical (infinite) structure with a countable language. We also assume that there is an upper bound to the arity of the function symbols in M:s language and that, for every 0 < n < ℵ0 and R ⊆ Mn which is definable in M without parameters, there exists a relation symbol, in the language of M, which is interpreted as R; these assumptions are not necessary for most results to be presented, but it simplifies the statement of a result which I mention in this introduction.

First we will consider ‘canonically embedded’ substructures of Meq. Here, a structure N is canonically embedded in Meq if N's universe is a subset of Meq which is definable without parameters and, for every 0 < n < ℵ0 and R ⊆ Nn which is ε-definable in Meq there is a relation symbol in the language of N which is interpreted as R; we also assume that the language of N has no other relation (or function or constant) symbols.

We give some general criteria for the stable embeddedness of a definable set. We use these criteria to establish the stable embeddedness in algebraically closed valued fields of two definable sets: The set of balls of a given radius r < 1 contained in the valuation ring and the set of balls of a given multiplicative radius r < 1. We also show that in an algebraically closed valued field a 0-definable set is stably embedded if and only if its algebraic closure is stably embedded.

In the last few decades many formal systems of fuzzy logics have been developed. Since the main differences between fuzzy and classical logics lie at the propositional level, the fuzzy predicate logics have developed more slowly (compared to the propositional ones). In this text we aim to promote interest in fuzzy predicate logics by contributing to the model theory of fuzzy predicate logics. First, we generalize the completeness theorem, then we use it to get results on conservative extensions of theories and on witnessed models.

This paper is concerned with n–localization property introduced by Newelski and Roslanowski in [10] and getting it for CS iterations of forcing notions.

Most Gentzen systems arising in logic contain few axiom schemata and many rule schemata. Hilbert systems, on the other hand, usually contain few proper inference rules and possibly many axioms. Because of this, the two notions tend to serve different purposes. It is common for a logic to be specified in the first instance by means of a Gentzen calculus, whereupon a Hilbert-style presentation ‘for’ the logic may be sought—or vice versa. Where this has occurred, the word ‘for’ has taken on several different meanings, partly because the Gentzen separator ⇒ can be interpreted intuitively in a number of ways. Here ⇒ will be denoted less evocatively by ⊲.

In this paper we aim to discuss some of the useful ways in which Gentzen and Hilbert systems may correspond to each other. Actually, we shall be concerned with the deducibility relations of the formal systems, as it is these that are susceptible to transformation in useful ways. To avoid potential confusion, we shall speak of Hilbert and Gentzen relations. By a Hilbert relation we mean any substitution-invariant consequence relation on formulas—this comes to the same thing as the deducibility relation of a set of Hilbert-style axioms and rules. By a Gentzen relation we mean the fully fledged generalization of this notion in which sequents take the place of single formulas. In the literature, Hilbert relations are often referred to as sentential logics. Gentzen relations as defined here are their exact sequential counterparts.

We prove that for any locally countable partial order ℙ = (2ε, ≤p, there exists a nonmeasurable antichain in ℙ. Some applications of the result are also presented.

We define elementary extension and elementary equivalence in Positive Logic.

We produce counterexamples to the unique and cofinal branches hypotheses, assuming (slightly less than) the existence of a cardinal which is strong past a Woodin cardinal.

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

This paper studies definability within the theory of institutions, a version of abstract model theory that emerged in computing science studies of software specification and semantics. We generalise the concept of definability to arbitrary logics, formalised as institutions, and we develop three general definability results. One generalises the classical Beth theorem by relying on the interpolation properties of the institution. Another relies on a meta Birkhoff axiomatizability property of the institution and constitutes a source for many new actual definability results, including definability in (fragments of) classical model theory. The third one gives a set of sufficient conditions for ‘borrowing’ definability properties from another institution via an ‘adequate’ encoding between institutions.

The power of our general definability results is illustrated with several applications to (many-sorted) classical model theory and partial algebra, leading for example to definability results for (quasi-)varieties of models or partial algebras. Many other applications are expected for the multitude of logical systems formalised as institutions from computing science and logic.

This paper investigates when it is possible for a partial ordering ℙ to force Pk(Λ)\V to be stationary in Vℙ. It follows from a result of Gitik that whenever ℙ adds a new real, then Pk(Λ)\V is stationary in Vℙ for each regular uncountable cardinal κ in Vℙ and all cardinals λ ≥ κ in Vℙ [4], However, a covering theorem of Magidor implies that when no new ω-sequences are added, large cardinals become necessary [7]. The following is equiconsistent with a proper class of ω1-Erdős cardinals: If ℙ is ℵ1-Cohen forcing, then Pk(Λ)\V is stationary in Vℙ, for all regular κ ≥ ℵ2and all λ ≩ κ. The following is equiconsistent with an ω1-Erdős cardinal: If ℙ is ℵ1-Cohen forcing, then is stationary in Vℙ. The following is equiconsistent with κ measurable cardinals: If ℙ is κ-Cohen forcing, then is stationary in Vℙ.

We prove that there exists a noncomputable c.e. real which is low for weak 2-randomness, a definition of randomness due to Kurtz, and that all reals which are low for weak 2-randomness are low for Martin-Löf randomness.

We establish a surprising connection between Menger's classical covering property and Blass-Laflamme's modern combinatorial notion of groupwise density. This connection implies a short proof of the groupwise density bound on the additivity number for Menger's property.

We explore the interaction between Lebesgue measure and dominating functions. We show, via both a priority construction and a forcing construction, that there is a function of incomplete degree that dominates almost all degrees. This answers a question of Dobrinen and Simpson, who showed that such functions are related to the proof-theoretic strength of the regularity of Lebesgue measure for Gδ sets. Our constructions essentially settle the reverse mathematical classification of this principle.