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

Ben Sherman sherman at csail.mit.edu
Mon Jan 2 14:44:56 EST 2017

> 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.

Steve Vickers. "A monad of valuation locales". 2011.

Steve Vickers. "Localic completion of generalized metric spaces I". 2005.

Steve Vickers. "Compactness in locales and in formal topology". 2006.

Thierry Coquand and Bas Spitters. "Integrals and Valuations". 2009.

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.

More information about the FOM mailing list