Cut-eliminability in second order logic calculi
classification
🧮 math.LO
keywords
cut-eliminabilitylogicordersecondsemanticsalgebrabooleancalculi
read the original 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.
This paper has not been read by Pith yet.
discussion (0)
Sign in with ORCID, Apple, or X to comment. Anyone can read and Pith papers without signing in.