The polymodal logic of provability GLP captures the relationship between stronger and stronger provability predicates in formal arithmetic, a result due to Japaridze. This logic has also found applications in mainstream proof theory, in particular Beklemishev's work on ordinal analysis of Peano Arithmetic and subsystems thereof. After reviewing the arithmetical interpretation of GLP, relational and topological semantics will be discussed. One hindrance to working with GLP is that it is frame incomplete. First I shall present a simple ordinal (topological) interpretation of the letterless fragment, based on results from my masters thesis. Then I will talk about a current effort to try to extend this treatment to the full fragment, in order to obtain simple topological semantics of GLP with variables. This represents work in progress, joint with Lev Beklemishev and Guram Bezhanishvili.

An *n*-dimensional category (in short, *n*-category)
has, for every *k* ≤ *n*, *k*-dimensional
objects that are called k-cells. For *k* > 0, each such cell
has a domain and a codomain which are (*k*−1)-cells. The
cells can be combined with the help of composition operations. The
concept of n-category generalizes the familiar notion of category
(which is the same as 1-category).

We describe two formal languages, based on different sets of operations, having terms that specify composed cells. Each of the two languages has its advantages. Their comparison is facilitated when we construe them as free mathematical structures.

If time permits, I will outline the problem of defiing the concept of weak higher dimensional category. This is the broader context in which our sub ject came up.

This is joint work with Michael Makkai and Marek Zawadowski.

The usual ergodic proof of Szemerédi's Theorem uses a
transfinite tower to derive a combinatorial result. It is known that
this tower can have arbitrary countable height. Using a
“partial Dialectica translation”, applied only to the
transfinite parts of the argument, we can adapt the ergodic proof to
use only ω^{ω} levels of this tower. (Since this
talk will focus on the proof-theoretic aspects, I will not assume any
knowledge of ergodic theory.)

New Foundations (NF) is a rather strange variant of set theory proposed by Quine. Its consistency is still an open problem. Jensen proposed a variant, NFU, which is close in spirit to NF but which can be proved consistent.

I have computed the consistency strength of several variants of NFU
proposed by Randall Holmes. The topic of this talk is the system
NFU^{*}. It turns out to have precisely the consistency
strength of ZC (Zermelo Set Theory with choice) plus
Σ_{2}-Replacement. The proof exploits a variant of
Barwise compactness which holds for suitable models of “ZC +
Σ_{2}-Replacement + V=L”.

In this talk, we present an ordinal-free proof of the cut-elimination
theorem for Π_{1}^{1}-analysis with ω-rule
using Buchholz's Ω-rule. First we begin with a subsystem of
Π_{1}^{1}-analysis with ω-rule, and explain
how to extend our proof into the full
Π_{1}^{1}-analysis with ω-rule. This is joint
work with Grigori Mints.

We develop a model of concurrent imperative programming with threads. We focus on a small imperative language with cooperative threads which execute without interruption until they terminate or explicitly yield control. We define and study a trace-based denotational semantics for this language; this semantics is fully abstract but mathematically elementary. We also give an equational theory for the computational effects that underlie the language, including thread spawning. We then analyze threads in terms of the free algebra monad for this theory.

When standard approaches to cut elimination do not work, analytic cut (on subformulas of the proved formula) can be sufficient. We present a general framework for proving corresponding normalization theorem and apply it to two difficult cases: S5 and the system B characterized by Kripke models with reflexive and symmetric accessibility relations. The system B appeared in studies of vagueness by K. Fine and T. Williamson, and in a recent study of safe reasoning by T. Williamson.

This talk is a survey of work on formal theories of single and iterated inductive definitions given by arithmetical closure conditions, whose initial aim was to give an ordinally informative and perspicuous proof-theoretic reduction of these theories in classical logic to their constructive counterparts. The theories in question were first introduced in the early 1960's, but the aim only crystallized 40 years ago. Initially, the purpose was to obtain corresponding reductions of impredicative subsystems of analysis, but then the theories of inductive definitions became of interest in their own right. The historical progress of that work, which reaches up to the very present, is examined in terms of aims, methods and results.

The slides for this talk can be found at http://math.stanford.edu/~feferman/papers.html, item #67.