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 http://math.stanford.edu/~feferman/papers.html, item #9.
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.
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.
Reference
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.
Reference
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.
References
The epsilon substitution method was introduced by Hilbert as a basic tool of his consistency program. Its extension to the impredicative case of ID_{1} 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.