Transitive extensional well founded relations provide an intuitionistic notion of ordinals which admits transfinite induction. However these ordinals are not directed and their successor operation is poorly behaved, leading to problems of functoriality.

We show how to make the successor monotone by introducing plumpness, which strengthens transitivity. This clarifies the traditional development of successors and unions, making it intuitionistic; even the (classical) proof of trichotomy is made simpler. The definition is, however, recursive, and, as their name suggests, the plump ordinals grow very rapidly.

Directedness must be defined hereditarily. It is orthogonal to the other four conditions, and the lower powerdomain construction is shown to be the universal way of imposing it.

We treat ordinals as order-types, and develop a corresponding set theory similar to Osius' transitive set objects. This presents Mostowski's theorem as a reflection of categories, and set-theoretic union is a corollary of the adjoint functor theorem. Mostowski's theorem and the rank for some of the notions of ordinal are formulated and proved without the axiom of replacement, but this seems to be unavoidable for the plump rank.

The comparison between sets and toposes is developed as far as the identification of replacement with completeness, and there are some suggestions for further work in this area.

Each notion of set or ordinal defines a free algebra for one of the theories discussed by Joyal and Moerdijk, namely joins of a family of arities together with an operation s satisfying conditions such as x ≤ sx, monotonicity or s(x ∨ y) ≤ sx ∨ sy.

Finally we discuss the fixed point theorem for a monotone endofunction s of a poset with least element and directed joins. This may be proved under each of a variety of additional hypotheses. We explain why it is unlikely that any notion of ordinal obeying the induction scheme for arbitrary predicates will prove the pure result.

We establish constructive refinements of several well-known theorems in elementary model theory. The additive group of the real numbers may be embedded elementarily into the additive group of pairs of real numbers, constructively as well as classically.

We show that the theory ATR0 is equivalent to a second-order generalization of the theory . As a result, ATR0 is conservative over for arithmetic sentences, though proofs in ATR0 can be much shorter than their counterparts.

Let κ be an uncountable cardinal and the edges of a complete graph with κ vertices be colored with ℵ0 colors. For the Erdős-Rado theorem implies that there is an infinite monochromatic subgraph. However, if , then it may be impossible to find a monochromatic triangle. This paper is concerned with the latter situation. We consider the types of colorings of finite subgraphs that must occur when the edges of the complete graph on vertices are colored with ℵ0 colors. In particular, we are concerned with the case ℵ1 ≤ κ ≤ ℵω.

The study of these color patterns (known as identities) has a history that involves the existence of compactness theorems for two cardinal models [2]. When the graph being colored has size ℵ1, the identities that must occur have been classified by Shelah [4]. If the graph has size greater than or equal to ℵω the identities have also been classified in [3]. The number of colors is fixed at ℵ0 as it is the natural place to start and the results here can be generalized to situations where more colors are used.

There is one difference that we now make explicit. When countably many colors are used we can define the following coloring of the complete graph on vertices. First consider the branches in the complete binary tree of height ω to be vertices of a complete graph.

An epistemic formalization of arithmetic is constructed in which certain non-trivial metatheoretical inferences about the system itself can be made. These inferences involve the notion of provability in principle, and cannot be made in any consistent extensions of Stewart Shapiro's system of epistemic arithmetic. The system constructed in the paper can be given a modal-structural interpretation

The concept of a generalized quantifier of a given similarity type was defined in [12]. Our main result says that on finite structures different similarity types give rise to different classes of generalized quantifiers. More exactly, for every similarity type t there is a generalized quantifier of type t which is not definable in the extension of first order logic by all generalized quantifiers of type smaller than t. This was proved for unary similarity types by Per Lindström [17] with a counting argument. We extend his method to arbitrary similarity types.

This paper deals with: (i) the theory which results from by restricting induction on the natural numbers to formulas which are positive in the fixed point constants, (ii) the theory BON(μ) plus various forms of positive induction, and (iii) a subtheory of Peano arithmetic with ordinals in which induction on the natural numbers is restricted to formulas which are Σ in the ordinals. We show that these systems have proof-theoretic strength φω0.

In this paper we study the logic of relational and partial variable sets, seen as a generalization of set-valued presheaves, allowing transition functions to be arbitrary relations or arbitrary partial functions. We find that such a logic is the usual intuitionistic and co-intuitionistic first order logic without Beck and Frobenius conditions relative to quantifiers along arbitrary terms. The important case of partial variable sets is axiomatizable by means of the substitutivity schema for equality. Furthermore, completeness, incompleteness and independence results are obtained for different kinds of Beck and Frobenius conditions.

It is well known that every Boolean algebra of size ω1 can be embedded into (ω)/fin. E. van Douwen proved that if CH failed then there is a Boolean algebra of size ω2 which cannot be embedded into (ω1)/ctble. We show that ◇ is equivalent to the statement that a certain natural Boolean algebra of size embeds into (ω1)/ctble. I would like to thank B. Velickovic for many helpful conversations.

We give a decision procedure for the ∀∃-theory of the weak truth-table (wtt) degrees of the recursively enumerable sets. The key to this decision procedure is a characterization of the finite lattices which can be embedded into the r.e. wtt-degrees by a map which preserves the least and greatest elements: a finite lattice has such an embedding if and only if it is distributive and the ideal generated by its cappable elements and the filter generated by its cuppable elements are disjoint.

We formulate general criteria that allow one to conclude that a distributive upper semi-lattice has a decidable two-quantifier theory. These criteria are applied not only to the weak truth-table degrees of the recursively enumerable sets but also to various substructures of the polynomial many-one (pm) degrees of the recursive sets. These applications to the pm degrees require no new complexity-theoretic results. The fact that the pm-degrees of the recursive sets have a decidable two-quantifier theory answers a question raised by Shore and Slaman in [21].

The existence of a countable complete theory with exactly ℵ1 many minimal models is independent of ZFC + ¬CH.

We prove various results on the notion of ordinal ultrafiters introduced by J. Baumgartner. In particular, we show that this notion of ultrafilter complexity is independent of the more familiar Rudin-Keisler ordering.

We introduce the concepts of Morley rank and Morley degree for structures based on Banach spaces. We characterize ω-stability in terms of Morley rank, and prove the existence of prime models for ω-stable theories.

We characterize the collapse of Buss' bounded arithmetic in terms of the provable collapse of the polynomial time hierarchy. We include also some general model-theoretical investigations on fragments of bounded arithmetic.

Pillay studied nonmultidimensional superstable theories in [8], among other things defining a certain hierarchy of regular types in terms of which all other types may be analysed. Using this hierarchy, he showed that after naming a suitable ‘base’ of parameters, there are j-constructible (hence locally atomic) models over arbitrary sets (see Section 2 for definitions). It is asked at the end of [8] whether the parameter set can be removed. On a different note, it has been known for some time that in nonmultidimensional superstable theories, R∞-rank is definable for formulas having finite rank (see for example [9]). Definability of R∞-rank has had various applications in the literature, and so it is natural to ask whether the restriction to finite rank is necessary. In this paper we do not quite answer this question, but instead use Pillay's analysis to establish the existence of a ‘new’ continuous rank (the original idea for which is due to Tanović) which is defined on all complete types, reflects forking as does R∞-rank and satisfies certain definability properties.

A countable, atomically stable structure in a finite, relational language has fewer than 2ω non-isomorphic substructures if and only if is cellular. An example shows that the finiteness of the language is necessary.

We show how sequent calculi for some generalized quantifiers can be obtained by generalizing the Herbrand approach to ordinary first order proof theory. Typical of the Herbrand approach, as compared to plain sequent calculus, is increased control over relations of dependence between variables. In the case of generalized quantifiers, explicit attention to relations of dependence becomes indispensible for setting up proof systems. It is shown that this can be done by turning variables into structured objects, governed by various types of structural rules. These structured variables are interpreted semantically by means of a dependence relation. This relation is an analogue of the accessibility relation in modal logic. We then isolate a class of axioms for generalized quantifiers which correspond to first-order conditions on the dependence relation.