Cut Elimination for Negative Free Logics with Definite Descriptions

Abstract We present a sequent calculus GNFL for negative free logic with definite descriptions in the classical and intuitionistic versions, with empty and nonempty domains. It is shown constructively that GNFL satisfies the cut elimination theorem and its cut-free version satisfies the subformula property.