Proof Mining and the Logical Strength of a Class of Implicit Fractional Boundary Value Problems

ABSTRACT The classical approach to establishing the existence of solutions for implicit fractional differential equations (FDEs) relies on non‐constructive fixed‐point theorems, notably Banach's contraction principle. This paper provides a foundational analysis of such an existence theorem from the perspectives of proof theory and reverse mathematics. We focus on a model problem involving an implicit FDE of order with ‐Caputo derivative and anti‐periodic boundary conditions. First, by applying methods of proof mining to the standard contraction mapping argument, we extract an explicit, computable rate of convergence for the associated Picard iteration. This yields a quantitative refinement of the classical existence proof and provides an a priori error estimate for numerical approximations. Second, we analyze the set‐existence axioms required for the proof within the framework of subsystems of second‐order arithmetic. We show that the existence theorem is provable in the system (Arithmetical Comprehension Axiom), establishing an upper bound on its logical strength. Furthermore, we provide a detailed analysis indicating that the theorem has logical strength at least that of , placing it within the level of the reverse mathematics hierarchy. Our work bridges fractional calculus and mathematical logic, providing both constructive insights for numerical analysis and a clear logical classification of a central result in the theory of FDEs.