- 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*(**S**^{n}**0**) for each*n*by a proof with ≤*k*lines then PA proves ∀*x**A*(*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*(**S**^{n}**0**) for just one (but large)*n*. Then there is an infinite set*X*(Π,*A*) ⊆with proofs of the same logical form Π π for all*N**A*(**S**^{m}**0**) with*m*∈*X*(Π,*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*=**S**^{2n}**0**), whereas the order induction schema ∀α(∀β<α*A*(β) →*A*(α)) → ∀α*A*(α) admits generalization from*n*sufficiently large to*A*(**S**^{n}*x*). 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

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

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.

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.

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.

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.

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
Vct_{Q}[*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.

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.

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.

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.