
We introduce the notion of feedback computable functions from $2^\omega$ to
$2^\omega$, extending feedback Turing computation in analogy with the standard
notion of computability for functions from $2^\omega$ to $2^\omega$. We then
show that the feedback computable functions are precisely the effectively Borel
functions. With this as motivation we define the notion of a feedback
computable function on a structure, independent of any coding of the structure
as a real. We show that this notion is absolute, and as an example characterize
those functions that are computable from a Gandy ordinal with some finite
subset distinguished.

BDN is a weak principle of constructive analysis. Several interesting
principles implied by BDN have already been identified, namely the closure of
the antiSpecker spaces under product, the Riemann Permutation Theorem, and the
Cauchyness of all partially Cauchy sequences. Here these are shown to be
strictly weaker than BDN, yet not provable in set theory alone under
constructive logic.

Varieties of the Fan Theorem have recently been developed in reverse
constructive mathematics, corresponding to different continuity principles.
They form a natural implicational hierarchy. Some of the implications have been
shown to be strict, others strict in a weak context, and yet others not at all,
using disparate techniques. Here we present a family of related Kripke models
which separates all of the as yet identified fan theorems.

We develop a realizability model in which the realizers are the reals not
just Turing computable in a fixed real but rather the reals in a countable
ideal of Turing degrees. This is then applied to prove several separation
results involving variants of the Fan Theorem.