June 17
Mateusz Łełyk, University of Warsaw
Partial Reflection over Uniform Disquotational Truth

In the context of arithmetic, a reflection principle for a theory Th is a formal way of expressing that all theorems of Th are true. In the presence of a truth predicate for the language of Th this principle can be expressed as a single sentence (called the Global Reflection principle over Th) but most often is met in the form of a scheme consisting of all sentences of the form

$\forall x \bigl( \text{Prov}_{\text{Th}}(\phi(\dot{x}))\rightarrow \phi(x)\bigr).$
Obviously such a scheme is not provable in a consistent theory Th. Nevertheless, such soundness assertions are said to provide a natural and justified way of extending ones initial theory.

This perspective is nowadays very fruitfully exploited in the context of formal theories of truth. One of the most basic observations is that strong axioms for the notions of truth follow from formally weak types of axiomatizations modulo reflection principles. In such a way compositional axioms are consequences of the uniform disquotational scheme for for the truth predicate, which is

$\forall x\, \, T(\phi(\dot{x}))\equiv \phi(x).$

The above observation is also used in the recent approach to ordinal analysis of theories of predicative strength by Lev Beklemishev and Fedor Pakhomov. The assignment of ordinal notations to theories proceeds via partial reflection principles (for formulae of a fixed $\Sigma_n$ complexity) over (iterated) disquotational scheme. It becomes important to relate theories of this form to fragments of standard theories of truth, in particular the ones based on induction for restricted classes of formulae such as $\text{CT}_0$ (the theory of compositional truth with $\Delta_0$-induction for the extended language. The theory was discussed at length in Bartek Wcisło's talk). Beklemishev and Pakhomov leave the following open question:

Is $\Sigma_1$-reflection principle over the uniform disquotational scheme provable in $\text{CT}_0$?

The main goal of our talk is to present the proof of the affirmative answer to this question. The result significantly improves the known fact on the provability of Global Reflection over PA in $\text{CT}_0$. During the talk, we explain the theoretical context described above including the information on how the result fits into Beklemishev-Pakhomov project. In the meantime we give a different proof of their characterisation of $\Delta_0$-reflection over the disquotational scheme.

Despite the proof-theoretical flavour of these results, our proofs rests on essentially model-theoretical techniques. The important ingredient is the Arithmetized Completeness Theorem.

Slides

Video

​