Cut-eliminability in second order logic calculi

2017/01/04 by Arai, Toshiyasu
#03F05 #FOS: Mathematics #Logic (math.LO)

paper · doi:10.48550/arxiv.1701.00929

Abstract

In this paper we propose a semantics in which the truth value of a formula is a pair of elements in a complete Boolean algebra. Through the semantics we can unify largely two proofs of cut-eliminability (Hauptsatz) in classical second order logic calculus, one is due to Takahashi-Prawitz and the other by Maehara.

Related

• The Cut Elimination and the Nonlengthening Property for the Sequent Calculus with Equality
• A Constructive Proof of Cut Elimination for a System of Full Second Order Logic
• A theory of cut-restriction: first steps
• First order logic properly displayed
• The higher dimensional propositional calculus