From a semantic point of view the logic of is like set theory in that it is a foundational theory of mathematics [Aczel 78,Barwise 75,Friedman 73,McCarty 84,Myhill 75]. We can try to explain the basic intuitions behind the theory to the point that the rules become self--evident; chapter 2 attempts this. We can also relate this theory to other foundational theories such as classical set theory. On the other hand it is just as meaningful and interesting to attempt to understand classical set theory in terms of type theory and to relate this theory to other apparently simpler ones such as constructive number theory (see [Beeson 83,Beeson 85]).
For computer scientists it is especially interesting to relate this theory to the theory of domains [Scott 76,Stoy 77] because both are attempts to give a mathematically rigorous account of computation. Thus, while it is not necessary to provide a ``denotational semantics'' for as the basis for reasoning about it, one might do so to compare approaches. It is also reasonable to use to give a constructive denotational semantics for programming languages; this topic is discussed briefly in chapter 11.