Model Sets in a Nonconstructive Logic of Partial Terms with Definite Descriptions
The logic of partial terms (LPT) is a variety of negative free logic. In LPT, functions, as well as predicates, are strict, and free variables are given the generality interpretation. Both nonconstructive (classical) and intuitionist brands of negative free logic have served in foundational investigations, and Hilbert-style axiomatizations, natural deduction systems, and Gentzen-style sequents have been developed for them. This paper focuses on nonconstructive LPT with definite descriptions, called LPD, lays the foundation for tableaux systems by defining the concept of an LPD model system and establishing Hintikka’s Lemma, and summarizes the corresponding tableaux proof rules.