  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.
