Logical Foundations for Programming Semantics

ID
TR-90-22
Authors
Paul C. Gilmore and George K. Tsiknis
Publishing date
August 1990
Abstract
This paper was presented to the Sixth Workshop on Mathematical Foundations of Programming Semantics held at Queen's University, May 15-19,1990. The 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. The 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. The 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.