The number of axioms

We derive results concerning the least possible number of distinct axioms in proofs in classical and intuitionistic sequent calculi and other related systems. In particular, we show that there is no recursive bound on the least possible number of distinct axioms in a proof of a provable sequent in terms of the sequent's length, and that there is no elementary bound on the least possible number of axioms in a cut-free proof of a provable sequent in terms of the least possible length of an arbitrary proof thereof, strengthening a classical result due to Orevkov and Statman. (c) 2022 Elsevier B.V. All rights reserved.