@EugeneZhang Yes, I believe so. (I have a macro on my keyboard that transform \phi into the Unicode symbol φ [which has the LaTeX commend of \varphi], and the macro probably didn't work for that one instance)

Thanks for the answer! I still didn't have time to go through the answer in depth, but about the last paragraph, $A^{<\omega}$ is not Dedekind finite (as witness by e.g. constant $a$ sequence of length $n$ for fixed $a$). I think we want to look only at $A^{1-1}×A$, the surjectivity argument should still follow

@GuozhenShen I did thought about trying to force such surjection (e.g. starting with Cohen model, and trying to add a surjection to the reals from the canonical Dedekind set) but I couldn't quite see how it will turn out

@GuozhenShen thanks, I'll check the paper out.

@MikhailKatz everything in Peano's theorem is countably coded, so you don't lose anything when translating it to ZF. Sometimes you do have cases where WKL_0 (or other weak systems) proves statement A but not prove statement B, but ZF- (or other strong system) prove that A is equivalent to B, fortunately it is not the case here, Simpson proved Peano's theorem in it's original form

@MikhailKatz Lebesgue measurable sets are not countably coded

@MikhailKatz by "pure existential statement" James means Peano's existence theorem without the additional "global" condition (that there is a maximal interval). Not sure what you mean by "equivalent to the usual ZF version", ZF proves everything that ${\sf {WKL}}_0$ can prove when talking about sets of naturals (i.e. reals)

Stephen G. Simpson has shown that over RCA_0, Peano's existence theorem is equivalent to WKL. I would imagine that adding the maximality condition is possible without too much effort