By global Peano existence theorem I mean the existence of a maximal interval of solution of a first order ODE $x'=f(x,t)$ with continuous $f$. The proofs of the global Peano Theorem found in the literature often simply appeal to Zorn’s Lemma; eg. Theorem 4.7 in Ganesh
S. S. Ganesh, Lecture Notes on Ordinary Differential Equations, Annual Foundation School IIT Kanpur, December 3 - 28, 2007, 34 pp. https://www.math.iitb.ac.in/~siva/afs07.pdf
The more careful proofs depend on ADC, usually without mentioning it explicitly. Hale
J. Hale, Ordinary Differential Equations, 2nd Edition, R. E. Krieger Publ. Co., Florida, 1980
in his proof of global Peano Theorem (Theorem 2.1, p. 17) writes:
“...there is a monotone increasing sequence {bn} constructed as above so that the solution $x(t)$ of (1.1) on $[a, b]$ has an extension to the interval $[a, b_n]$ and $(b_n, x(b_n))$ is not in $V_n$. Since the $b_n$ are bounded above, let $\omega = \lim_{n\to\infty} b_n$. It is clear that $x$ has been extended to the interval $[a, \omega)$...”
What is actually clear is that his construction yields solutions $x_n(t)$ on $[a, b_n]$ for each $n$, and each $x_n(t)$ has extensions to some $x_{n+1}(t)$. ADC is needed to justify the existence of $x(t)$. Similarly Hartman
P. Hartman, Ordinary Differential Equations, 2nd Edition, SIAM, Philadelphia, 2002
in the proof of II, 3.1, p. 13, constructs an increasing sequence $\{b_n\}$ such that any solution on $[a, b_n]$ has an extension to a solution on $[a, b_{n+1}]$. ADC is needed to justify the existence of a solution on $[a, \omega^+]$ for $\omega^+ = \lim_{n\to\infty} b_n$. In the proof of III, Lemma 3.1, a key step to the proof of III, 3.1 (Osgood’s Theorem), ACC is used implicitly to choose the sequence $\{u_n(t)\}$. Similar unacknowledged use of ADC appears on pp. 355–356 in
J. Kurzweil, Ordinary Differential Equations. Introduction to the Theory of Ordinary Differential Equations in the Real Domain, translated from the Czech by M. Basch, Studies in Applied Mechanics, 13, Elsevier Scientific Publishing, Amsterdam, 1986.
Is there a published proof of global Peano existence that's valid in ZF?