Cut-eliminability in second order logic calculi

TL;DR

This paper introduces a semantics for second order logic where formulas are evaluated in a Boolean algebra, unifying two major proofs of cut-eliminability in classical second order logic calculus.

Contribution

It proposes a novel semantics that unifies two existing proofs of cut-eliminability in classical second order logic calculus.

Findings

Unified proof of cut-eliminability for second order logic

Semantics based on Boolean algebra for second order formulas

Simplifies understanding of cut-elimination in second order logic

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.