The Logic of Partial Terms LPT is a strict negative free logic that provides an economical framework for developing many traditional mathematical theories having partial functions. In these traditional theories, all functions and predicates are strict. For example, if a unary function (predicate) is applied to an undefined argument, the result is undefined (respectively, false). On the other hand, every practical programming language incorporates at least one nonstrict or lazy construct, such as the if-then-else, but nonstrict functions cannot be either (...) primitive or introduced in definitional extensions in LPT. Consequently, lazy programming language constructs do not fit the traditional mathematical mold inherent in LPT. A nonstrict (positive free) logic is required to handle nonstrict functions and predicates. Previously developed nonstrict logics are not fully satisfactory because they are verbose in describing strict functions (which predominate in many programming languages), and some logicians find their semantics philosophically unpalatable. The newly developed Lazy Logic of Partial Terms LL is as concise as LPT in describing strict functions and predicates, and strict and nonstrict functions and predicates can be introduced in definitional extensions of traditional mathematical theories. LL is "built on top of" LPT, and, like LPT, admits only one domain in the semantics. In the semantics, for the case of a nonstrict unary function h in an LL theory T, we have $\models_T h(\perp) = y \longleftrightarrow \forall x(h(x) = y)$ , where $\perp$ is a canonical undefined term. Correspondingly, in the axiomatization, the "indifference" (to the value of the argument) axiom $h(\perp) = y \longleftrightarrow \forall x(h(x) = y)$ guarantees a proper fit with the semantics. The price paid for LL's naturalness is that it is tailored for describing a specific area of computer science, program specification and verification, possibly limiting its role in explicating classical mathematical and philosophical subjects. (shrink)

Partial functions can be easily represented in set theory as certain sets of ordered pairs. However, classical set theory provides no special machinery for reasoning about partial functions. For instance, there is no direct way of handling the application of a function to an argument outside its domain as in partial logic. There is also no utilization of lambda-notation and sorts or types as in type theory. This paper introduces a version of von-Neumann-Bernays-Gödel set theory for reasoning about sets, proper (...) classes, and partial functions represented as classes of ordered pairs. The underlying logic of the system is a partial first-order logic, so class-valued terms may be nondenoting. Functions can be specified using lambda-notation, and reasoning about the application of functions to arguments is facilitated using sorts similar to those employed in the logic of the IMPS Interactive Mathematical Proof System. The set theory is intended to serve as a foundation for mechanized mathematics systems. (shrink)