We prove that in all Mitchell-Steel core models, □k holds for all k. (See Theorem 2.) From this we obtain new consistency strength lower bounds for the failure of □k if k is either singular and countably closed, weakly compact, or measurable. (Corollaries 5, 8, and 9.) Jensen introduced a large cardinal property that we call subcompactness; it lies between superstrength and supercompactness in the large cardinal hierarchy. We prove that in all Jensen core models, □k holds iff k is not subcompact. (See Theorem 15; the only if direction is essentially due to Jensen.)

This paper aims to outline an analysis and interpretation of the process that led to First-Order Logic and its consolidation as a core system of modern logic. We begin with an historical overview of landmarks along the road to modern logic, and proceed to a philosophical discussion casting doubt on the possibility of a purely rational justification of the actual delimitation of First-Order Logic. On this basis, we advance the thesis that a certain historical tradition was essential to the emergence of modern logic; this traditional context is analyzed as consisting in some guiding principles and, particularly, a set of exemplars (i.e., paradigmatic instances). Then, we proceed to interpret the historical course of development reviewed in section 1, which can broadly be described as a two-phased movement of expansion and then restriction of the scope of logical theory. We shall try to pinpoint ambivalencies in the process, and the main motives for subsequent changes. Among the latter, one may emphasize the spirit of modern axiomatics, the situation of foundational insecurity in the 1920s, the resulting desire to find systems well-behaved from a proof-theoretical point of view, and the metatheoretical results of the 1930s. Not surprisingly, the mathematical and, more specifically, the foundational context in which First-Order Logic matured will be seen to have played a primary role in its shaping.

Mathematical logic is what logic, through twenty-five centuries and a few transformations, has become today. (Jean van Heijenoort)

In 1933 Gödel introduced a calculus of provability (also known as modal logic S4) and left open the question of its exact intended semantics. In this paper we give a solution to this problem. We find the logic LP of propositions and proofs and show that Gödel's provability calculus is nothing but the forgetful projection of LP. This also achieves Gödel's objective of defining intuitionistic propositional logic Int via classical proofs and provides a Brouwer-Heyting-Kolmogorov style provability semantics for Int which resisted formalization since the early 1930s. LP may be regarded as a unified underlying structure for intuitionistic, modal logics, typed combinatory logic and λ-calculus.

The four authors present their speculations about the future developments of mathematical logic in the twenty-first century. The areas of recursion theory, proof theory and logic for computer science, model theory, and set theory are discussed independently.

We consider tautologies formed from a pseudo-random number generator, defined in Krajíček [11] and in Alekhnovich et al. [2]. We explain a strategy of proving their hardness for Extended Frege systems via a conjecture about bounded arithmetic formulated in Krajíček [11]. Further we give a purely finitary statement, in the form of a hardness condition imposed on a function, equivalent to the conjecture.

We show how the notion of full Frobenius group of finite Morley rank generalizes that of bad group, and how it seems to be more appropriate when we consider the possible existence (still unknown) of nonalgebraic simple groups of finite Morley rank of a certain type, notably with no involution. We also show how these groups appear as a major obstacle in the analysis of FT-groups, if one tries to extend the Feit-Thompson theorem to groups of finite Morley rank.

This is the introductory half of a lecture given at the Association for Symbolic Logic Annual Meeting in Philadelphia in March, 2001. Our goal is to give logicians and advanced students who are unfamiliar with inner model theory a taste of what the subject is about at a level where it is possible to say something meaningful about the intuitions and proofs. At the same time, we wish to avoid overwhelming the reader, so we will leave out many well known closely related theorems and give only short proof sketches. Neither the results nor the proofs found here are due to the author. We will begin near the beginning but still touch on some modern aspects of the theory. The proofs and historical notes that we leave out can be found in the books and articles listed in the references. Our approach to the theory of 0# is a combination of that taken by Dodd in his book and by Steel in his lectures to students. Dodd's introduction is one of the author's favorite essays on inner model theory; another is the introduction to Martin-Steel [6]. In Section 2, we review the theory of 0# in a form that touches on some of the techniques that have been and continue to be generalized. These combine what is commonly called iteration and fine structure. In Section 3, we give a superficial description of what comes after 0#. Those interested in learning about more recent developments in inner model theory are encouraged to see the articles Lowe-Steel [5] and Steel [8], both of which are currently available online at http://www.math.berkeley.edu/~ steel.

§1. Introduction. With Hrushovski's proof of the function field Mordell-Lang conjecture [16] the relevance of geometric stability theory to diophantine geometry first came to light. A gulf between logicians and number theorists allowed for contradictory reactions. It has been asserted that Hrushovski's proof was simply an algebraic argument masked in the language of model theory. Another camp held that this theorem was merely a clever one-off. Still others regarded the argument as magical and asked whether such sorcery could unlock the secrets of a wide coterie of number theoretic problems.

