Formulations of an Extended NaDSet

ID
TR-91-15
Authors
Paul C. Gilmore and George K. Tsiknis
Publishing date
August 1991
Length
28 pages
Abstract

NaDSet, a Natural Deduction based 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 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. The authors gratefully acknowledges support from the Natural Science and Engineering Research Council of Canada.