This paper compares the subsystem of analysis based on the Π11-comprehension axiom (Π11-CA) with classical Bar Induction (BI). An extension of Bar Induction using infinitary formulae is also considered, which was suggested to us by G. Kreisel (oral communication).

To describe these formal systems, we first describe the language, L, appropriate for their formalization. L contains the language of ENT (1st order arithmetic) plus function variables ƒi, gi, hi, etc. Number-theoretic terms are built up from +, × , ′ , 0, and application.

The object of this paper is to make a study of four systems of modal logic (S4, S5, and their intuitionistic analogues IM4 and IM5) with the techniques of the theory of abstract logics set up by Suszko, Bloom, Brown, Verdú and others. The abstract concepts corresponding to such systems are defined as generalizations of the logics naturally associated to their algebraic models (topological Boolean or Heyting algebras, general or semisimple). By considering new suitably defined connectives and by distinguishing between having the rule of necessitation only for theorems or as a full inference rule (which amounts to dealing with all filters or with open filters of the algebras) we are able to reduce the study of a modal (abstract) logic L to that of two nonmodal logics L− and L+ associated with L. We find that L is “of IM4 type” if and only if L− and L+ are both intuitionistic and have the same theorems, and logics of type S4, IM5 or S5 are obtained from those of type IM4 simply by making classical L−, L+ or both. We compare this situation with that found in recent approaches to intuitionistic modal logic using birelational models or using higher-level sequent-systems. The treatment of modal systems with abstract logics is rather new, and in our way to it we find several general constructions and results which can also be applied to other modal systems weaker than those we study in detail.

This paper concerns Tarski's use of the term “model” in his 1936 paper “On the Concept of Logical Consequence.” Against several of Tarski's recent defenders. I argue that Tarski employed a non-standard conception of models in that paper. Against Tarski's detractors. I argue that this nonstandard conception is more philosophically plausible than it may appear. Finally, I make a few comments concerning the traditionally puzzling case of Tarski's ω-rule example.

We present and study the category of formal topologies and some of its variants. Two main results are proven. The first is that, for any inductively generated formal cover, there exists a formal topology whose cover extends in the minimal way the given one. This result is obtained by enhancing the method for the inductive generation of the cover relation by adding a coinductive generation of the positivity predicate. Categorically, this result can be rephrased by saying that inductively generated formal topologies are coreflective into inductively generated formal covers.

The second result is that unary formal covers are exponentiable in the category of inductively generated formal covers and hence, thanks to the coreflection, unary formal topologies are exponentiable in the category of inductively generated formal topologies.

From a localic point of view the exponentiability of unary formal topologies means that algebraic dcpos are exponentiable in the category of open locales. But, the coreflection theorem states that open locales are coreflective in locales and hence, as a consequence of well-known impredicative results on exponentiable locales, it allows to prove that locally compact open locales are exponentiable in the category of open locales.

It is shown that if ZF is consistent, then so is ZFC + GCH + “There is a graph with cardinality ℵ2 and chromatic number ℵ2 such that every subgraph of cardinality ≤ ℵ1, has chromatic number ≤ ℵ0”. This partially answers a question of Erdös and Hajnal.

In this paper we introduce a new natural deduction system for the logic of lattices, and a number of extensions of lattice logic with different negation connectives. We provide the class of natural deduction proofs with both a standard inductive definition and a global graph-theoretical criterion for correctness, and we show how normalisation in this system corresponds to cut elimination in the sequent calculus for lattice logic. This natural deduction system is inspired both by Shoesmith and Smiley's multiple conclusion systems for classical logic and Girard's proofnets for linear logic.

We study random relational structures that are relatively exchangeable—that is, whose distributions are invariant under the automorphisms of a reference structure ${M}$. When ${M}$ is ultrahomogeneous and has trivial definable closure, all random structures relatively exchangeable with respect to $m$ satisfy a general Aldous–Hoover-type representation. If ${M}$ also satisfies the n-disjoint amalgamation property (n-DAP) for all $n \ge 1$, then relatively exchangeable structures have a more precise description whereby each component depends locally on ${M}$.

In this note we present an axiomatization of the classical two-valued propositional calculus, for which proofs of decidability, consistency, completeness, and independence, are almost trivial (given an understanding of truth tables).

Let I⊿0 denote the fragment of Peano arithmetic where induction is restricted only to bounded formulas (⊿0-formulas), i.e. formulas where all the quantifiers are bounded. We will examine the behaviour in I⊿0 of Chebyshev's classical result on the distribution of primes. Chebyshev showed that each of the following functions on N is bounded by a polynomial in each of the others:

