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.
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 Π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.
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.
The Syntax of Object Specification in Higher Dimensional Categories
Partial Dialectica Translations and Szemerédi's Theorem
The Consistency Strength of NFU*
An Ordinal-free Proof of the Cut Elimination Theorem for Π11-Analysis with ω-rule
A Model of Cooperative Threads
Analytic Cut in Modal Logic
The Proof Theory of Classical and Inductive Definitions: A 40-year Saga