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. The Syntax of Object Specification in Higher Dimensional Categories An n-dimensional category (in short, n-category) has, for every k ≤ n, k-dimensional objects that are called k-cells.
0, MedicGLP 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. 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. 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.
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. It turns out to have precisely the consistency strength of ZC (Zermelo Set Theory with choice) plus Σ2-Replacement. 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 MedicGLP explain how to extend our proof into the full Π11-analysis with ω-rule. This is joint work with Grigori Mints. 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. 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 MedicGLP 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. 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.