TL;DR
This paper presents a terminating cut-elimination procedure for the logic calculus SBL, which corresponds to second-order arithmetic principles like Pi^{1}_{2}-Separation and Bar Induction.
Contribution
It introduces a novel cut-elimination method ensuring termination for SBL, linking proof theory with second-order arithmetic principles.
Findings
Successful cut-elimination procedure for SBL
Ensures termination in the calculus
Connects proof theory with second-order arithmetic
Abstract
In this paper we give a terminating cut-elimination procedure for a logic calculus SBL. SBL corresponds to the second order arithmetic Pi^{1}_{2}-Separation and Bar Induction.
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.