Talk by Philip Welch (LTCS)

Short Title: 
Talk by Philip Welch
Event Date(s): 
Thursday, 1. March 2018 - 10:15 to 11:30

Room A097, ExWi, Sidlerstrasse 5, 3012 Bern

Prof. Dr. Philip Welch (University of Bristol)

Recursions of higher types and low levels of determinacy

We explore how generalisations of Kleene's theory of recursion in type 2 objects (which can be used to characterise complete Pi^1_1 sets and open determinacy) can be lifted to Sigma^0_3-Determinacy. The latter is the highest level in the arithmetical hierarchy whose determinacy is still provable in analysis. The generalisation requires the use of so-called infinite time Turing machines, and the levels of the Gödel constructible hierarchy needed to see that such machines models produce an output are, perhaps surprisingly, intimately connected with those needed to prove the existence of such strategies. The subsystem of analysis needed for this work is Pi^1_3-CA_0, and there is something suggestive of what may be needed to give a proof theory for this latter theory.