Abstract

We study the formalization within sybsystems of second-order arithmetic of theorems concerning periodic points in dynamical systems on the real line. We show that Sharkovsky's theorem is provable in WKL0. We show that, with an additional assumption, Sharkovsky's theorem is provable in RCA0. We show that the existence for all n of n-fold iterates of continuous mappings of the closed unit interval into itself is equivalent to the disjunction of Σ02 induction and weak König's lemma