Department of Computer Science
University of British Columbia
2366 Main Mall
Vancouver, B.C. Canada V6T 1Z4
e-mail: [email protected]

SOUNDNESS & CUT-ELIMINATION
for NaDSyL
by
Paul C Gilmore
Technical Report TR97-1
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.