Solving Domain Equations in NaDSet

Solutions of systems of domain equations is the basis for what is called the Strachey-Scott approach to providing a denotational semantics for programming languages. The solutions offered by the mathematical methods developed by Scott, however, do not provide a computational basis for the semantics in the form of a proof theory. The purpose of this paper is to provide such a theory using the logic and set theory NaDSet. The development of NaDSet was motivated by the following three principles: 1. Abstraction, along with truth functions and quantification, is one of the three fundamental concepts of logic and should be formalized in the same manner as the other two. 2. Natural deduction presentations of logic provide a transparent formalization of Tarski's reductionist semantics. 3. Atomic formulas receive their truth values from a nominalist interpretation. That these three principles lead to a successful resolution of the set theoretic paradoxes and to a sound formulation of NaDSet has been demonstrated elsewhere with proofs of consistency and completeness. Applications of NaDSet to programming language semantics, category theory, non-well-founded sets, and to foundational questions of mathematics have also been demonstrated. The financial support of the Natural Science and Engineering Research Council of Canada is gratefully acknowledged.