Mathematical Logic Seminar Abstracts Winter 2009

Grigori Mints (Stanford)
Reviews of Two Recent Papers
• Baaz, Matthias and Wojtylak, Piotr: “Generalizing proofs in monadic languages” (with a postscript by Georg Kreisel). Annals of Pure and Applied Logic 154(2), 71–138 (2008).

Kreisel's conjecture stated that if Peano Arithmetic PA proves A(Sn0) for each n by a proof with ≤ k lines then PA proves ∀xA(x). It had been proved by R. Parikh (Zbl 0269.02011) for a monadic formulation of PA with S as the only function and predicates for addition and multiplication. The paper under review provides a detailed treatment in numerous special cases for the following drastic modification by G. Kreisel (in a supplement to Zbl 0609.03019).

Suppose that π is a proof of A(Sn0) for just one (but large) n. Then there is an infinite set X(Π,A) ⊆ N with proofs of the same logical form Π π for all A(Sm0) with mX(Π,A). The central notion in the reviewed paper is uniform derivability of a schema (by one and the same proof schema for all instances) instead of derivability in k steps. Descriptions of the sets X(Π,a) are derived from the properties of linear diophantine equations describing the proof schema. Equivalent (with respect to the set of theorems) formulations of PA behave differently in this respect. The ordinary successor induction gives uniform proofs of ∃x(x+x=S2n0), whereas the order induction schema ∀α(∀β<α A(β) → A(α)) → ∀α A(α) admits generalization from n sufficiently large to A(Snx). Hence the successor induction schema is not uniformly derivable from order induction, while the other direction holds in the presence of finitely many basic arithmetical axioms. A long postscript by G. Kreisel supplements and criticizes the main body of the paper.

• Colson, Loïc and Michel, David: “Pedagogical second-order propositional calculi”. Journal of Logic and Computation 18(4), 669–695 (2008).

Proper subsystems Ps-Prop2 and P-Prop2 of the ordinary intuitionistic propositional calculus Prop2 considered here are negationless in the sense that negation is not definable and all subformulas are “motivated”: if A1,…,AnF then there is a substitution σ such that ⊦ σ A1,… ⊦ σ An, ⊦ σ F. This is achieved by restriction on the axioms introducing assumptions of natural deduction: Γ,AA is an axiom only if ⊦ σ A for some substitution σ. “Initial” σ simply substitutes ⊤ (truth) for everything. Restricted subsystems Ps-Prop2 and P-Prop2 are intertranslatable with Prop2 by devices similar to (but simpler than) ones used earlier by other authors for predicate logic and arithmetic.

Philipp Gerhardy (Oslo)
Proof Mining in Topological Dynamics

The Multiple Birkhoff Recurrence theorem by Furstenberg and Weiss in 1978 is a seminal result for the interaction between topological dynamics and combinatorics, establishing Ramsey-type theorems through corresponding recurrence results. However, while combinatorial proofs often contain explicit quantitative information, topological proofs usually do not contain realizers, bounds or similar data. E.g. for van der Waerden's theorem—for every finite colouring of the integers one colour contains arbitrarily long arithmetic progressions—one may ask for a number N = N(q; k) such that for every q-colouring of [0;N], one colour contains a progression of length k. The combinatorial proof contains an explicit upper bound on N(q; k), while Furstenberg and Weiss' topological proof does not. Thus one may ask: what is the algorithmic content of the topological proofs of Ramsey-type theorems. We will present an analysis of Furstenberg and Weiss' Multiple Birkhoff Recurrence theorem which generalizes a previous analysis by Girard. We will also discuss the use of compactness in proofs of the Multiple Birkhoff Recurrence theorem, i.e. the concept of minimality in topological dynamics, sketch the treatment of generalizations of the Multiple Birkhoff Recurrence theorem, and, if time permits, survey some related proof mining results in ergodic theory.

John Burgess (Princeton)
Putting Structuralism in Its Place

Modern logic was originally developed in large part in order to provide a mathematical model of theorem-proving, a model about which theorems could be proved. Differences between a mathematical model and what is modeled are only to be expected, but in the case of logic, these have sometimes provoked rather strange reactions. One difference, in particular, has given rise to rather extravagant philosophical claims under the label “structuralism”. A closer look at the logic of the situation suggests a way of improving the modeling and avoiding the extravagance.

Edward Zalta (Stanford)
A Defense of Logicism

