# The ICICS/CS Reading Room

## UBC CS TR-90-22 Summary

- No on-line copy of this technical report is available.

- Logical Foundations for Programming Semantics, August 1990 Paul C. Gilmore and George K. Tsiknis
This paper was presented to the Sixth Workshop on Mathematical Foundations of Programming
Semantics held at Queen's University, May 15-19,1990.
\n\nThe paper provides an introduction to a natural deduction based set theory, NaDSet, and
illustrates its use in programming semantics. The need for such a set theory for the development
of programming semantics is motivated by contrasting the presentation of recursive definitions
within first order logic with their presentation within NaDSet. Within first order logic such
definitions are always incomplete in a very simple sense: Induction axioms must be added to the
given definitions and extended with every new recursive definition. Within a set theory such as
NaDSet, recursive definitions of sets are represented as terms in the theory and are complete in
the sense that all properties of the set can be derived from its definition. Such definitions not
only have this advantage of completeness, but they also permit recursively defined sets to be
members of the universe of discourse of the logic and thereby be shown to be members of other
defined sets.
\nThe resolution of the paradoxes provided by NaDSet is dependant upon replacing the naive
comprehension axiom scheme of an inconsistent first order logic with natural deduction rules for
the introduction of abstraction terms into arguments. The abstraction terms admitted are a
generalization of the abstraction terms usually admitted into set theory. In order to avoid a
confusion of use and mention, the nominalist interpretation of the atomic formulas of the logic
forces NaDSet to be second order, although only a single kind of quantifier and variable is
required.
\nThe use of NaDSet for programming semantics is illustrated for a simple flow diagram language
that has been used to illustrate the principles of denotational semantics. The presentation of the
semantics within NaDSet is not only fully formal, in contrast to the simply mathematical
presentation of denotational semantics, but because NaDSet is formalized as a natural deduction
logic, its derivations can be simply checked by machine.

If you have any questions or comments regarding this page please send mail to
help@cs.ubc.ca.