“Completeness: Turing, Schütte, Feferman (and Löb)”
Martedì 5 Aprile 2022, ore 16:30 - Aula 1A150 - Michael Rathjen (University of Leeds)
Abstract
Progressions of theories along paths through Kleene’s $\mathcal O$, adding the consistency of the previous theory at every successor step, can deduce every true $\Pi^0_1$-statement. This was shown by Turing in his 1938 thesis who called these progressions “ordinal logics”.
In 1962 Feferman proved the amazing theorem that progressions based on the “uniform reflection principle” can deduce every true arithmetic statement. In contrast to Turing’s, Feferman’s proof is very complicated, involving several cunning applications of self-reference via the recursion theorem.
Using Schütte’s method of search trees (or decomposition trees) for $\omega$-logic and reflexive induction, however, one can give a rather transparent proof.
The main aim of the talk is to present a general proof-theoretic machinery, based on search trees, and discuss intensional and extensional aspects of metamathematical results.
