§1. I will start with a quick definition of descriptive set theory: It is the study of the structure of definable sets and functions in separable completely metrizable spaces. Such spaces are usually called Polish spaces. Typical examples are ℝn, ℂn, (separable) Hilbert space and more generally all separable Banach spaces, the Cantor space 2ℕ, the Baire space ℕℕ, the infinite symmetric group S∞, the unitary group (of the Hilbert space), the group of measure preserving transformations of the unit interval, etc.

In this theory sets are classified in hierarchies according to the complexity of their definitions and the structure of sets in each level of these hierarchies is systematically analyzed. In the beginning we have the Borel sets in Polish spaces, obtained by starting with the open sets and closing under the operations of complementation and countable unions, and the corresponding Borel hierarchy ( sets). After this come the projective sets, obtained by starting with the Borel sets and closing under the operations of complementation and projection, and the corresponding projective hierarchy ( sets).

There are also transfinite extensions of the projective hierarchy and even much more complex definable sets studied in descriptive set theory, but I will restrict myself here to Borel and projective sets, in fact just those at the first level of the projective hierarchy, i.e., the Borel (), analytic () and coanalytic () sets.

Hilbert's finitist program was not created at the beginning of the twenties solely to counteract Brouwer's intuitionism, but rather emerged out of broad philosophical reflections on the foundations of mathematics and out of detailed logical work; that is evident from notes of lecture courses that were given by Hilbert and prepared in collaboration with Bernays during the period from 1917 to 1922. These notes reveal a dialectic progression from a critical logicism through a radical constructivism toward finitism; the progression has to be seen against the background of the stunning presentation of mathematical logic in the lectures given during the winter term 1917/18. In this paper, I sketch the connection of Hilbert's considerations to issues in the foundations of mathematics during the second half of the 19th century, describe the work that laid the basis of modern mathematical logic, and analyze the first steps in the new subject of proof theory. A revision of the standard view of Hilbert's and Bernays's contributions to the foundational discussion in our century has long been overdue. It is almost scandalous that their carefully worked out notes have not been used yet to understand more accurately the evolution of modern logic in general and of Hilbert's Program in particular. One conclusion will be obvious: the dogmatic formalist Hilbert is a figment of historical (de)construction! Indeed, the study and analysis of these lectures reveal a depth of mathematical-logical achievement and of philosophical reflection that is remarkable. In the course of my presentation many questions are raised and many more can be explored; thus, I hope this paper will stimulate interest for new historical and systematic work.

In [12], Ernst Zermelo described a succession of models for the axioms of set theory as initial segments of a cumulative hierarchy of levels UαVα. The recursive definition of the Vα's is:

Thus, a little reflection on the axioms of Zermelo-Fraenkel set theory (ZF) shows that Vω, the first transfinite level of the hierarchy, is a model of all the axioms of ZF with the exception of the axiom of infinity. And, in general, one finds that if κ is a strongly inaccessible ordinal, then Vκ is a model of all of the axioms of ZF. (For all these models, we take ∈ to be the standard element-set relation restricted to the members of the domain.) Doubtless, when cast as a first-order theory, ZF does not characterize the structures 〈Vκ,∈∩(Vκ×Vκ)〉 for κ a strongly inaccessible ordinal, by the Löwenheim-Skolem theorem. Still, one of the main achievements of [12] consisted in establishing that a characterization of these models can be attained when one ventures into second-order logic. For let second-order ZF be, as usual, the theory that results from ZF when the axiom schema of replacement is replaced by its second-order universal closure. Then, it is a remarkable result due to Zermelo that second-order ZF can only be satisfied in models of the form 〈Vκ,∈∩(Vκ×Vκ)〉 for κ a strongly inaccessible ordinal.

The history of modern logic is usually written as the history of mathematical or, more general, symbolic logic. As such it was created by mathematicians. Not regarding its anticipations in Scholastic logic and in the rationalistic era, its continuous development began with George Boole's The Mathematical Analysis of Logic of 1847, and it became a mathematical subdiscipline in the early 20th century. This style of presentation cuts off one eminent line of development, the philosophical development of logic, although logic is evidently one of the basic disciplines of philosophy. One needs only to recall some of the standard 19th century definitions of logic as, e.g., the art and science of reasoning (Whateley) or as giving the normative rules of correct reasoning (Herbart).

