pith. machine review for the scientific record. sign in

arxiv: 2605.07128 · v1 · submitted 2026-05-08 · 💻 cs.SC · cs.CC· math.LO

Recognition: 1 theorem link

· Lean Theorem

Relating the Computational and Logical Difficulty of Solving ODEs: From Polynomial to Discontinuous Right-Hand Sides

Alonso N\'u\~nez, Olivier Bournez

Authors on Pith no claims yet

Pith reviewed 2026-05-11 02:37 UTC · model grok-4.3

classification 💻 cs.SC cs.CCmath.LO
keywords ordinary differential equationsinitial value problemsright-hand side regularitycomputational stratapolynomial timeundecidabilitytransfinite computationBig Five hierarchy
0
0 comments X

The pith

The regularity of the right-hand side function places each ODE initial value problem into one exact computational stratum, from polynomial-time solutions to transfinite computation.

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

The paper shows that the existence and properties of solutions to the initial value problem y prime of t equals f of t comma y of t with y of t zero equals y zero fall into distinct computational classes determined by how regular the function f is. This alignment is presented as exact and independent of how the problem is encoded. A sympathetic reader would care because it separates genuine barriers to solving ODEs from limits of particular solvers or models, covering cases from fast symbolic methods to undecidable ones.

Core claim

We prove that every level of the Big Five hierarchy is inhabited by a natural statement from classical ODE theory, as an exact equivalence: the regularity of f is an intrinsic algorithmic invariant placing the initial value problem y prime of t equals f of t comma y of t comma y of t zero equals y zero, into one of several computational strata, ranging from polynomial-time solvability to transfinite computation.

What carries the argument

The regularity condition on the right-hand side f of the ODE initial value problem, which serves as the invariant that assigns the problem to a specific computational and logical stratum.

If this is right

  • Polynomial right-hand sides permit quasi-linear time solutions over power series.
  • Continuous right-hand sides yield computable solutions whose difficulty can reach PSPACE-completeness over compact domains.
  • Discontinuous or less regular right-hand sides can require undecidable or higher-order computations.
  • The resulting stratification identifies intrinsic parameters such as length bounds, radii of convergence, and moduli of continuity that restore feasibility.
  • Symbolic solvers can be checked to determine whether failure stems from a fundamental barrier or from implementation limits.

Where Pith is reading between the lines

These are editorial extensions of the paper, not claims the author makes directly.

  • A practical ODE solver could first classify the regularity of f to select the appropriate solution method or resource estimate.
  • The same regularity-based classification might apply to other classes of differential equations beyond the initial value problem.
  • Numerical or symbolic implementations could use the identified parameters like moduli of continuity to switch between exact and approximate techniques.

Load-bearing premise

That there exist natural statements from classical ODE theory whose logical strength matches each level of the hierarchy without the particular statement or encoding introducing artifacts that alter the computational content.

What would settle it

An explicit ODE example whose solution requires a different level of computational resources or logical strength than the regularity class of its right-hand side f would predict.

read the original abstract

When a computer algebra system fails to solve an Ordinary Differential Equation, is this a limitation of its implementation, or a genuine computational barrier? Three traditions bear on the question. Modern computer algebra algorithms can be extremely efficient: Newton-type methods solve polynomial ODEs over $\mathbb{Q}[[X]]$ in quasi-linear time. Analog models of computation has shown that polynomial ODEs and Turing machines are two presentations of the same phenomenon, with solution length acting as time and precision as space. Computable analysis shows that ODEs can be intrinsically hard -- undecidable, even $\mathsf{PSPACE}$-complete, over compact domains. Comparing these traditions is natural and necessary, yet such comparisons routinely reduce to comparisons of encodings rather than of underlying algorithmic content. We argue that reverse mathematics provides a representation-invariant lens in which algorithmic content is compared directly. We prove that every level of the Big Five hierarchy is inhabited by a natural statement from classical ODE theory, as an exact equivalence: the regularity of $f$ is an intrinsic algorithmic invariant placing the initial value problem $y'(t)=f(t,y(t))$, $y(t_0)=y_0$, into one of several computational strata, ranging from polynomial-time solvability to transfinite computation. The resulting stratification acts as a practical diagnostic common to the three traditions. By abstracting from representation, it separates fundamental barriers from the technical shortcomings of symbolic solvers, the artefacts of analog encodings, and the effectivity constraints of computable analysis, identifying the intrinsic parameters (length bounds, radii of convergence, moduli of continuity) under which feasibility is restored.

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, simulated authors' rebuttal, and a circularity audit. Tearing a paper down is the easy half of reading it; the pith above is the substance, this is the friction.

