Abstract:

 I will talk about Halpern-Läuchli Theorem (HL) and its proof(s). This is an ongoing project with Chong Chitat and Li Wei at National University of Singapore, aiming to find the proof-theoretic strength of HL. I will sketch a proof that under Σ3-induction, there is a computable solution for HL. Necessary definitions will be introduced.