In the paper the relationship between the philosophical and the mathematical development of logic will be discussed. Answers to the following questions will be provided:

1. What were the reasons for the philosophers' lack of interest in formal logic?

2. What were the reasons for the mathematicians' interest in logic?

3. What did “logic reform” mean in the 19th century? Were the systems of mathematical logic initially regarded as contributions to a reform of logic?

4. Was mathematical logic regarded as art, as science or as both?

After giving a brief overview of the renewal of interest in logic and the foundations of mathematics in Göttingen in the period 1914-1921, I give a detailed presentation of the approach to the foundations of mathematics found in Behmann's doctoral dissertation of 1918, Die Antinomie der transfiniten Zahl und ihre Auflösung durch die Theorie von Russell und Whitehead. The dissertation was written under the guidance of David Hilbert and was primarily intended to give a clear exposition of the solution to the antinomies as found in Principia Mathematica. In the process of explaining the theory of Principia, Behmann also presented an original approach to the foundations of mathematics which saw in sense perception of concrete individuals the Archimedean point for a secure foundation of mathematical knowledge. The last part of the paper points out an important numbers of connections between Behmann's work and Hilbert's foundational thought.

This paper is an edited form of a letter written by the two authors (in the name of Tarski) to Wolfram Schwabhäuser around 1978. It contains extended remarks about Tarski's system of foundations for Euclidean geometry, in particular its distinctive features, its historical evolution, the history of specific axioms, the questions of independence of axioms and primitive notions, and versions of the system suitable for the development of 1-dimensional geometry.

In 1883, while a student of C. S. Peirce at Johns Hopkins University, Christine Ladd-Franklin published a paper titled On the Algebra of Logic, in which she develops an elegant and powerful test for the validity of syllogisms that constitutes the most significant advance in syllogistic logic in two thousand years. Sadly, her work has been all but forgotten by logicians and historians of logic. Ladd-Franklin's achievement has been overlooked, partly because it has been overshadowed by the work of other logicians of the nineteenth century renaissance in logic, but probably also because she was a woman. Though neglected, the significance of her contribution to the field of symbolic logic has not been diminished by subsequent achievements of others.

In this paper, I bring to light the important work of Ladd-Franklin so that she is justly credited with having solved a problem over two millennia old. First, I give a brief survey of the history of syllogistic logic. In the second section, I discuss the logical systems called “algebras of logic”. I then outline Ladd-Franklin's algebra of logic, discussing how it differs from others, and explain her test for the validity of the syllogism, both in her symbolic language and the more familiar language of modern logic. Finally I present a rigorous proof of her theorem. Ladd-Franklin developed her algebra of logic before the methods necessary for a rigorous proof were available to her. Thus, I do now what she could not have done then.

The fundamental question in reverse mathematics is to determine which set existence axioms are required to prove particular theorems of mathematics. In addition to being interesting in their own right, answers to this question have consequences in both effective mathematics and the foundations of mathematics. Before discussing these consequences, we need to be more specific about the motivating question.

Reverse mathematics is useful for studying theorems of either countable or essentially countable mathematics. Essentially countable mathematics is a vague term that is best explained by an example. Complete separable metric spaces are essentially countable because, although the spaces may be uncountable, they can be understood in terms of a countable basis. Simpson (1985) gives the following list of areas which can be analyzed by reverse mathematics: number theory, geometry, calculus, differential equations, real and complex analysis, combinatorics, countable algebra, separable Banach spaces, computability theory, and the topology of complete separable metric spaces. Reverse mathematics is less suited to theorems of abstract functional analysis, abstract set theory, universal algebra, or general topology.