Referee Report

2 major / 2 minor

Summary. The manuscript claims that reverse mathematics supplies a representation-invariant framework for classifying the computational difficulty of solving initial value problems y'(t)=f(t,y(t)), y(t0)=y0. It asserts exact equivalences over RCA0 between natural statements from classical ODE theory—parameterized by the regularity of f (polynomial, continuous, Lipschitz, discontinuous)—and each of the Big Five subsystems, ranging from polynomial-time solvability to statements requiring arithmetical transfinite recursion or Π¹₁-comprehension.

Significance. If the equivalences hold without encoding artifacts, the work would usefully bridge computer algebra, analog computation, and computable analysis by isolating intrinsic parameters (length bounds, radii of convergence, moduli of continuity) that determine feasibility. The identification of natural ODE statements inhabiting each level of the hierarchy is a concrete strength that could serve as a diagnostic separating fundamental barriers from implementation or representation issues.

major comments (2)
  1. [§5] §5 (discontinuous right-hand sides): the claimed equivalence of the existence statement for solutions to an ODE with discontinuous f to Π¹₁-CA0 must include an explicit formalization in the language of second-order arithmetic showing that the coding of the graph of f and the set of solutions does not presuppose a comprehension axiom; without this, the equivalence risks circularity as noted in the stress-test concern.
  2. [§4] Proof of the ATR0-level equivalence (likely §4): the construction must verify that the ODE statement is not defined using arithmetical transfinite recursion in the representation of the solution or the modulus of continuity, to ensure the equivalence is non-circular and the statement remains natural.
minor comments (2)
  1. [Introduction] The introduction would benefit from a short table or diagram summarizing the mapping from regularity class to Big Five subsystem and the corresponding computational stratum.
  2. [§2] Notation for the formalization of 'solution' (continuous function coded by a real, or via integral equation) should be fixed early and used consistently across sections.

Simulated Author's Rebuttal

2 responses · 0 unresolved

We thank the referee for the careful and constructive review. The major comments rightly emphasize the need for explicit formalizations to confirm that the ODE statements are natural and the equivalences non-circular. We agree these clarifications will strengthen the paper and address potential concerns about encoding artifacts. We respond to each point below and will incorporate the requested details in a revised manuscript.

read point-by-point responses

  1. Referee: [§5] §5 (discontinuous right-hand sides): the claimed equivalence of the existence statement for solutions to an ODE with discontinuous f to Π¹₁-CA0 must include an explicit formalization in the language of second-order arithmetic showing that the coding of the graph of f and the set of solutions does not presuppose a comprehension axiom; without this, the equivalence risks circularity as noted in the stress-test concern.

    Authors: We thank the referee for this observation. The existence statement for solutions with discontinuous f is formalized over RCA0 by representing the graph of f as a set G ⊆ ℝ×ℝ coded by a real (via standard pairing), with discontinuity expressed by a Π⁰₁ predicate on G that requires no comprehension beyond RCA0. The solution is a set Y coding the function y, and the proof establishes equivalence to Π¹₁-CA0 by showing that the existence of Y follows from (and implies) the comprehension axiom for Π¹₁ formulas, without using that axiom in the definition of G or Y. To eliminate any residual ambiguity and directly address the stress-test concern, we will add a new subsection in §5 that writes out the precise second-order formulas for the graph coding, the ODE predicate, and the solution set, confirming all are definable without presupposing Π¹₁ comprehension. revision: yes

  2. Referee: [§4] Proof of the ATR0-level equivalence (likely §4): the construction must verify that the ODE statement is not defined using arithmetical transfinite recursion in the representation of the solution or the modulus of continuity, to ensure the equivalence is non-circular and the statement remains natural.

    Authors: We appreciate this request for explicit verification. In the §4 construction, the modulus of continuity is obtained from the Lipschitz constant via a recursive definition using only Δ⁰₁ comprehension and basic arithmetic (available in RCA0), while the solution is represented as the limit of a sequence of Picard iterates defined by iterated integration; this sequence is arithmetical and does not invoke transfinite recursion. The equivalence then shows that the existence of such a solution set is equivalent to ATR0. We will revise the proof in §4 to include a dedicated paragraph that explicitly lists the second-order formulas for the modulus and solution representation, demonstrating that none of them employ ATR, thereby confirming the statement is natural and the equivalence non-circular. revision: yes

