We discuss the computational content of Nonstandard Analysis based on recent proof-theoretic developments.
A new linear inference of size 8
Linear inferences are propositional tautologies of the form , where and are formulas with at most one occurrence of each propositional variable. These form a -complete set, but surprisingly little is known about their structure, despite their importance in structural proof theory (and beyond). In this post I will cover some of the background on…
What proof mining is about, Part II: Structures and metatheorems
As I said last time, it is time to raise the stakes and start dealing with sentences involving structures, which at first will be the structures of first-order logic. Let, then, be a first-order signature and be a family of -sentences. For the purposes of this post, we shall say, for any -structure , that…
Checking proofs with very low complexity
The very notion of mathematical proof is founded upon the idea that a proof is ‘routine’ to check. While it may be difficult to actually prove a mathematical theorem, a proof should allow us to verify its truth . But exactly how much effort is required to check a proof, in terms of computational complexity?…
