In this paper we present the proof that there is no elementary translation from cut- free derivations in the sequent calculus variant of the epsilon calculus to LK-proofs with bounded cut-complexity. This is a partial answer to a question by Toshiyasu Arai. Fur- thermore, we show that the intuitionistic format of the sequent calculus variant of the epsilon calculus is not sound for intuitionistic logic, due to the presence of all classical quantifier-shift rules.
No takes yet. Share an insight, caveat, or question.
Baaz et al. (2024) studied this question.
Synapse has enriched 5 related papers. Consider them for comparative context: