Well-foundedness in realizability (Q850808)

The main result of this paper is that, for any realizability topos \(\mathcal R\) over a topos \(\mathcal S\) with natural number object, the global sections functor \(\Gamma:{\mathcal R}\to{\mathcal S}\) preserves and reflects well-foundedness of binary relations (provided `well-foundedness' is interpreted in the constructively sensible way: a relation is well-founded iff one has an induction principle for it). In particular, this result applies when \(\mathcal S\) is the classical topos of sets and \(\mathcal R\) is Hyland's effective topos, leading to particularly simple proofs of well-foundedness for appropriate relations in the latter. As an application, the authors develop a `generalized Markov Principle' and show that it holds in the effective topos.