TL;DR: Dag Normann and I have obtained LOTS of equivalences between the second-order Big Five of Reverse Mathematics and third-order theorems from mainstream analysis about (possibly) discontinuous functions, working in Kohlenbach’s higher-order Reverse Mathematics. We also show that slight generalisations or variations of the aforementioned third-order theorems fall FAR outside of the Big Five. Our…
Sam Sanders
The computational content of Nonstandard Analysis
We discuss the computational content of Nonstandard Analysis based on recent proof-theoretic developments.
Lifting proofs: from Specker sequences to nets
This post provides an answer to the question: Can we somehow ‘lift’ proofs in a restricted language to interesting proofs in a richer language?
Of representations of mathematics
Studying mathematics via logic implies one needs to choose a suitable logical language and represent part of mathematics therein. This post deals with the question whether such representations remain true to the original, or somehow distort it. I show that even the well-known representation of continuous functions leads to significant distortion.
