arXiv:1606.01763 Abstract | arXiv Analytics

arXiv:1606.01763 [math.LO]Abstract References Reviews Resources

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

Published 2016-06-06Version 1

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.

Categories: math.LO, cs.LO

Subjects: 03F05, 03F07, F.4.1

Keywords: full second order logic, cut elimination, constructive proof, first order logic, cutrank growth

Related articles: Most relevant | Search more

arXiv:2105.06877 [math.LO] (Published 2021-05-14, updated 2021-05-19)

First order logic properly displayed

Samuel Balco, Giuseppe Greco, Alexander Kurz, Andrew Moshier, Alessandra Palmigiano, Apostolos Tzimoulis

arXiv:math/0210387 [math.LO] (Published 2002-10-24)

Consistency Without Cut Elimination

Kai Bruennler, Alessio Guglielmi

arXiv:1212.0108 [math.LO] (Published 2012-12-01)

An Ehrenfeucht-Fraïssé Game for $L_{ω_1ω}$