Abstract#R##N##R##N#In this paper we show some non-elementary speed-ups in logic calculi: Both a predicative second-order logic and a logic for fixed points of positive formulas are shown to have non-elementary speed-ups over first-order logic. Also it is shown that eliminating second-order cut formulas in second-order logic has to increase sizes of proofs super-exponentially, and the same in eliminating second-order epsilon axioms. These are proved by relying on results due to P. Pudlak. (© 2008 WILEY-VCH Verlag GmbH & Co. KGaA, Weinheim)
['Toshiyasu Arai']
Non‐elementary speed‐ups in logic calculi