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 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.

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.

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.

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].

In The Axiom of Determinacy, Forcing Axioms and the Nonstationary Ideal [W1], Woodin constructs the partial order ℙmax, which in the presence of large cardinals yields a forcing extension of L(ℝ) where ZFC holds and the non-stationary ideal on ω1 (hereafter denoted NSω1) is ω2-saturated. The basic analysis of ℙmax forcing over L(ℝ) can be carried out assuming only the Axiom of Determinacy (AD). In the central result of this paper, we show that if one increases slightly the strength of the determinacy assumptions, then Chang's Conjecture—the assertion that every finitary algebra on ω2 has a subalgebra of order type ω1—holds in this extension as well. Specifically, we obtain:

Corollary 4.6. Assume AD + V = L(ℝ, μ) + μ is a normal, fine measure on. Chang's Conjecture holds in any ℙmax-generic extension of L(ℝ).

This technique for obtaining Chang's Conjecture is fairly general. We [Se] have adapted it to obtain Chang's Conjecture in the model presented by Steel and Van Wesep [SVW] and Woodin [Wl] has adapted it to his ℚmax forcing notion. In each of these models, as in the ℙmax extension, one forces over L(ℝ) assuming AD to obtain ZFC and NSω1 is ω2-saturated.

By unpublished results of Woodin, the assumption for Corollary 4.6 is equiconsistent with the existence of ω2 many Woodin cardinals, and hence strictly stronger than ADL(ℝ). One would like to reduce this assumption to ADL(ℝ). Curiously, this reduction is not possible in the arguments for ℚmax or the Steel and Van Wesep model, and the following argument of Woodin suggests why it may not be possible for ℙmax either.

We prove that the problem of determining the minimum propositional proof length is NP-hard to approximate within a factor of . These results are very robust in that they hold for almost all natural proof systems, including: Frege systems, extended Frege systems, resolution. Horn resolution, the polynomial calculus, the sequent calculus, the cut-free sequent calculus, as well as the polynomial calculus. Our hardness of approximation results usually apply to proof length measured either by number of symbols or by number of inferences, for tree-like or dag-like proofs. We introduce the Monotone Minimum (Circuit) Satisfying Assignment problem and reduce it to the problems of approximation of the length of proofs.

Reverse mathematics uses subsystems of second order arithmetic to determine which set existence axioms are required to prove particular theorems. Surprisingly, almost every theorem studied is either provable in RCA0 or equivalent over RCA0 to one of four other subsystems: WKL0, ACA0, ATR0 or – CA0. Of these subsystems, – CA0 has the fewest known equivalences. This article presents a new equivalence of – C0 which comes from ordered group theory.

One of the fundamental problems about ordered groups is to classify all possible orders for various classes of orderable groups. In general, this problem is extremely difficult to solve. Mal'tsev [1949] solved a related problem by showing that the order type of a countable ordered group is ℤαℚε where ℤ is the order type of the integers, ℚ is the order type of the rationals, α is a countable ordinal, and ε is either 0 or 1. The goal of this article is to prove that this theorem is equivalent over RCA0 to – CA0.

In Section 2, we give the basic definitions and notation for RCA0, ACA0 and CA0 as well as for ordered groups. For more information on reverse mathematics, see Friedman, Simpson, and Smith [1983] or Simpson [1999] and for ordered groups, see Kokorin and Kopytov [1974] or Fuchs [1963]. Our notation will follow these sources. In Section 3, we show that – CA0 suffices to prove Mal'tsev's Theorem and the reversal is done over RCA0 in Section 4.

With each projective geometry we can associate a Lyndon algebra. Such an algebra always satisfies Tarski's axioms for relation algebras and Lyndon algebras thus form an interesting connection between the fields of projective geometry and algebraic logic. In this paper we prove that if G is a class of projective geometries which contains an infinite projective geometry of dimension at least three, then the class L(G) of Lyndon algebras associated with projective geometries in G has an undecidable equational theory. In our proof we develop and use a connection between projective geometries and diagonal-free cylindric algebras.

We introduce a notion of syntactical truth predicate (s.t.p.) for the second order arithmetic PA2. An s.t.p. is a set T of closed formulas such that:

(i) T(t = u) if and only if the closed first order terms t and u are convertible, i.e., have the same value in the standard interpretation

(ii) T(A → B) if and only if (T(A) ⇒ T(B))

(iii) T(∀xA) if and only if (T(A[x ← t]) for any closed first order term t)

(iv) T(∀X A) if and only if (T(A[X ← ∆]) for any closed set definition ∆ = {x ∣ D(x)}).

S.t.p.'s can be seen as a counterpart to Tarski's notion of (model-theoretical) validity and have main model properties. In particular, their existence is equivalent to the existence of an ω-model of PA2, this fact being provable in PA2 with arithmetical comprehension only.

