Computable Real Analysis without Set Theory or Turing Machines

Abstract:

The many schools of computable or constructive analysis
accept without question the received notion of set with structure.
They rein in the wild behaviour of set-theoretic functions
using the double bridle of topology and recursion theory,
adding encodings of explicit numerical representations
to the epsilons and deltas of metrical analysis.
Fundamental conceptual results such as the Heine--Borel theorem
can only be saved by set-theoretic tricks such as
Turing tapes with infinitely many non-trivial symbols.

It doesn't have to be like that.

When studying computable continuous functions,
we should never consider uncomputable or discontinuous ones,
only to exclude them later.
By the analogy between topology and computation,
we concentrate on open subspaces.
So we admit $+$, $-$, $\times$, $\div$, $<$, $>$, $\neq$, $\land$ and~$\lor$,
but not $\leq$, $\geq$, $=$, $\lnot$ or~$\Rightarrow$.
Universal quantification captures the Heine--Borel theorem,
being allowed over \emph{compact} spaces.
Dedekind completeness can also be presented in a natural logical style
that is much simpler than the constructive notion of Cauchy sequence,
and also more natural for both analysis and computation.

Since open subspaces are defined as continuous functions to the
Sierpi\'nski space, rather than as subsets,
they enjoy a ``de~Morgan'' duality with closed subspaces
that is lost in intuitionistic set-, type- or topos theories.
Dual to $\forall$ compact spaces is $\exists$ over ``overt'' spaces.
Classically, all spaces are overt,
whilst other constructive theories use explicit enumerations
or distance functions instead.
Arguments using $\exists$ and overtness are both dramatically simpler
and formally dual to familiar ideas about compactness.