Mathematical Logic Seminar Abstracts Spring 2009

Solomon Feferman (Stanford)
Introduction to Systems of Notation for Predicative Ordinals (And Beyond): Completeness and Effectiveness Properties

As background for the talks April 28 and May 5 on the work of Beklemishev relating systems of notation for predicative ordinals to provability algebras, I will go over material from my paper “Systems of predicative analysis, II: Representations of ordinals”, J. Symbolic Logic 33 (1968) 193–220, that is also available at, item #9.

Peter Koellner (Harvard)
Intrinsic Justifications and Reflection Principles

Gödel initiated the program of finding and justifying axioms that effect a significant reduction in incompleteness and he drew a fundamental distinction between intrinsic and extrinsic justifications. Reflection principles are the most promising candidates for new axioms that are intrinsically justified. Taking as our starting point Tait's work on general reflection principles, we will discuss a series of limitative results concerning this approach. These results collectively show that general reflection principles are either weak (in that they are consistent relative to the Erdős cardinal κ(ω)) or inconsistent. The philosophical significance of these results is discussed.

Grigori Mints (Stanford)
Review of L. Beklemishev's “Reflection schemata and provability algebras in formal arithmetic”

Proof-theoretic ordinals are used to measure the consistency strength of formal theories and growth rate of computable functions. Defining suitable ordinals for strong theories is one of the most important outstanding problems of proof theory and foundations. It is not even clear what is suitable “material” for such definitions. One of the popular candidates is consistency statements.

We outline the problem and describe a solution for the ordinal ε0 (cosistency stength of the first order arithmetic) given by L. Beklemishev.


Thomas Icard (Stanford)
Review of L. Beklemishev's “Veblen hierarchy in the context of provability algebras”

In the previous seminar on May 5, we had a presentation of Beklemishev's solution to the problem of providing a canonical ordinal notation system up to ε0, the consistency strength of first-order arithmetic. A natural question is how this can be extended beyond ε0 to larger ordinals measuring the strength of, e.g., fragments of second order arithmetic. I shall present Beklemishev's own proposal for how to extend the system up to the ordinal Γ0, the consistency strength predicative analysis.


Johan van Benthem (Stanford, Amsterdam)
The Information in Logic: Dynamic Epistemic Logic Meets Intuitionism

The notion of information is implicit in many logical systems, but it takes a (de-)constructive effort to make it explicit, especially as notions of information appropriate to logic are diverse, and not all charted. We start with dynamic epistemic logic of observation-based semantic information, and first show how it needs protocol extensions to deal with 'procedural information'. In addition, it needs syntactic access structure for inferential update, and acts of 'promotion' giving conscious access to implicit knowledge. Next, we discuss a major alternative in this light: intuitionistic logic as a theory of implicit information, 'epistemically loading' meanings of logical constants. The latter system merges three kinds of information: factual, procedural, and inferential, in a mix that is tantalizingly different from that of dynamic epistemic logic. Finally, we discuss some other dimensions: 'loading' versus addition, and the role of (constructive) proof interpretations.

This talk connects several ideas in the DEL literature, but takes them in a perhaps surprising direction: the heartrland of constructivism.


Grigori Mints (Stanford)
A Simple Epsilon Substitution Method for ID1

The epsilon substitution method was introduced by Hilbert as a basic tool of his consistency program. Its extension to the impredicative case of ID1 was outlined in my paper (2000) and carried out by T. Arai. Unfortunately his formulation and termination proof are very complicated. In this talk a much simpler formulation and termination proof are presented. The simplification is based on simple recursion-theoretic considerations.