Understanding Specker Sequences and Proof Mining
Learn about Specker sequences, their significance in computable analysis, and how they are relevant to proof mining. Explore the new definition of Specker sequences and the concept of rate of metastability.
Download Presentation
Please find below an Image/Link to download the presentation.
The content on the website is provided AS IS for your information and personal use only. It may not be sold, licensed, or shared on other websites without obtaining consent from the author. If you encounter any issues during the download, it is possible that the publisher has removed the file from their server.
You are allowed to download the files provided on this website for personal or commercial use, subject to the condition that they are used lawfully. All files are the property of their respective owners.
The content on the website is provided AS IS for your information and personal use only. It may not be sold, licensed, or shared on other websites without obtaining consent from the author.
E N D
Presentation Transcript
Specker Sequences and their relevance to Proof Mining
What is a Specker sequence The Standard definition of Specker sequences, found in computable analysis, is a monotone sequences of converging computable numbers whose limit is not computable The first construction of such a sequence was by Specker in 1949 and was used to demonstrate that the field of computable numbers did not satisfy the least upper bound property
New definition of Specker sequences Since the property of Specker s original sequence that was useful to us was the fact that the sequence didn t have a computable rate of convergence. In the context of Proof Mining we shall call any sequence of converging computable numbers, without a computable rate of convergence, a Specker sequence. This relaxation of the original definition therefore allows for the existence of sequences of computable numbers converging to computable limits to be Specker and we shall see that this can actually happen!
