An induction principle for consequence in arithmetic universes (Q456884)

An arithmetic universe is a pretopos in which there is an object \(\mathsf{List}(A)\) with the obvious constructors and a recursion predicate, all of them encoded as suitable arrows. In this context, the article proves that, given two predicates \(\phi\) and \(\psi\) for natural numbers satisfying a base case \(\phi(0) \to \psi(0)\) and an induction step that, for generic \(n\), the hypothesis \(\phi(n) \to \psi(n)\) allows one to deduce \(\phi(n + 1) \to \psi(n + 1)\), then it is already true in that arithmetic universe that \((\forall n)(\phi(n) \to \psi(n))\). Since arithmetic universes, being pretoposes, do not have exponentiation in general, this induction principle is substantially harder to prove than in a topos. The development is interesting in itself as it analyses a notion of ``subspace'' of an arithmetic universe, including open and closed subspaces and a Boolean algebra generated by them. Hence, the work provides some ``topological'' insight in the theory of arithmetic universes which could be of interest beyond the specific result in the article. The paper concludes with the application of the induction principle to locatedness of Dedekind sections: once again, the topological nature of the induction principle in the considered context becomes evident, making the example both clarifying and potentially inspiring.