[FOM] Troelstra's Paradox and Markov's Principle

[Ben Sherman]

> On December 29, 2016 at 4:57:54 AM EST, Frank Waaldijk <fwaaldijk at gmail.com> wrote:
> 
> You will understand that I am a little sceptical, especially since no effort seems to have been made to really develop analysis with Formal Topology methods. The fact that there is no clear, non-changing, axiomatic and definitional framework for Formal Topology doesn't help me lose this skepsis.

I want to take this opportunity to point to some work that has been done to develop analysis (or at least what I consider analysis) with formal topology or equivalent methods:

Steve Vickers. "A localic theory of lower and upper integrals". 2008.
https://www.cs.bham.ac.uk/~sjv/integration.pdf

Steve Vickers. "A monad of valuation locales". 2011.
https://www.cs.bham.ac.uk/~sjv/Riesz.pdf

Steve Vickers. "Localic completion of generalized metric spaces I". 2005.
http://www.tac.mta.ca/tac/volumes/14/15/14-15.pdf

Steve Vickers. "Compactness in locales and in formal topology". 2006.
https://www.cs.bham.ac.uk/~sjv/CompLocFT.pdf

Thierry Coquand and Bas Spitters. "Integrals and Valuations". 2009.
https://arxiv.org/abs/0808.1522

These papers might be hard to find if you're searching for formal topology: the papers referenced above often use a different, but equivalent, formalism to formal topology, and either do not mention the connection explicitly, or do so briefly. Steve Vickers has many other papers which you may also consider relevant.

In my view, I think these works give evidence that formal topology works well for developing analysis.