In the intervening years each of these prejudices has been revealed as false though such attitudes are still common. The methods pioneered in [16] have been extended and applied to a number of other problems. At their best, these methods have been integrated into the general methods for solving diophantine problems. Moreover, the newer work suggests limits to the application of model theory to diophantine geometry. For example, all such known applications are connected with commutative algebraic groups. This need not be an intrinsic restriction, but its removal requires serious advances in the model theory of fields.

We discuss the differences between first-order set theory and second-order logic as a foundation for mathematics. We analyse these languages in terms of two levels of formalization. The analysis shows that if second-order logic is understood in its full semantics capable of characterizing categorically central mathematical concepts, it relies entirely on informal reasoning. On the other hand, if it is given a weak semantics, it loses its power in expressing concepts categorically. First-order set theory and second-order logic are not radically different: the latter is a major fragment of the former.

In 1960, E. P. Wigner, a joint winner of the 1963 Nobel Prize for Physics, published a paper titled On the Unreasonable Effectiveness of Mathematics in the Natural Sciences [61]. This paper can be construed as an examination and affirmation of Galileo's tenet that “The book of nature is written in the language of mathematics”. To this effect, Wigner presented a large number of examples that demonstrate the effectiveness of mathematics in accurately describing physical phenomena. Wigner viewed these examples as illustrations of what he called the empirical law of epistemology, which asserts that the mathematical formulation of the laws of nature is both appropriate and accurate, and that mathematics is actually the correct language for formulating the laws of nature. At the same time, Wigner pointed out that the reasons for the success of mathematics in the natural sciences are not completely understood; in fact, he went as far as asserting that “… the enormous usefulness of mathematics in the natural sciences is something bordering on the mysterious and there is no rational explanation for it.”

In this paper, we shall discuss some recent contributions to the project [15, 14, 2, 18, 22, 23] of explaining why no satisfactory system of complete invariants has yet been found for the torsion-free abelian groups of finite rank n ≥ 2. Recall that, up to isomorphism, the torsion-free abelian groups of rank n are exactly the additive subgroups of the n-dimensional vector space ℚn which contain n linearly independent elements. Thus the collection of torsion-free abelian groups of rank at most n can be naturally identified with the set S (ℚn) of all nontrivial additive subgroups of ℚn. In 1937, Baer [4] solved the classification problem for the class S(ℚ)of rank 1 groups as follows.

Let ℙ be the set of primes. If G is a torsion-free abelian group and 0 ≠ x ϵ G, then the p-height of x is defined to be

hx(p) = sup{n ϵ ℕ ∣ There exists y ϵ G such that pny = x} ϵ ℕ ∪{∞}; and the characteristic χ (x) of x is defined to be the function

If we assume the axiom of choice, then every two cardinal numbers are comparable. In the absence of the axiom of choice, this is no longer so. For a few cardinalities related to an arbitrary infinite set, we will give all the possible relationships between them, where possible means that the relationship is consistent with the axioms of set theory. Further we investigate the relationships between some other cardinal numbers in specific permutation models and give some results provable without using the axiom of choice.

We consider various concepts associated with the revision theory of truth of Gupta and Belnap. We categorize the notions definable using their theory of circular definitions as those notions universally definable over the next stable set. We give a simplified (in terms of definitional complexity) account of varied revision sequences—as a generalised algorithmic theory of truth. This enables something of a unification with the Kripkean theory of truth using supervaluation schemes.

We prove the triviality of the Grothendieck ring of a ℤ-valued field K under slight conditions on the logical language and on K. We construct a definable bijection from the plane K2 to itself minus a point. When we specialize to local fields with finite residue field, we construct a definable bijection from the valuation ring to itself minus a point.

§ 1. Introduction. In this communication we present some recent results on the classification of Polish metric spaces up to isometry and on the isometry groups of Polish metric spaces. A Polish metric space is a complete separable metric space (X, d).

Our first goal is to determine the exact complexity of the classification problem of general Polish metric spaces up to isometry. This work was motivated by a paper of Vershik [1998], where he remarks (in the beginning of Section 2): “The classification of Polish spaces up to isometry is an enormous task. More precisely, this classification is not ‘smooth’ in the modern terminology.” Our Theorem 2.1 below quantifies precisely the enormity of this task.

After doing this, we turn to special classes of Polish metric spaces and investigate the classification problems associated with them. Note that these classification problems are in principle no more complicated than the general one above. However, the determination of their exact complexity is not necessarily easier.

The investigation of the classification problems naturally leads to some interesting results on the groups of isometries of Polish metric spaces. We shall also present these results below.

The rest of this section is devoted to an introduction of some basic ideas of a theory of complexity for classification problems, which will help to put our results in perspective. Detailed expositions of this general theory can be found, e.g., in Hjorth [2000], Kechris [1999], [2001].