In his proof he used, as auxiliaries, factorials and binomial coefficients.

When we work in a weak system like I⊿0 we have to deal with two problems:

(i) There is not an immediate meaning for symbols like xy, Πp≤xp, and x!.

(ii) Some basic functions like exponentiation, factorial, and product of primes up to a certain element, are in general only partially definable.

The first problem is equivalent to finding ⊿0-formulas representing the relations z = xy, y = Πp≤xp, and y = x!. While we can easily express that y is the product of all primes less than or equal to x in a ⊿0-way, it requires a subtle argument to define z = xy by a ⊿0-formula. The most natural way of expressing it is via the formalization of the Chinese remainder theorem coding the recursion procedure used in the definition of xy. But this can be expressed only via a Σ1-formula. ⊿0-definitions of exponentiation were given by Paris and Bennett (see [GD] and [B]), and all sensible definitions of this type are equivalent (see Remark 1). Later we will examine properties of such a definition E0(x, y, z). The ⊿00-definition of y = Πp≤xp is much more straightforward, since both the relation of being a prime and the divisibility relation are ⊿0-definable. We will give an explicit definition of it and denote it by Ψ(x, y). In this way, by a ⊿0-induction, we will be able to prove the uniqueness of the elements y and z satisfying Ψ(x, y) and E0(x, y, z), respectively.

In this note we shall prove a certain relative recursiveness lemma concerning countable models of set theory (Lemma 5). From this lemma will follow two results about special types of such models.

Kreisel [5] and Mostowski [6] have shown that certain (finitely axiomatized) systems of set theory, formulated by means of the ϵ relation and certain additional non-logical constants, do not possess recursive models. Their purpose in doing this was to construct consistent sentences without recursive models. As a first corollary of Lemma 5, we obtain a very simple proof, not involving any formal constructions within the system of the notions of truth and satisfiability, of an extension of the Kreisel-Mostowski theorems. Namely, set theory with the single non-logical constant ϵ does not possess any recursively enumerable model. Thus we get, as a side product, an easy example of a consistent sentence containing a single binary relation which does not possess any recursively enumerable model; this sentence being the conjunction of the (finitely many) axioms of set theory.

One of the main tools in the study of nonmonotonic consequence relations is the representation of such relations in terms of preferential models. In this paper we give an unified and simpler framework to obtain such representation theorems.

Kueker's conjecture is proved for stable theories, for theories that interpret a linear ordering, and for theories with Skolem functions. The proof of the stable case involves certain results on coordinatization that are of independent interest.

We construct a type p with preweight ω with respect to itself in a theory with few types. A type with this property must be present in a stable theory with finitely many (but more than one) countable models. The construction is a modification of Hrushovski's important pseudoplane construction.

We show, within the framework of Bishop's constructive mathematics, that (sequential) completeness of the locally convex space (ℝ) of test functions is equivalent to the principle BD-ℕ which holds in classical mathemtatics, Brouwer's intuitionism and Markov's constructive recursive mathematics, but does not hold in Bishop's constructivism.

We give a commentary on Newelski's suggestion or conjecture [8] that topological dynamics, in the sense of Ellis [3], applied to the action of a definable group G(M) on its “external type space” SG.ext(M), can explain, account for, or give rise to, the quotient G/G00, at least for suitable groups in NIP theories. We give a positive answer for measure-stable (or f sg) groups in NIP theories. As part of our analysis we show the existence of “externally definable” generics of G(M) for measure-stable groups. We also point out that for G definably amenable (in a NIP theory) G/G00 can be recovered, via the Ellis theory, from a natural Ellis semigroup structure on the space of global f-generic types.

We characterize the generalized quantifiers Q which satisfy the scheme QxQyф ↔ QyQxф, the so-called self-commuting quantifiers, or quantifiers with the Fubini property.

It is well known that L, the first-order predicate calculus, is unsuitable for characterizing certain mathematical structures. Since some of those structures are quite often considered by mathematicians, extensions of L have been considered which (partially) solve the above problem. Roughly speaking, the extensions of L fall into two main categories:

(I) extensions obtained by allowing higher order variables, and

(II) extensions obtained by allowing infinitely long formulas.

We give a characterization of the cofinality of the strong measure zero ideal under the continuum hypothesis and prove that we can force it to a value less than the power of the continuum.

We show that every sufficiently iterable countable mouse has a unique iteration strategy whose associated iteration maps are lexicographically minimal. This enables us to extend the results of [3] on the good behavior of the standard parameter from tame mice to arbitrary mice.