© 2004 by Oxford University Press
Axiomatization of a Denotational Semantics for First-order Logic
Philosophy Department, University of Auckland, Private Bag 92019, Auckland 1, New Zeland. * E-mail: k.vermeulen{at}auckland.ac.nz
An axiomatization is presented of the denotational semantics for first order language of Apt [1]. The goal is to obtain a rational reconstruction of the intuitions underlying this semantics. The axiomatization combines ideas about four valued logic with facts about substitutions. Soundness and completeness of the axiomatization are established. From the completeness proof a decision procedure is obtained that shows how four valued logic and order sensitivity of substitution together add up in a natural way to the denotational semantics for the language of first order logic as proposed by Apt.
Key Words: Declarative programming, denotational semantics, first order logic, axiomatization
Received 12 December 2003. Revised June 2004.
* The Philosophy Department much regrets the death of Kees Vermeulen, who died not long after correcting the proofs of this article.