Pierre Pradic (ENS de Lyon), The Logical Strength of Büchi's Decidability Theorem