Cut Elimination for Gentzen's Sequent Calculus with Equality and Logic of Partial Terms

摘要

We provide a natural formulation of the sequent calculus with equality and establish the cut elimination theorem. We also briefly outline and comment on its application to the logic of partial terms, when "existence" is formulated as equality with a (bound) variable.