Cut-elimination for SBL
classification
🧮 math.LO
keywords
cut-eliminationarithmeticcalculuscorrespondsgiveinductionlogicorder
read the original 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.
This paper has not been read by Pith yet.
discussion (0)
Sign in with ORCID, Apple, or X to comment. Anyone can read and Pith papers without signing in.