Circularity Check

0 steps flagged

No significant circularity; equivalences proven independently via reverse mathematics

full rationale

The paper proves direct equivalences in second-order arithmetic between natural statements about ODE initial-value problems (classified by regularity of f) and each level of the Big Five hierarchy. These are established as theorems over RCA0, WKL0, etc., rather than by defining the ODE statements in terms of the hierarchy or by fitting parameters that are then renamed as predictions. No self-definitional reductions, fitted-input predictions, or load-bearing self-citations appear in the derivation chain; the representation-invariant lens is obtained by explicit formalization of solution existence and computability, not by smuggling ansatzes or renaming known results. The central claims remain self-contained against external benchmarks of reverse mathematics.

Axiom & Free-Parameter Ledger

0 free parameters · 2 axioms · 0 invented entities

The central claim rests on the existence of natural ODE statements that exactly match each level of the reverse mathematics hierarchy. No free parameters are fitted. Axioms are standard from reverse mathematics and classical ODE theory. No new entities are introduced.

axioms (2)
  • standard math The Big Five subsystems of second-order arithmetic (RCA0, WKL0, ACA0, ATR0, Π¹₁-CA0)
    Invoked directly as the hierarchy whose levels are inhabited by ODE statements.
  • domain assumption Classical existence and uniqueness results for ODE initial value problems depend on the regularity class of the right-hand side f
    Used as the source of the natural statements placed at each hierarchy level.

pith-pipeline@v0.9.0 · 5603 in / 1512 out tokens · 68352 ms · 2026-05-11T02:37:53.701346+00:00 · methodology

discussion (0)

Sign in with ORCID, Apple, or X to comment. Anyone can read and Pith papers without signing in.

Lean theorems connected to this paper

Citations machine-checked in the Pith Canon. Every link opens the source theorem in the public Lean library.

Reference graph

Works this paper leans on

