Mathematical Logic Seminar Abstracts Spring 2008

Thomas Icard (Stanford)
Semantics of Polymodal Gödel-Löb Logic

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.

Victor Harnik (Haifa)
The Syntax of Object Specification in Higher Dimensional Categories

An n-dimensional category (in short, n-category) has, for every kn, 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.

Henry Towsner (UCLA, Berkeley)
Partial Dialectica Translations and Szemerédi's Theorem

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.)

Robert Solovay (Berkeley)
The Consistency Strength of NFU*

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”.

Ryota Akiyoshi (Tokyo)
An Ordinal-free Proof of the Cut Elimination Theorem for Π11-Analysis with ω-rule

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

Gordon Plotkin (Edinburgh)
A Model of Cooperative Threads

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.

Grigori Mints (Stanford)
Analytic Cut in Modal Logic

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.

Solomon Feferman (Stanford)
The Proof Theory of Classical and Inductive Definitions: A 40-year Saga

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, item #67.