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

Preprint English OPEN
Skansi, Sandro;
  • Subject: Mathematics - Logic | Computer Science - Logic in Computer Science | 03F05, 03F07 | F.4.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 induct... View more
Share - Bookmark