Section 2 introduces the major subsystems of second order arithmetic used in reverse mathematics: RCA0, WKL0, ACA0, ATR0 and – CA0. Sections 3 through 7 consider various theorems of ordered group theory from the perspective of reverse mathematics. Among the results considered are theorems on ordered quotient groups (including an equivalent of ACA0), groups and semigroup conditions which imply orderability (WKL0), the orderability of free groups (RCA0), Hölder's Theorem (RCA0), Mal'tsev's classification of the order types of countable ordered groups ( – CA0)

Some of the most important developments of symbolic logic took place in the 1920s. Foremost among them are the distinction between syntax and semantics and the formulation of questions of completeness and decidability of logical systems. David Hilbert and his students played a very important part in these developments. Their contributions can be traced to unpublished lecture notes and other manuscripts by Hilbert and Bernays dating to the period 1917–1923. The aim of this paper is to describe these results, focussing primarily on propositional logic, and to put them in their historical context. It is argued that truth-value semantics, syntactic (“Post-”) and semantic completeness, decidability, and other results were first obtained by Hilbert and Bernays in 1918, and that Bernays's role in their discovery and the subsequent development of mathematical logic is much greater than has so far been acknowledged.

We introduce a logic BI in which a multiplicative (or linear) and an additive (or intuitionistic) implication live side-by-side. The propositional version of BI arises from an analysis of the proof-theoretic relationship between conjunction and implication; it can be viewed as a merging of intuitionistic logic and multiplicative intuitionistic linear logic. The naturality of BI can be seen categorically: models of propositional BI's proofs are given by bicartesian doubly closed categories, i.e., categories which freely combine the semantics of propositional intuitionistic logic and propositional multiplicative intuitionistic linear logic. The predicate version of BI includes, in addition to standard additive quantifiers, multiplicative (or intensional) quantifiers and which arise from observing restrictions on structural rules on the level of terms as well as propositions. We discuss computational interpretations, based on sharing, at both the propositional and predicate levels.

Certain set theoretical notions cannot be split into finer subnotions.

In program synthesis, we transform a specification into a system that is guaranteed to satisfy the specification. When the system is open, then at each moment it reads input signals and writes output signals, which depend on the input signals and the history of the computation so far. The specification considers all possible input sequences. Thus, if the specification is linear, it should hold in every computation generated by the interaction, and if the specification is branching, it should hold in the tree that embodies all possible input sequences.

Often, the system cannot read all the input signals generated by its environment. For example, in a distributed setting, it might be that each process can read input signals of only part of the underlying processes. Then, we should transform a specification into a system whose output depends only on the readable parts of the input signals and the history of the computation. This is called synthesis with incomplete information. In this work we solve the problem of synthesis with incomplete information in its full generality. We consider linear and branching settings with complete and incomplete information. We claim that alternation is a suitable and helpful mechanism for coping with incomplete information. Using alternating tree automata, we show that incomplete information does not make the synthesis problem more complex, in both the linear and the branching paradigm. In particular, we prove that independently of the presence of incomplete information, the synthesis problems for CTL and CTL*. are complete for EXPTIME and 2EXPTIME, respectively.

The class of all recursive functions fails to possess a natural hierarchical structure, generated predicatively from “within”. On the other hand, many (proof-theoretically significant) sub-recursive classes do. This paper attempts to measure the limit of predicative generation in this context, by classifying and characterizing those (predictably terminating) recursive functions which can be successively defined according to an autonomy condition of the form: allow recursions only over well-orderings which have already been “coded” at previous levels. The question is: how can a recursion code a well-ordering? The answer lies in Girard's theory of dilators, but is reworked here in a quite different and simplified framework specific to our purpose. The “accessible” recursive functions thus generated turn out to be those provably recursive in ( –CA)0.

The Lévy-Solovay Theorem[8] limits the kind of large cardinal embeddings that can exist in a small forcing extension. Here I announce a generalization of this theorem to a broad new class of forcing notions. One consequence is that many of the forcing iterations most commonly found in the large cardinal literature create no new weakly compact cardinals, measurable cardinals, strong cardinals, Woodin cardinals, strongly compact cardinals, supercompact cardinals, almost huge cardinals, huge cardinals, and so on.