Specker sequences and their relevance to Proof Mining

Add to your list(s) Download to your calendar using vCal

• Morenikeji Neri
• Thursday 17 March 2022, 14:00-15:00
• LG23, SoCS and Zoom (see abstract for link).

If you have a question about this talk, please contact Anupam Das.

The Proof Mining project aims to see what quantitative information can be extracted from proofs using techniques from proof theory. A classic example of this is the following: Given a proof that a sequence converges, can we extract a rate of convergence? In this talk, I will present some important theoretical results in this direction. Firstly, I will outline E. Specker’s proof that there exist convergent sequences of computable numbers which don’t have a rate of convergence. However, not all hope is lost! Applying the classical functional interpretation to the statement of Cauchy convergences yields what is known as a ‘rate of metastability’ which, like a rate of convergence, provides extra quantitative information about the convergence of a sequence. I will explain what this is, and then give some new examples from work in progress where both rates of convergence and rates of metastability have been extracted from convergence proofs. Lastly, I will outline some ongoing work on formalising concepts from proof mining and computable analysis in the Lean proof assistant, where in particular I have formalised Specker’s construction, defined the concepts of computable rates of convergence and metastability, and I have proved basic lemmas related to how they interact with Cauchy convergence as well as each other.

==== Zoom details ====

https://bham-ac-uk.zoom.us/j/81873335084?pwd=T1NaUFg2U1l6d0RLL2RlTzFBam1IUT09

Meeting ID: 818 7333 5084 Passcode: 217

This talk is part of the Lab Lunch series.

This talk is included in these lists:

• LG23, SoCS and Zoom (see abstract for link)
• Lab Lunch

Note that ex-directory lists are not shown.