In this talk, I extend the argument in the paper “What is Neologicism?” co-authored with Bernard Linsky (Bulletin of Symbolic Logic 12(1), June 2006, 60–99). Linsky and I argued that if the notion of reduction used by the original logicists is weakened, a new form of neologicism emerges that can be generally applied to arbitrary mathematical theories. In the present talk, however, I develop positive arguments for thinking: (1) that the notion of reduction assumed by the early logicists is the wrong notion of reduction given their epistemological motivations and goals; (2) that the notion of ‘ontological reduction’ defined in the paper “Neo-logicism? An Ontological Reduction of Mathematics to Metaphysics” (Erkenntnis, 53(1–2), 2000, 219–265) allows one to attain the epistemological goals driving logicism; (3) that when the comprehension principle for object theory is replaced by the equipotent abstraction principle, the resulting system is a logic, given that we accept that weak second-order logic is part of logic; and thus (4) logicism is true: since arbitrary mathematical theories are ontologically reducible in the logic of object theory, mathematics is reducible to logic.

Paul Eklof (Irvine)
Some Uses of Set Theory in Algebra

This will be a survey talk for non-experts in algebra. The applications covered will extend from Shelah's proof of the undecidability of the Whitehead Problem to recent algebraic theorems proved in ZFC using set-theoretic methods. A common theme is the use of the Singular Compactness Theorem.

Vaughan Pratt (Stanford)
Complex Linear Algebra from a Modification of Euclid's Postulates

We formulate the first three of Euclid's five postulates algebraically, and in lieu of postulates 4 and 5 postulate that every finite set of points has a centroid. We show that the variety of models of this algebraic theory is equivalent to the category VctQ[i] of vector spaces over the complex rationals. We complete any such model to a continuum, i.e. a vector space over the complex numbers, using only the geometric primitives defined by this theory, independently of any notion of number or metric. Various subtheories characterize the vector spaces over the reals, over the rationals, their affine (origin-free) counterparts, the Gaussian integers, etc.

The counterpart of abelian groups in this framework is a notion of grove arising naturally from Euclid's first two postulates. We show that sets and groves are algebraic in each other, giving a rare example of a structure as algebraically primitive as sets themselves.

This system differs from Hilbert's second-order and Tarski's first-order axiomatizations of geometry in four principal ways: it matches Euclid's original postulates more closely; its model theory at least for the rationals follows Szmielew in being more algebraic than Tarski's; each variant of the theory determines its underlying field up to isomorphism; and it limits itself to Euler's affine fragment of Euclidean geometry extended to the complex numbers.

Solomon Feferman (Stanford)
And So On…: Reasoning with Infinite Diagrams

Most theorems in mathematics state a fact about infinitely many objects of a certain kind, e.g. all triangles. But the diagram used in a proof only represents one such object, and it is an issue whether the particular representation taken is typical, i.e. does not have features which are not shared by all the objects under consideration. This is a frequent concern when dealing with proofs of geometric theorems that rely to a significant extent on diagrams. In this talk I'll bring attention to a different kind of diagram that is ubiquitous in modern mathematics, in which there is a single infinite configuration under consideration, and what is exhibited in the diagram is a typical finite part of that configuration, with the balance indicated by the use of dots (…) in some way. The consideration of such infinite diagrams is interesting because they enlarge the question of what makes a diagram typical. Moreover, I shall argue that there are certain proofs in modern mathematics where the use of such infinite diagrams is essential, i.e. it is not possible to even follow the proof without consulting the diagram at practically every step of the way. In fact, there are certain theorems that can't even be understood without reference to such a diagram.

Jesse Alama (Stanford)
Avigad, Dean and Mumma's “A formal system for Euclid's Elements

This presentation will be a review of a recent paper, "A formal system for Euclid's Elements", by J. Avigad, E. Dean, and J. Mumma. It is available electronically at

http://arxiv.org/abs/0810.4315 .
The authors give a formal system for faithfully expressing the Euclid's proofs in Elements, books 1–4 (on plane geometry), especially Euclid's diagram-based reasoning. The work advances the claim that Euclid's arguments are more rigorous than modern critics suggest. I shall review some key features of the formal system: its language, axioms and rules; the notion of a “direct consequence” (which is intended to capture what intuitively can be “read off” a diagram); ways in which the formalism adheres to and diverges from Euclid; completeness; and implementation.

Eric Pacuit (Stanford)
The Barcan Formula and Completeness of First-Order Modal Logic

In this talk, we will survey some recent work on completeness of first-order modal logics. In particular we will look at the role that the Barcan formula(s) play in various completeness proofs. We will focus on non-normal systems (cf. “First-Order Classical Modal Logic” by Horacio Arlo-Costa and Eric Pacuit, Studia Logica 84(2), 2006) and general completeness theorems (cf. “A General Semantics for Quantified Modal Logic” by Robert Goldblatt and Edwin Mares, Advances in Modal Logic 6, 2006). Time permitting we will also look at alternative semantics for the first-order modal language.