A Constructive Proof of Cut Elimination for a System of Full Second Order Logic

2016/06/06 by Sandro Skansi, Skansi, Sandro
Computer Science · Mathematics · #03F05 #03F07 #F.4.1 #FOS: Computer and information sciences #FOS: Mathematics #Formal Methods in Verification #Logic (math.LO) #Logic in Computer Science (cs.LO) #Logic, programming, and type systems #acm:03F05 #acm:03F07 #cs.LO #math.LO #msc:03F05 #msc:03F07 #semigroups and automata theory

paper · pdf · doi:10.48550/arxiv.1606.01763

This paper has been withdrawn by the author due to crucial errors noted by reviewers: no cut-elimination proof for second-order logic can be formalized in second-order arithmetic. The author's arguments are formalizable in a subsystem of Kalmar-elementary arithmetic. So the purported proof seems patently wrong

openalex publication_date 2016/06/06 · arxiv created 2016/06/21 · arxiv updated 2016/06/22 · openalex created_date 2016/06/24 · openalex updated_date 2026/07/28

Abstract

In this paper we present a constructive proof of cut elimination for a system of full second order logic with the structural rules absorbed and using sets instead of sequences. The standard problem of the cutrank growth is avoided by using a new parameter for the induction, the cutweight. This technique can also be applied to first order logic.

Related

• On the convergence of reduction-based and model-based methods in proof theory
• A theory of cut-restriction: first steps
• Cut-restriction: from cuts to analytic cuts
• Cut-eliminability in second order logic calculi
• Consistency Without Cut Elimination