A maximal almost disjoint (mad) family ⊆ [ω]ω is Cohen-stable if and only if it remains maximal in any Cohen generic extension. Otherwise it is Cohen-unstable. It is shown that a mad family. .is Cohen-unstable if and only if there is a bijection G from ω to the rationals such that the sets G[A]. A ∈ are nowhere dense. An ℵ0-mad family, . is a mad family with the property that given any countable family ℬ ⊂ [ω]ω such that each element of ℬ meets infinitely many elements of in an infinite set there is an element of meeting each element of ℬ in an infinite set. It is shown that Cohen-stable mad families exist if and only if there exist ℵ0-mad families. Either of the conditions b = c or a < cov() implies that there exist Cohen-stable mad families. Similar results are obtained for splitting families. For example, a splitting family. . is Cohen-unstable if and only if there is a bijection G from ω to the rationals such that the boundaries of the sets G[S], S ∈ are nowhere dense. Also. Cohen-stable splitting families of cardinality ≤ κ exist if and only if ℵ0-splitting families of cardinality ≤ κ exist.

It is proved that Vaught's conjecture is true for modules over an arbitrary countable hereditary noetherian prime ring.

We present a basis for the admissible rules of intuitionistic propositional logic. Thereby a conjecture by de Jongh and Visser is proved. We also present a proof system for the admissible rules, and give semantic criteria for admissibility.

A vast and interesting family of natural semantics lor belief revision is defined. Suppose one is given a distance d between any two models. One may then define the revision of a theory K by a formula α as the theory defined by the set of all those models of α that are closest, by d. to the set of models of K. This family is characterized by a set of rationality postulates that extends the AGM postulates. The new postulates describe properties of iterated revisions.

We introduce a new cardinal characteristic r*. related to the reaping number r. and show that

• posets of size < r* which add reals add unbounded reals;

• posets of size < r which add unbounded reals add Cohen reals.

We also show that add() ≤ min(r. r*). It follows that posets of size < add() which add reals add Cohen reals.

This improves results of Roslanowski and Shelah [RS] and of Zapletal [Z].

In the early eighties, answering a question of A. Macintyre, J. H. Schmerl ([13]) proved that every countable recursively saturated structure, equipped with a function β encoding the finite functions, is the β-closure of an infinite indiscernible sequence. This result implies that every countably saturated structure, in a countable but not necessarily recursive language, is an Ehrenfeucht-Mostowski model, by which we mean that the structure expands, in a countable language, to the Skolem hull of an infinite indiscernible sequence (in the new language).

More recently, D. Lascar ([5]) showed that the saturated model of cardinality ℵ1 of an ω-stable theory is also an Ehrenfeucht-Mostowski model.

These results naturally raise the following problem: which (countable) complete theories have an uncountably saturated Ehrenfeucht-Mostowski model. We study a generalization of this question. Namely, we call ACI-model a structure which can be expanded, in a countable language L′, to the algebraic closure (in L′) of an infinite indiscernible sequence (in L′). And we try to characterize the λ-saturated structures which are ACI-models.

The main results are the following. First it is enough to restrict ourselves to ℵ1-saturated structures: if T has an ℵ1-saturated ACI-model then, for every infinite λ, T has a λ-saturated ACI-model. We obtain a complete answer in the case of stable theories: if T is stable then the three following properties are equivalent: (a) T is ω-stable, (b) T has an ℵ1-saturated ACI-model, (c) every saturated model of T is an Ehrenfeucht-Mostowski model. The unstable case is more complicated, however we show that if T has an ℵ1-saturated ACI-model then T doesn't have the independence property.

We prove that any 1-closed (see def 1.1) model of the Π2 consequences of PA satisfies ¬Cons PA which gives a proof of the second Gödel incompleteness theorem without the use of the Gödel diagonal lemma. We prove a few other theorems by the same method.

Acceptable programming systems have many nice properties like s-m-n-Theorem, Composition and Kleene Recursion Theorem. Those properties are sometimes called control structures, to emphasize that they yield tools to implement programs in programming systems. It has been studied, among others by Riccardi and Royer, how these control structures influence or even characterize the notion of acceptable programming system. The following is an investigation, how these control structures behave in the more general setting of complete numberings as defined by Mal'cev and Eršov.

By the theory TT is meant the higher order predicate logic with the following recursively defined types:

(1) 1 is the type of individuals and [] is the type of the truth values:

(2) [τ1…..τn] is the type of the predicates with arguments of the types τ1…..τn.

The theory ITT described in this paper is an intensional version of TT. The types of ITT are the same as the types of TT, but the membership of the type 1 of individuals in ITT is an extension of the membership in TT. The extension consists of allowing any higher order term, in which only variables of type 1 have a free occurrence, to be a term of type 1. This feature of ITT is motivated by a nominalist interpretation of higher order predication.

In ITT both well-founded and non-well-founded recursive predicates can be defined as abstraction terms from which all the properties of the predicates can be derived without the use of non-logical axioms.

The elementary syntax, semantics, and proof theory for ITT are defined. A semantic consistency proof for ITT is provided and the completeness proof of Takahashi and Prawitz for a version of TT without cut is adapted for ITT: a consequence is the redundancy of cut.

We prove that the strong Martin conjecture is false. The counterexample is the first-order theory of infinite atomic Boolean algebras. We show that for this class of Boolean algebras, the classification of their (ω + ω)-elementary theories can be reduced to the classification of the elementary theories of their quotient algrbras modulo the Frechét ideals.