# The ICICS/CS Reading Room

## UBC CS TR-91-15 Summary

- No on-line copy of this technical report is available.

- 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
help@cs.ubc.ca.