We discuss the computational content of Nonstandard Analysis based on recent proof-theoretic developments.
Sam Sanders
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.
