On the CONSISTENCY and COMPLETENESS of an EXTENDED NaDSet

ID
TR-91-17
Authors
Paul C. Gilmore
Publishing date
August 1991
Length
54 pages
Abstract

NaDSet in its extended form has been defined in several previous papers describing its applications. It is a Natural Deduction based Set theory and logic. In this paper the logic is shown to enjoy a form of $\omega$-consistency from which simple consistency follows. The proof uses transfinite induction over the ordinals up to $\varepsilon_0$, in the style of Gentzen's consistency proof for arithmetic. A completeness proof in the style of Henkin is also given. Finally the cut rule of deduction is shown to be redundant.