Technical Reports

The ICICS/CS Reading Room

UBC CS TR-91-15 Summary

Formulations of an Extended NaDSet, August 1991 Paul C. Gilmore and George K. Tsiknis, 28 pages

NaDSet, a {\underline N}atural {\underline D}eduction based {\underline Set} theory and logic, of this paper is an extension of an earlier logic of the same name. It and some of its applications have been described in earlier papers. A proof of the consistency and completeness of NaDSet is provided elsewhere. In all these earlier papers NaDSet has been formulated as a Gentzen sequent calculus similar to the formulation LK by Gentzen of classical first order logic, although it was claimed that any natural deduction formalization of first order logic, such as Gentzen's natural deduction formulation NK, could be simply extended to be a formalization of NaDSet. This is indeed the case for the method of semantic tableaux of Beth or for Smullyan's version of the tableaux, but the extensions needed for other formalizations, including NK and the intuitionistic version NJ, require some care. The consistency of NaDSet is dependant upon restricting its axioms to those of the form ${\bf A} \rightarrow {\bf A}$, where {\bf A} is an atomic formula; an equivalent restriction for the natural deduction formulation is not obvious. The main purpose of this paper is to describe the needed restriction and to prove the equivalence of the resulting natural deduction logic with the Gentzen sequent calculus formulation for both the intuitionistic and the classical versions of NaDSet. Additionally the paper provides a brief sketch of the motivation for NaDSet and some of its proven and potential applications. \nThe authors gratefully acknowledges support from the Natural Science and Engineering Research Council of Canada.

If you have any questions or comments regarding this page please send mail to