59 extracted references · 59 canonical work pages

  1. [1]

    The failure in computable analysis of a classical existence theorem for differential equations.Proceedings of the American Mathematical Society, 30:151–156, 1971

    Oliver Aberth. The failure in computable analysis of a classical existence theorem for differential equations.Proceedings of the American Mathematical Society, 30:151–156, 1971

    work page 1971

  2. [2]

    A new characteriza- tion of FAC0 via discrete ordinary differential equations

    Melissa Antonelli, Arnaud Durand, and Juha Kontinen. A new characteriza- tion of FAC0 via discrete ordinary differential equations. In Rastislav Kr´ alovic and Anton´ ın Kucera, editors,49th International Symposium on Mathemati- cal Foundations of Computer Science, MFCS 2024, Bratislava, Slovakia, Au- gust 26-30, 2024, volume 306 ofLIPIcs, pages 10:1–10:1...

    work page 2024

  3. [3]

    Characterizing small circuit classes from FAC 0 to FAC 1 via discrete ordinary differential equa- tions

    Melissa Antonelli, Arnaud Durand, and Juha Kontinen. Characterizing small circuit classes from FAC 0 to FAC 1 via discrete ordinary differential equa- tions. In Pawel Gawrychowski, Filip Mazowiecki, and Michal Skrzypczak, editors,50th International Symposium on Mathematical Foundations of Com- puter Science, MFCS 2025, Warsaw, Poland, August 25-29, 2025, ...

    work page 2025

  4. [4]

    Towards new charac- terizations of small circuit classes via discrete ordinary differential equations

    Melissa Antonelli, Arnaud Durand, and Juha Kontinen. Towards new charac- terizations of small circuit classes via discrete ordinary differential equations. Theor. Comput. Sci., 1062:115655, 2026

    work page 2026

  5. [5]

    PhD thesis, Ecole Polytechnique, 2025

    Manon Blanc.Discrete-Time and Continuous-Time Systems over the Reals: Relating Complexity with Robustness, Length and Precision. PhD thesis, Ecole Polytechnique, 2025. Phd Young Talent Award L’Or´ eal-Unesco 2025, and Prix STIC Doctorants du plateau de Saclay 2025

    work page 2025

  6. [6]

    The complexity of computing in continu- ous time: Space complexity is precision

    Manon Blanc and Olivier Bournez. The complexity of computing in continu- ous time: Space complexity is precision. In Karl Bringmann, Martin Grohe, Gabriele Puppis, and Ola Svensson, editors,51st International Colloquium on Automata, Languages, and Programming, ICALP 2024, Tallinn, Estonia, July 8-12, 2024, volume 297 ofLIPIcs, pages 129:1–129:22. Schloss ...

    work page 2024

  7. [7]

    published by the Authors, 2017

    Alin Bostan, Fr´ ed´ eric Chyzak, Marc Giusti, Romain Lebreton, Gr´ egoire Lecerf, Bruno Salvy, and ´Eric Schost.Algorithmes efficaces en calcul formel. published by the Authors, 2017

    work page 2017

  8. [8]

    Campagnolo

    Olivier Bournez and Manuel L. Campagnolo. A survey on continuous time computations. In S.B. Cooper, B. L¨ owe, and A. Sorbi, editors,New Com- putational Paradigms. Changing Conceptions of What is Computable, pages 383–423. Springer-Verlag, New York, 2008

    work page 2008

  9. [9]

    Polynomial differential equations compute all real computable functions on computable compact intervals.Journal of Complexity, 23(3):317– 335, June 2007

    Olivier Bournez, Manuel Lameiras Campagnolo, Daniel Silva Gra¸ ca, and Em- manuel Hainry. Polynomial differential equations compute all real computable functions on computable compact intervals.Journal of Complexity, 23(3):317– 335, June 2007

    work page 2007

  10. [10]

    A characterization of functions over the integers computable in polynomial time using discrete ordinary differential equations.Computational Complexity, 32(2):7, 2023

    Olivier Bournez and Arnaud Durand. A characterization of functions over the integers computable in polynomial time using discrete ordinary differential equations.Computational Complexity, 32(2):7, 2023. 18

    work page 2023

  11. [11]

    Solvable initial value problems ruled by discontinuous ordinary differential equations

    Olivier Bournez and Riccardo Gozzi. Solvable initial value problems ruled by discontinuous ordinary differential equations. Technical report, ´Ecole Poly- technique, France, 2024

    work page 2024

  12. [12]

    Solving discontinuous initial value prob- lems with unique solutions is equivalent to computing over the transfinite

    Olivier Bournez and Riccardo Gozzi. Solving discontinuous initial value prob- lems with unique solutions is equivalent to computing over the transfinite. In Symposium on Theoretical Aspects of Computer Science (STACS), Clermont- Ferrand, France, 2024

    work page 2024

  13. [13]

    On the complexity of solving initial value problems

    Olivier Bournez, Daniel Silva Gra¸ ca, and Amaury Pouly. On the complexity of solving initial value problems. In Joris van der Hoeven and Mark van Hoeij, editors,International Symposium on Symbolic and Algebraic Computation, ISSAC’12, Grenoble, France - July 22 - 25, 2012, pages 115–121. ACM, 2012

    work page 2012

  14. [14]

    Polynomial time corresponds to solutions of polynomial ordinary differential equations of poly- nomial length.Journal of the ACM, 64(6):38:1–38:76, 2017

    Olivier Bournez, Daniel Silva Gra¸ ca, and Amaury Pouly. Polynomial time corresponds to solutions of polynomial ordinary differential equations of poly- nomial length.Journal of the ACM, 64(6):38:1–38:76, 2017

    work page 2017

  15. [15]

    A survey on analog models of computa- tion

    Olivier Bournez and Amaury Pouly. A survey on analog models of computa- tion. In Vasco Brattka and Peter Hertling, editors,Handbook of Computability and Complexity in Analysis. Springer, 2021

    work page 2021

  16. [16]

    Weihrauch complexity in computable analysis

    Vasco Brattka, Guido Gherardi, and Arno Pauly. Weihrauch complexity in computable analysis. InHandbook of computability and complexity in analysis, pages 367–417. Springer, 2021

    work page 2021

  17. [17]

    A tutorial on com- putable analysis

    Vasco Brattka, Peter Hertling, and Klaus Weihrauch. A tutorial on com- putable analysis. InNew computational paradigms, pages 425–491. Springer, 2008

    work page 2008

  18. [18]

    Fast algorithms for manipulating formal power series.Journal of the ACM (JACM), 25(4):581–595, 1978

    Richard P Brent and Hsiang T Kung. Fast algorithms for manipulating formal power series.Journal of the ACM (JACM), 25(4):581–595, 1978

    work page 1978

  19. [19]

    Reverse mathematics of complexity lower bounds.Electron

    Lijie Chen, Jiatu Li, and Igor Carboni Oliveira. Reverse mathematics of complexity lower bounds.Electron. Colloquium Comput. Complex., TR24- 060, 2024

    work page 2024

  20. [20]

    The intrinsic computational difficulty of functions

    Alan Cobham. The intrinsic computational difficulty of functions. In Y. Bar- Hillel, editor,Proceedings of the International Conference on Logic, Method- ology, and Philosophy of Science, pages 24–30. North-Holland, Amsterdam, 1962

    work page 1962

  21. [21]

    Coddington and Norman Levinson.Theory of Ordinary Differentiel Equations

    Earl E. Coddington and Norman Levinson.Theory of Ordinary Differentiel Equations. McGraw-Hill, apr 1972

    work page 1972

  22. [22]

    Effective computability of solutions of ordinary differential equations the thousand monkeys approach

    Pieter Collins and Daniel Silva Gra¸ ca. Effective computability of solutions of ordinary differential equations the thousand monkeys approach. In Vasco Brattka, Ruth Dillhage, Tanja Grubba, and Angela Klutsch, editors,Proceed- ings of the Fifth International Conference on Computability and Complexity in Analysis, CCA 2008, Hagen, Germany, August 21-24, 2...

    work page 2008

  23. [23]

    Effective computability of solutions of differential inclusions the ten thousand monkeys approach.Journal of Uni- versal Computer Science, 15(6):1162–1185, 2009

    Pieter Collins and Daniel Silva Gra¸ ca. Effective computability of solutions of differential inclusions the ten thousand monkeys approach.Journal of Uni- versal Computer Science, 15(6):1162–1185, 2009

    work page 2009

  24. [24]

    Cambridge University Press Cambridge, 2010

    Stephen Cook and Phuong Nguyen.Logical foundations of proof complexity, volume 11. Cambridge University Press Cambridge, 2010

    work page 2010

  25. [25]

    Papadimitriou

    Constantinos Daskalakis and Christos H. Papadimitriou. Computing pure nash equilibria in graphical games via markov random fields. In Joan Feigen- baum, John C.-I. Chuang, and David M. Pennock, editors,Proceedings 7th ACM Conference on Electronic Commerce (EC-2006), Ann Arbor, Michigan, USA, June 11-15, 2006, pages 91–99, New York, NY, USA, 2006. ACM

    work page 2006

  26. [26]

    Some systems of second order arithmetic and their use

    Harvey M Friedman. Some systems of second order arithmetic and their use. InProc. of ICM, volume 1, pages 235–242. Canadian Math. Congress, 1975

    work page 1975

  27. [27]

    Systems on second order arithmetic with restricted in- duction i, ii.J

    Harvey M Friedman. Systems on second order arithmetic with restricted in- duction i, ii.J. Symb. Logic, 41:557–559, 1976

    work page 1976

  28. [28]

    PhD thesis, Instituto Superior T´ ecnico, Lisbon, Portugal and University of Algarve, Faro, Portugal, 2022

    Riccardo Gozzi.Analog Characterization of Complexity Classes. PhD thesis, Instituto Superior T´ ecnico, Lisbon, Portugal and University of Algarve, Faro, Portugal, 2022

    work page 2022

  29. [29]

    Set descriptive complexity of solvable functions.Computability, 2025

    Riccardo Gozzi and Olivier Bournez. Set descriptive complexity of solvable functions.Computability, 2025. Accepted for publication. To appear

    work page 2025

  30. [30]

    Gra¸ ca, N

    Daniel S. Gra¸ ca, N. Zhong, and J. Buescu. Computability, noncomputability and undecidability of maximal intervals of IVPs.Transactions of the American Mathematical Society, 361(6):2913–2927, 2009

    work page 2009

  31. [31]

    Gra¸ ca and Ning Zhong

    Daniel S. Gra¸ ca and Ning Zhong. Computability of differential equations. In Vasco Brattka and Peter Hertling, editors,Handbook of Computability and Complexity in Analysis. Springer., 2018

    work page 2018

  32. [32]

    Ro- bust simulations of turing machines with analytic maps and flows

    Daniel Silva Gra¸ ca, Manuel Lameiras Campagnolo, and Jorge Buescu. Ro- bust simulations of turing machines with analytic maps and flows. In S. Barry Cooper, Benedikt L¨ owe, and Leen Torenvliet, editors,New Computational Paradigms, First Conference on Computability in Europe, CiE 2005, Amster- dam, The Netherlands, June 8-12, 2005, Proceedings, volume 35...

    work page 2005

  33. [33]

    John Wiley and Sons, 1964

    Philip Hartman.Ordinary Differential Equations. John Wiley and Sons, 1964

    work page 1964

  34. [34]

    Graduate texts in computer science

    Neil Immerman.Descriptive complexity. Graduate texts in computer science. Springer, 1999

    work page 1999

  35. [35]

    Degrees of members ofπ10 classes.Pacific Journal of Mathematics, 40(3):605–616, 1972

    Carl Jockusch and Robert Soare. Degrees of members ofπ10 classes.Pacific Journal of Mathematics, 40(3):605–616, 1972

    work page 1972

  36. [36]

    Lipschitz continuous ordinary differential equations are polynomial-space complete

    Akitoshi Kawamura. Lipschitz continuous ordinary differential equations are polynomial-space complete. InProceedings of the 24th Annual IEEE Con- ference on Computational Complexity, CCC 2009, Paris, France, 15-18 July 2009, pages 149–160. IEEE, IEEE Computer Society, 2009. 20

    work page 2009

  37. [37]

    M¨ uller, Carsten R¨ osnick, and Martin Ziegler

    Akitoshi Kawamura, Norbert Th. M¨ uller, Carsten R¨ osnick, and Martin Ziegler. Computational benefit of smoothness: Parameterized bit-complexity of numerical operators on analytic functions and gevrey’s hierarchy.Journal of Complexity, 31(5):689–714, 2015

    work page 2015

  38. [38]

    Computational complexity of smooth differential equations.Log

    Akitoshi Kawamura, Hiroyuki Ota, Carsten R¨ osnick, and Martin Ziegler. Computational complexity of smooth differential equations.Log. Methods Comput. Sci., 10(1), 2014

    work page 2014

  39. [39]

    Parameterized com- plexity for uniform operators on multidimensional analytic functions and ODE solving

    Akitoshi Kawamura, Florian Steinberg, and Holger Thies. Parameterized com- plexity for uniform operators on multidimensional analytic functions and ODE solving. In Lawrence S. Moss, Ruy J. G. B. de Queiroz, and Maricarmen Mart´ ınez, editors,Logic, Language, Information, and Computation - 25th In- ternational Workshop, WoLLIC 2018, Bogota, Colombia, July ...

    work page 2018

  40. [40]

    Springer, Springer, 2018

    work page 2018

  41. [41]

    On the computational complexity of ordinary differential equations

    Ker-I Ko. On the computational complexity of ordinary differential equations. Information and Control, 58(1-3):157–194, jul/aug/sep 1983

    work page 1983

  42. [42]

    Birkh¨ auser, Boston, 1991

    Ker-I Ko.Complexity theory of real functions, volume 3 ofProgress in theo- retical computer science. Birkh¨ auser, Boston, 1991

    work page 1991

  43. [43]

    Cambridge University Press, 1995

    Jan Kraj´ ıcek.Bounded arithmetic, propositional logic, and complexity theory, volume 60 ofEncyclopedia of mathematics and its applications. Cambridge University Press, 1995

    work page 1995

  44. [44]

    Jiayi Liu.RT 2 2 does not implyW KL 0.J. Symb. Log., 77(2):609–620, 2012

    work page 2012

  45. [45]

    Recursive function theory and numerical analysis.J

    Webb Miller. Recursive function theory and numerical analysis.J. Comput. System Sci., 4(5):465–472, 1970

    work page 1970

  46. [46]

    Papadimitriou

    Christos H. Papadimitriou. On the complexity of the parity argument and other inefficient proofs of existence.Journal of Computer and System Sciences, 48(3):498–532, jun 1994

    work page 1994

  47. [47]

    PhD thesis, Ecole Polytechnique and Unidersidade Do Al- garve, Defended on July 6, 2015

    Amaury Pouly.Continuous models of computation: from computability to complexity. PhD thesis, Ecole Polytechnique and Unidersidade Do Al- garve, Defended on July 6, 2015. 2015. https://pastel.archives-ouvertes.fr/tel- 01223284, Prix de Th` ese de l’Ecole Polyechnique 2016, Ackermann Award 2017

    work page 2015

  48. [48]

    Computational complexity of solv- ing polynomial differential equations over unbounded domains.Theoretical Computer Science, 626:67–82, 2016

    Amaury Pouly and Daniel Silva Gra¸ ca. Computational complexity of solv- ing polynomial differential equations over unbounded domains.Theoretical Computer Science, 626:67–82, 2016

    work page 2016

  49. [49]

    M. B. Pour-El and J. I. Richards. A computable ordinary differential equation which possesses no computable solution.Ann. Math. Logic, 17:61–90, 1979

    work page 1979

  50. [50]

    Cambridge University Press, 2017

    Marian B Pour-El and J Ian Richards.Computability in analysis and physics, volume 1. Cambridge University Press, 2017

    work page 2017

  51. [51]

    Some undecidable problems involving elementary functions of a real variable.Journal of Symbolic Logic, 33(4):514–520, 1968

    Daniel Richardson. Some undecidable problems involving elementary functions of a real variable.Journal of Symbolic Logic, 33(4):514–520, 1968. 21

    work page 1968

  52. [52]

    An effective cauchy-peano existence theorem for unique so- lutions.International Journal of Foundations of Computer Science, 7(2):151– 160, 1996

    Keijo Ruohonen. An effective cauchy-peano existence theorem for unique so- lutions.International Journal of Foundations of Computer Science, 7(2):151– 160, 1996

    work page 1996

  53. [53]

    Decidability and complexity of event detection problems for odes.Complexity, 2(6):41–53, 1997

    Keijo Ruohonen. Decidability and complexity of event detection problems for odes.Complexity, 2(6):41–53, 1997

    work page 1997

  54. [54]

    David Seetapun and Theodore A. Slaman. On the strength of ramsey’s theo- rem.Notre Dame J. Formal Log., 36(4):570–582, 1995

    work page 1995

  55. [55]

    Stephen G. Simpson. Which set existence axioms are needed to prove the cauchy/peano theorem for ordinary differential equations?The Journal of Symbolic Logic, 49(3):783–802, 1984

    work page 1984

  56. [56]

    Cambridge University Press, 2009

    Stephen George Simpson.Subsystems of second order arithmetic, volume 1. Cambridge University Press, 2009

    work page 2009

  57. [57]

    Soare.Turing Computability: Theory and Applications

    Robert I. Soare.Turing Computability: Theory and Applications. Theory and Applications of Computability. Springer, Berlin, Heidelberg, 2016

    work page 2016

  58. [58]

    Moshe Y. Vardi. The complexity of relational query languages (extended ab- stract). In Harry R. Lewis, Barbara B. Simons, Walter A. Burkhard, and Lawrence H. Landweber, editors,Proceedings of the 14th Annual ACM Sym- posium on Theory of Computing, May 5-7, 1982, San Francisco, California, USA, pages 137–146. ACM, 1982

    work page 1982

  59. [59]

    Texts in Theoret- ical Computer Science

    Klaus Weihrauch.Computable Analysis - An Introduction. Texts in Theoret- ical Computer Science. An EATCS Series. Springer, 2000. 22

    work page 2000