A sequent calculus for a negative free logic (Q622624)

By the term ``free logic'', K. Lambert characterized those logics which, roughly, do not necessarily enjoy existential presupposition. They are interesting not only philosophically but also in relation to a formal approach in computer science. In considering the validity of an expression containing a ``non-existing'' term, there are some different standpoints, among which that of ``negative free logic'' thinks it is always false. In this paper, the author provides a sequent calculus, called N, for a negative free logic with identity, and proves the admissibility of the cut-rule. In the latter half, soundness, compactness, and completeness of N are shown with respect to a standard semantics for negative free logic.