2016/06/19 by Sam Sanders
Computer Science · Mathematics · #Calculus (dental) #Computability #Computability, Logic, AI Algorithms #Content (measure theory) #Logic, programming, and type systems #Mathematical and Theoretical Analysis #Proof theory #Quantifier (linguistics) #Scope (computer science) #Work (physics) #cs.LO
paper · pdf · doi:10.4204/eptcs.213.3
published as EPTCS 213, 2016, pp. 24-40 · In Proceedings CL&C 2016, arXiv:1606.05820
openalex publication_date 2016/06/19 · arxiv created 2016/06/21 · arxiv updated 2016/06/22 · openalex created_date 2016/06/24 · openalex updated_date 2026/08/05
Kohlenbach's proof mining program deals with the extraction of effective information from typically ineffective proofs. Proof mining has its roots in Kreisel's pioneering work on the so-called unwinding of proofs. The proof mining of classical mathematics is rather restricted in scope due to the existence of sentences without computational content which are provable from the law of excluded middle and which involve only two quantifier alternations. By contrast, we show that the proof mining of classical Nonstandard Analysis has a very large scope. In particular, we will observe that this scope includes any theorem of pure Nonstandard Analysis, where `pure' means that only nonstandard definitions (and not the epsilon-delta kind) are used. In this note, we survey results in analysis, computability theory, and Reverse Mathematics.