
Department of Computer Science
University of British Columbia
2366 Main Mall
Vancouver, B.C. Canada V6T 1Z4
email: [email protected]
SOUNDNESS & CUTELIMINATION
for NaDSyL
by
Paul C Gilmore
Technical Report TR971
February 1997
ABSTRACT
NaDSyL, a Natural Deduction based Symbolic Logic, like some earlier logics, is
motivated by the belief that a confusion of use and mention is the source of the set
theoretic paradoxes. However NaDSyL differs from the earlier logics in several
important respects.
"Truth gaps", as they have been called by Kripke, are essential to the consistency of
the earlier logics, but are absent from NaDSyL; the law of the excluded middle is
derivable for all the sentences of NaDSyL. But the logic has an undecidable elementary
syntax, a departure from tradition that is of little importance, since the semantic tree
presentation of the proof theory can incorporate the decision process for the elementary
syntax.
The use of the lambda calculus notation in NaDSyL, rather than the set theoretic
notation of the earlier logics, reflects much more than a change of notation. For a second
motivation for NaDSyL is the provision of a higher order logic based on the original term
models of the lambda calculus rather than on the Scott models. These term models are
the "natural" intepretation of the lambda calculus for the naive nominalist view that
justifies the belief in the source of the paradoxes. They provide the semantics for the first
order domain of the second order logic NaDSyL.
The elementary and logical syntax or proof theory of NaDSyL is fully described, as well as its semantics. Semantic proofs of the soundness of NaDSyL with cut and of the completeness of NaDSyL without cut are given. That cut is a redundant rule follows form these results. Some applications of the logic are also described.