Differential equations in constructive analysis and in the recursive realizability topos (Q793725)

This paper is concerned with the constructive theory of differential equations, as cast in the following three settings: (1) as provable in Heyting's arithmetic \(+\) ''Every f:\(N\to N\) is recursive''; (2) as true in the recursive realizability topos [\textit{J. M. E. Hyland}, The L. E. J. Brouwer Centen. Symp., Proc. Conf., Noordwijkerhout/Holl. 1981, Stud. Logic Found. Math. 110, 165-216 (1982; Zbl 0522.03055)]; (3) in computable analysis in which all assumptions are made computable [cf. \textit{O. Aberth}, Computable analysis (1980; Zbl 0461.03015), in contrast with \textit{M. B. Pour-El} and \textit{I. Richards}, Adv. Math. 39, 215-239 (1981; Zbl 0465.35054)]. It is shown that in this constructive recursive context one has the existence of approximate solutions, and the Picard uniqueness and existence theorem for ordinary differential equations, as well as the standard uniqueness and existence theorems for the wave equation and the heat equation. On the other hand, the Cauchy-Peano existence theorem for ordinary differential equations is even refutable in the theory mentioned in (1), but it does not constructively imply the Heine-Borel theorem, in contrast with the classical setting of [\textit{S. G. Simpson}, J. Symb. Logic 49, 783-802 (1984)].