Ordinal notations and well-orderings in bounded arithmetic

This paper investigates provability and non-provability of well-foundedness of ordinal notations in weak theories of bounded arithmetic. We define a notion of well-foundedness on bounded domains. We show that T₂¹ and S₂² can prove the well-foundedness on bounded domains of the ordinal notations below ₀ and Γ₀. As a corollary, the class of polynomial local search problems, PLS, can be augmented with cost functions that take ordinal values below ₀ and Γ₀ without increasing the class PLS.