A Denotational Semantics for First-Order Logic
Krzysztof R. Apt1,2

arXiv:cs/0005008v1 [] 8 May 2000

1

CWI, P.O. Box 94079, 1090 GB Amsterdam, the Netherlands
2
University of Amsterdam, the Netherlands
http://www.cwi.nl/˜apt

Abstract. In Apt and Bezem [AB99] we provided a computational interpretation of first-order formulas over arbitrary interpretations. Here
we complement this work by introducing a denotational semantics for
first-order logic. Additionally, by allowing an assignment of a non-ground
term to a variable we introduce in this framework logical variables.
The semantics combines a number of well-known ideas from the areas of
semantics of imperative programming languages and logic programming.
In the resulting computational view conjunction corresponds to sequential composition, disjunction to “don’t know” nondeterminism, existential quantification to declaration of a local variable, and negation to the
“negation as finite failure” rule. The soundness result shows correctness
of the semantics with respect to the notion of truth. The proof resembles
in some aspects the proof of the soundness of the SLDNF-resolution.

1

Introduction

Background
To explain properly the motivation for the work here discussed we need to go
back to the roots of logic programming and constraint logic programming. Logic
programming grew out of the seminal work of Robinson [Rob65] on the resolution method and the unification method. First, Kowalski and Kuehner [KK71]
introduced a limited form of resolution, called linear resolution. Then Kowalski
[Kow74] proposed what we now call SLD-resolution. The SLD-resolution is both
a restriction and an extension of the resolution method. Namely, the clauses are
restricted to Horn clauses. However, in the course of the resolution process a
substitution is generated that can be viewed as a result of a computation. Right
from the outset the SLD-resolution became then a crucial example of the computation as deduction paradigm according to which the computation process is
identified with a constructive proof of a formula (a query) from a set of axioms
(a program) with the computation process yielding the witness (a substitution).
This lineage of logic programming explains two of its relevant characteristics:
1. the queries and clause bodies are limited to the conjunctions of atoms,
2. the computation takes place (implicitly) over the domain of all ground terms
of a given first-order language.

The restriction in item 1. was gradually lifted and through the works of Clark
[Cla78] and Lloyd and Topor [LT84] one eventually arrived at the possibility of
using as queries and clause bodies arbitrary first-order formulas. This general
syntax is for example available in the language Gödel of Lloyd and Hill [HL94].
A way to overcome the restriction in item 2. was proposed in 1987 by Jaffar
and Lassez in their influential CLP(X) scheme that led to constraint logic programming. In this proposal the computation takes place over an arbitrary interpretation and the queries and clause bodies can contain constraints, i.e., atomic
formulas interpreted over the chosen interpretation. The unification mechanism
is replaced by a more general process of constraint solving and the outcome of
a computation is a sequence of constraints to which the original query reduces.
This powerful idea was embodied since then in many constraint logic programming languages, starting with the CLP(R) language of Jaffar, Michaylov,
Stuckey, and Yap [JMSY92] in which linear constraints over reals were allowed,
and the CHIP language of Dincbas et al. [DVS+ 88] in which linear constraints
over finite domains, combined with constraint propagation, were introduced. A
theoretical framework for CHIP was provided in van Hentenryck [Van89].
This transition from logic programming to constraint logic programming introduced a new element. In the CLP(X) scheme the test for satisfiability of a sequence of constraints was needed, while a proper account of the CHIP computing
process required an introduction of constraint propagation into the framework.
On some interpretations these procedures can be undecidable (the satisfiability
test) or computationally expensive (the “ideal” constraint propagation). This
explains why in the realized implementations some approximation of the former
or limited instances of the latter were chosen for.
So in both approaches the computation (i.e., the deduction) process needs
to be parametrized by external procedures that for each specific interpretation
have to be provided and implemented separately. In short, in both cases the
computation process, while parametrized by the considered interpretation, also
depends on the external procedures used. In conclusion: constraint logic programming did not provide a satisfactory answer to the question of how to lift
the computation process of logic programming from the domain of all ground
terms to an arbitrary interpretation without losing the property that this process
is effective.
Arbitrary interpretations are important since they represent a declarative
counterpart of data types. In practical situations the selected interpretations
would admit sorts that would correspond to the data types chosen by the user
for the application at hand, say terms, integers, reals and/or lists, each with the
usual operations available. It is useful to contrast this view with the one taken
in typed versions of logic programming languages. For example, in the case
of the Gödel language (polymorphic) types are provided and are modeled by
(polymorphic) sorts in the underlying theoretic model. However, in this model
the computation still implicitly takes place over one fixed domain, that of all
ground terms partitioned into sorts. This domain properly captures the builtin types but does not provide an account of user defined types. Moreover, in
2

this approach different (i.e., not uniform) interpretation of equality for different
types is needed, a feature present in the language but not accounted for in the
theoretical model.
Formulas as Programs
The above considerations motivated our work on a computational interpretation
of first-order formulas over arbitrary interpretations reported in Apt and Bezem
[AB99]. This allowed us to view first-order formulas as executable programs.
That is why we called this approach formulas as programs. In our approach the
computation process is a search of a satisfying valuation for the formula in question. Because the problem of finding such a valuation is in general undecidable,
we had to introduce the possibility of partial answers, modeled by an existence
of run-time errors.
This ability to compute over arbitrary interpretations allowed us to extend
the computation as deduction paradigm to arbitrary interpretations. We noted
already that the SLD-resolution is both a restriction and an extension of the resolution method. In turn, the formulas as programs approach is both a restriction
and an extension of the logic programming. Namely, the unification process is
limited to an extremely simple form of matching involving variables and ground
terms only. However, the computation process now takes place over an arbitrary
structure and full-first order syntax is adopted.
The formulas as programs approach to programming has been realized in the
programming language Alma-0 [ABPS98] that extends imperative programming
by features that support declarative programming. In fact, the work reported in
Apt and Bezem [AB99] provided logical underpinnings for a fragment of Alma-0
that does not include destructive assignment or recursive procedures and allowed
us to reason about non-trivial programs written in this fragment.
Rationale for This Paper
The computational interpretation provided in Apt and Bezem [AB99] can be
viewed as an operational semantics of first-order logic. The history of semantics of
programming languages has taught us that to better understand the underlying
principles it is beneficial to abstract from the details of the operational semantics.
This view was put forward by Scott and Strachey [SS71] in their proposal of
denotational semantics of programming languages according to which, given a
programming language, the meaning of each program is a mathematical function
of the meanings of its direct constituents.
The aim of this paper is to complement the work of [AB99] by providing a
denotational semantics of first-order formulas. This semantics combines a number of ideas realized in the areas of (nondeterministic) imperative programming
languages and the field of logic programming. It formalizes a view according to
which conjunction can be seen as sequential composition, disjunction as “don’t
know” nondeterminism, existential quantification as declaration of a local variable, and it relates negation to the “negation as finite failure” rule.
3

The main result is that the denotational semantics is sound with respect
to the truth definition. The proof is reminiscent in some aspects of the proof
of the soundness of the SLDNF-resolution of Clarke [Cla78]. The semantics of
equations allows matching involving variables and non-ground terms, a feature
not present in [AB99] and in Alma-0. This facility introduces logical variables in
this framework but also creates a number of difficulties in the soundness proof
because bindings to local variables can now be created.
First-order logic is obviously a too limited formalism for programming. In
[AB99] we discussed a number of extensions that are convenient for programming purposes, to wit sorts (i.e., types), arrays, bounded quantification and
non-recursive procedures. This leads to a very expressive and easy to program
in subset of Alma-0. We do not envisage any problems in incorporating these
features into the denotational semantics here provided. A major problem is how
to deal with recursion.
The plan of the paper is as follows. In the next section we discuss the difficulties encountered when solving arbitrary equations over algebras. Then, in
Section 3 we provide a semantics of equations and in Section 4 we extend it to
the case of first-order formulas interpreted over an arbitrary interpretation. The
resulting semantics is denotational in style. In Section 5 we relate this semantics
to the notion of truth by establishing a soundness result. In Section 6 we draw
conclusions and suggest some directions for future work.

2

Solving Equations over Algebras

Consider some fixed, but arbitrary, language of terms L and a fixed, but arbitrary
algebra J for it (sometimes called a pre-interpretation). A typical example is the
language defining arithmetic expressions and its standard interpretation over the
domain of integers.
We are interested in solving equations of the form s = t over an algebra, that
is, we seek an instantiation of the variables occurring in s and t that makes this
equation true when interpreted over J . By varying L and J we obtain a whole
array of specific decision problems that sometimes can be solved efficiently, like
the unification problem or the problem of solving linear equations over reals, and
sometimes are undecidable, like the problem of solving Diophantine equations.
Our intention is to use equations as a means to assign values to variables.
Consequently, we wish to find a natural, general, situation for which the problem
of determining whether an equation s = t has a solution in a given algebra is
decidable, and to exhibit a “most general solution”, if one exists. By using most
general solutions we do not lose any specific solution.
This problem cannot be properly dealt with in full generality. Take for example the polynomial equations over integers. Then the equation x2 − 3x + 2 = 0
has two solutions, {x/1} and {x/2}, and none is “more general” than the other
under any reasonable definition of a solution being more general than another.
In fact, given an arbitrary interpretation, the only case that seems to be of
any use is that of comparing a variable and an arbitrary term. This brings us to
4

equations of the form x = t, where x does not occur in t. Such an equation has
obviously a most general solution, namely the instantiation {x/t}.
A dual problem is that of finding when an equation s = t has no solution in
a given algebra. Of course, non-unifiability is not a rescue here: just consider the
already mentioned equation x2 − 3x + 2 = 0 the sides of which do not unify.
Again, the only realistic situation seems to be when both terms are ground
and their values in the considered algebra are different. This brings us to equations s = t both sides of which are ground terms.

3

Semantics of Equations

After these preliminary considerations we introduce specific “hybrid” objects in
which we mix the syntax and semantics.
Definition 1. Consider a language of terms L and an algebra J for it. Given
a function symbol f we denote by fJ the interpretation of f in J .
– Consider a term of L in which we replace some of the variables by the elements of the domain D. We call the resulting object a generalized term.
– Given a generalized term t we define its J -evaluation as follows:
• replace each constant occuring in t by its value in J ,
• repeatedly replace each sub-object of the form f (d1 , . . ., dn ) where f is a
function symbol and d1 , . . ., dn are the elements of the domain D by the
element fJ (d1 , . . ., dn ) of D.
We call the resulting generalized term a J -term and denote it by [[t]]J . Note
that if t is ground, then [[t]]J is an element of the domain of J .
– By a J -substitution we mean a finite mapping from variables to J -terms
which assigns to each variable x in its domain a J -term different from x.
We write it as {x1 /h1 , . . . , xn /hn }.
✷
The J -substitutions generalize both the usual substitutions and the valuations, which assign domain values to variables. By adding to the language L
constants for each domain element and for each ground term we can reduce the
J -substitutions to the substitutions. We preferred not to do this to keep the
notation simple.
In what follows we denote the empty J -substitution by ε and arbitrary J substitutions by θ, η, γ with possible subscripts.
A more intuitive way of introducing J -terms is as follows. Each ground term
of s of L evaluates to a unique value in J . Given a generalized term t replace
each maximal ground subterm of t by its value in J . The outcome is the J -term
[[t]]J .
We define the notion of an application of a J -substitution θ to a generalized
term t in the standard way and denote it by tθ. If t is a term, then tθ does not
have to be a term, though it is a generalized term.

5

Definition 2.
– A composition of two J -substitutions θ and η, written as θη, is defined as
the unique J -substitution γ such that for each variable x
xγ = [[(xθ)η]]J .
✷
Let us illustrate the introduced concepts by means of two examples.
Example 1. Take an arbitrary language of terms L. The Herbrand algebra Her
for L is defined as follows:
– its domain is the set HU L of all ground terms of L (usually called the
Herbrand universe),
– if f is an n-ary function symbol in L, then its interpretation is the mapping
from (HU L )n to HU L which maps the sequence t1 , . . . , tn of ground terms
to the ground term f (t1 , . . . , tn ).
Consider now a term s. Then [[s]]Her equals s because in Her every ground
term evaluates to itself. So the notions of a term, a generalized term and a Herterm coincide. Consequently, the notions of substitutions and Her-substitutions
coincide.
✷
Example 2. Take as the language of terms the language AE of arithmetic expressions. Its binary function symbols are the usual · (“times”), + (“plus”) and
− (“minus”), and its unique binary symbol is − (“unary minus”). Further, for
each integer k there is a constant k.
As the algebra for AE we choose the standard algebra Int that consists of
the set of integers with the function symbols interpreted in the standard way. In
what follows we write the binary function symbols in the usual infix notation.
Consider the term s ≡ x + (((3 + 2) · 4) − y). Then [[s]]AE equals x + (20 − y).
Further, given the AE-substitution θ := {x/6 − z, y/3} we have sθ ≡ (6 −
z) + (((3 + 2) · 4) − 3) and consequently, [[sθ]]AE = (6 − z) + 17. Further, given
η := {z/4}, we have θη = {x/2, y/3, z/4}.
✷
To define the meaning of an equation over an algebra J we view J -substitutions as states and use a special state
– error, to indicate that it is not possible to determine effectively whether a
solution to the equation sθ = tθ in J exists.
We now define the semantics [[·]] of an equation between two generalized terms
as follows:

{θ{sθ/[[tθ]]J }} if sθ is a variable that does not occur in tθ,




{θ{tθ/[[sθ]]J }} if tθ is a variable that does not occur in sθ



and sθ is not a variable,
[[s = t]](θ) :=
if [[sθ]]J and [[tθ]]J are identical,
 {θ}



if sθ and tθ are ground and [[sθ]]J 6= [[tθ]]J ,
∅


{error}
otherwise.
6

It will become clear in the next section why we collect here the unique outcome into a set and why we “carry” θ in the answers.
Note that according to the above definition we have [[s = t]](θ) = {error}
for the non-ground generalized terms sθ and tθ such that the J -terms [[sθ]]J
and [[tθ]]J are different. In some situations we could safely assert then that
[[s = t]](θ) = {θ} or that [[s = t]](θ) = ∅. For example, for the standard algebra Int for the language of arithmetic expressions we could safely assert that
[[x + x = 2 · x]](θ) = {θ} and [[x + 1 = x]](θ) = ∅ for any AE-substitution θ.
The reason we did not do this was that we wanted to ensure that the semantics is uniform and decidable so that it can be implemented.

4

A Denotational Semantics for First-Order Logic

Consider now a first-order language with equality L. In this section we extend
the semantics [[·]] to arbitrary first-order formulas from L interpreted over an
arbitrary interpretation. [[·]] depends on the considered interpretation but to
keep the notation simple we do not indicate this dependence. This semantics
is denotational in the sense that meaning of each formula is a mathematical
function of the meanings of its direct constituents.
Fix an interpretation I. I is based on some algebra J . We define the notion
of an application of a J -substitution θ to a formula φ of L, written as φθ, in the
usual way.
Consider an atomic formula p(t1 , . . ., tn ) and a J -substitution θ. We denote
by pI the interpretation of p in I.
We say that
– p(t1 , . . ., tn )θ is true if p(t1 , . . ., tn )θ is ground and ([[t1 θ]]J , . . ., [[tn θ]]J ) ∈ pI ,
– p(t1 , . . ., tn )θ is false if p(t1 , . . ., tn )θ is ground and ([[t1 θ]]J , . . ., [[tn θ]]J ) 6∈ pI .
In what follows we denote by Subs the set of J -substitutions and by P(A),
for a set A, the set of all subsets of A.
For a given formula φ its semantics [[φ]] is a mapping
[[φ]] : Subs → P(Subs ∪ {error}).
The fact that the outcome of [[φ]](θ) is a set reflects the possibility of a
nondeterminism here modeled by the disjunction.
To simplify the definition we extend [[·]] to deal with subsets of Subs∪{error}
by putting
[[φ]](error) := {error},
and for a set X ⊆ Subs ∪ {error}
[

[[φ]](X) :=

e∈X

7

[[φ]](e).

Further, to deal with the existential quantifier, we introduce an operation
DROPx , where x is a variable. First we define DROPx on the elements of Subs∪
{error} by putting for a J -substitution θ

θ if x is not in the domain of θ,
DROPx (θ) :=
η if θ is of the form η ⊎ {x/s},
and
DROPx (error) := error.
Then we extend it element-wise to subsets of Subs ∪ {error}, that is, by
putting for a set X ⊆ Subs ∪ {error}
DROPx (X) := {DROPx (e) | e ∈ X}.
[[·]] is defined by structural induction as follows, where A is an atomic formula
different from s = t:

if Aθ is true,
 {θ}
if Aθ is false,
– [[A]](θ) := ∅

{error} otherwise, that is if Aθ is not ground,
– [[φ1 ∧ φ2 ]](θ) := [[φ2 ]]([[φ1 ]](θ)),
– [[φ1 ∨ φ2 ]](θ)
:= [[φ1 ]](θ) ∪ [[φ2 ]](θ),
if [[φ]](θ) = ∅,
 {θ}
if θ ∈ [[φ]](θ),
– [[¬φ]](θ) := ∅

{error} otherwise,
– [[∃x φ]](θ) := DROPy ([[φ{x/y}]](θ)), where y is a fresh variable.
To better understand this definition let us consider some simple examples
that refer to the algebras discussed in Examples 1 and 2.
Example 3. Take an interpretation I based on the Herbrand algebra Her. Then
[[f (x) = z ∧ g(z) = g(f (x))]]({x/g(y)}) = [[g(z) = g(f (x))]](θ) = {θ},
where θ := {x/g(y), z/f (g(y))}. On the other hand
[[g(f (x)) = g(z)]]({x/g(y)}) = {error}.
✷
Example 4. Take an interpretation I based on the standard algebra AE for the
language of arithmetic expressions. Then
[[y = z − 1 ∧ z = x + 2]]({x/1}) = [[z = x + 2]]({x/1, y/z − 1}) = {x/1, y/2, z/3}.
Further,
[[y + 1 = z − 1]]({y/1, z/3}) = {y/1, z/3}
8

and even
[[x · (y + 1) = (v + 1) · (z − 1)]]({x/v + 1, y/1, z/3}) = {x/v + 1, y/1, z/3}.
On the other hand
[[y − 1 = z − 1]](ε) = {error}.
✷
The first example shows that the semantics given here is weaker than the
one provided by the logic programming. In turn, the second example shows that
our treatment of arithmetic expressions is more general than the one provided
by Prolog.
This definition of denotational semantics of first-order formulas combines a
number of ideas put forward in the area of semantics of imperative programming
languages and the field of logic programming.
First, for an atomic formula A, when Aθ is ground, its meaning coincides with
the meaning of a Boolean expression given in de Bakker [dB80, page 270]. In
turn, the meaning of the conjunction and of the disjunction follows [dB80, page
270] in the sense that the conjunction corresponds to the sequential composition
operation “;” and the disjunction corresponds to the “don’t know” nondeterministic choice, denoted there by ∪.
Next, the meaning of the negation is inspired by its treatment in logic programming. To be more precise we need the following observations the proofs of
which easily follow by structural induction.
Note 1.
(i) If η ∈ [[φ]](θ), then η = θγ for some J -substitution γ.
(ii) If φθ is ground, then [[φ]](θ) ⊆ {θ}.

✷

First, we interpret [[φ]](θ) ∩ Subs 6= ∅ as the statement “the query φθ succeeds”. More specifically, if η ∈ [[φ]](θ), then by Note 1(i) for some γ we have
η = θγ.
In general, γ is of course not unique: take for example θ := {x/0} and η = θ.
Then both η = θε and η = θθ. However, it is easy to show that if η is less general
than θ, then in the set {γ | η = θγ} the J -substitution with the smallest domain
is uniquely defined. In what follows given J -substitutions η and θ such that η is
less general than θ, when writing η = θγ we always refer to this uniquely defined
γ.
Now we interpret θγ ∈ [[φ]](θ) as the statement “γ is the computed answer
substitution for the query φθ”. In turn, we interpret [[φ]](θ) = ∅ as the statement
“the query φθ finitely fails”.
Suppose now that [[φ]](θ)∩Subs 6= ∅, which means that the query φθ succeeds.
Assume additionally that φθ is ground. Then by Note 1(ii) θ ∈ [[φ]](θ) and
consequently by the definition of the meaning of negation [[¬φ]](θ) = ∅, which
means that the query ¬φθ finitely fails.
9

In turn, suppose that [[φ]](θ) = ∅, which means that the query φθ finitely
fails. By the definition of the meaning of negation [[¬φ]](θ) = {θ}, which means
that the query ¬φθ succeeds with the empty computed answer substitution.
This explains the relation with the “negation as finite failure” rule according
to which for a ground query Q:
– if Q succeeds, then ¬Q finitely fails,
– if Q finitely fails, then ¬Q succeeds with the empty computed answer substitution.
In fact, our definition of the meaning of negation corresponds to a generalization of the negation as finite failure rule already mentioned in Clark [Cla78],
according to which the requirement that Q is ground is dropped and the first
item is replaced by:
– if Q succeeds with the empty computed answer substitution, then ¬Q finitely
fails.
Finally, the meaning of the existential quantification corresponds to the
meaning of the block statement in imperative languages, see, e.g., de Bakker
[dB80, page 226], with the important difference that the local variable is not
initialized. From this viewpoint the existential quantifier ∃x corresponds to the
declaration of the local variable x. The DROPx operation was introduced in
Clarke [Cla79] to deal with the declarations of local variables.
We do not want to make the meaning of the formula ∃x φ dependent on
the choice of y. Therefore we postulate that for any fresh variable y the set
DROPy ([[φ{x/y}]](θ)) is a meaning of ∃x φ given a J -substitution θ. Consequently, the semantics of ∃x φ has many outcomes, one for each choice of y.
This “multiplicity” of meanings then extends to all formulas containing the existential quantifier. So for example for any variable y different from x and z
the J -substitution {z/f (y)} is the meaning of ∃x (z = f (x)) given the empty
J -substitution ε.

5

Soundness

To relate the introduced semantics to the notion of truth we first formalize the
latter using the notion of a J -substitution instead of the customary notion of a
valuation.
Consider a first-order language L with equality and an interpretation I for
it based on some algebra J . Let θ be a J -substitution. We define the relation
I |=θ φ for a formula φ by structural induction. First we assume that θ is defined
on all free variables of φ and put
– I |=θ s = t iff [[sθ]]J and [[tθ]]J coincide,
– I |=θ p(t1 , . . ., tn ) iff p(t1 , . . ., tn )θ is ground and ([[t1 θ]]J , . . ., [[tn θ]]J ) ∈ pI .
10

In other words, I |=θ p(t1 , . . ., tn ) iff p(t1 , . . ., tn )θ is true. The definition extends
to non-atomic formulas in the standard way.
Now assume that θ is not defined on all free variables of φ. We put
– I |=θ φ iff I |=θ ∀x1 , . . ., ∀xn φ where x1 , . . ., xn is the list of the free variables
of φ that do not occur in the domain of θ.
Finally,
– I |= φ iff I |=θ φ for all J -substitutions θ.
To prove the main theorem we need the following notation. Given a J substitution η := {x1 /h1 , . . . , xn /hn } we define hηi := x1 = h1 ∧ . . . ∧ xn =
hn .
In the discussion that follows the following simple observation will be useful.
Note 2. For all J -substitutions θ and formulas φ
I |=θ φ iff I |= hθi → φ.
✷
The following theorem now shows correctness of the introduced semantics
with respect to the notion of truth.
Theorem 1 (Soundness).
Consider a first-order language L with equality and an interpretation I for
it based on some algebra J . Let φ be a formula of L and θ a J -substitution.
(i) For each J -substitution η ∈ [[φ]](θ)
I |=η φ.
(ii) If error 6∈ [[φ]](θ), then
I |= φθ ↔

k
_

∃yi hηi i,

i=1

where [[φ]](θ) = {θη1 , . . ., θηk }, and for i ∈ [1..k] yi is a sequence of variables
that appear in the range of ηi .
Note that by (ii) if [[φ]](θ) = ∅, then
I |=θ ¬φ.
In particular, if [[φ]](ε) = ∅, then
I |= ¬φ.
11

Proof. The proof proceeds by simultaneous induction on the structure of the
formulas.
φ is s = t.
If η ∈ [[φ]](θ), then three possibilities arise.
1. sθ is a variable that does not occur in tθ.
Then [[s = t]](θ) = {θ{sθ/[[tθ]]J }} and consequently η = θ{sθ/[[tθ]]J }. So
I |=η (s = t) holds since sη = [[tθ]]J and tη = tθ.
2. tθ is a variable that does not occur in sθ and sθ is not a variable.
Then [[s = t]](θ) = {θ{tθ/[[sθ]]J }}. This case is symmetric to 1.
3. [[sθ]]J and [[tθ]]J are identical.
Then η = θ, so I |=η (s = t) holds.
If error 6∈ [[φ]](θ), then four possibilities arise.
1. sθ is a variable that does not occur in tθ.
Then [[s = t]](θ) = {θ{sθ/[[tθ]]J }}. We have I |= (s = t)θ ↔ sθ = [[tθ]]J .
2. tθ is a variable that does not occur in sθ and sθ is not a variable.
Then [[s = t]](θ) = {θ{tθ/[[sθ]]J }}. This case is symmetric to 1.
3. [[sθ]]J and [[tθ]]J are identical.
Then [[s = t]](θ) = {θ}. We have [[s = t]](θ) = {θε} and I |=θ s = t, so
I |= (s = t)θ ↔ hεi, since hεi is vacuously true.
4. sθ and tθ are ground J -terms and [[sθ]]J 6= [[tθ]]J .
Then [[s = t]](θ) = ∅ and I |=θ ¬(s = t), so I |= (s = t)θ ↔ f alsum, where
f alsum denotes the empty disjunction.
φ is an atomic formula different from s = t.
If η ∈ [[φ]](θ), then η = θ and φθ is true. So I |=θ φ, i.e., I |=η φ.
If error 6∈ [[φ]](θ), then either [[φ]](θ) = {θ} or [[φ]](θ) = ∅. In both cases the
argument is the same as in case 3. and 4. for the equality s = t.
Note that in both cases we established a stronger form of (ii) in which each
list yi is empty, i.e., no quantification over the variables in yi appears.
φ is φ1 ∧ φ2 . This is the most elaborate case.
If η ∈ [[φ]](θ), then for some J -substitution γ both γ ∈ [[φ1 ]](θ) and η ∈
[[φ2 ]](γ). By induction hypothesis both I |=γ φ1 and I |=η φ2 . But by Note 1(i)
η is less general than γ, so I |=η φ1 and consequently I |=η φ1 ∧ φ2 .
If error 6∈ [[φ]](θ), then for some X ⊆ Subs both [[φ1 ]](θ) = X and error 6∈
[[φ2 ]](η) for all η ∈ X.
By induction hypothesis
I |= φ1 θ ↔

k
_

i=1

12

∃yi hηi i,

where X = {θη1 , . . ., θηk } and for i ∈ [1..k] yi is a sequence of variables that
appear in the range of ηi . Hence
I |= (φ1 ∧ φ2 )θ ↔

k
_

(∃yi hηi i ∧ φ2 θ),

i=1

so by appropriate renaming of the variables in the sequences yi
k
_

I |= (φ1 ∧ φ2 )θ ↔

∃yi (hηi i ∧ φ2 θ).

i=1

But for any J -substitution δ and a formula ψ
I |= hδi ∧ ψ ↔ hδi ∧ ψδ,
so
I |= (φ1 ∧ φ2 )θ ↔ (

k
_

∃yi (hηi i ∧ φ2 θηi ).

(1)

i=1

Further, we have for i ∈ [1..k]
[[φ2 ]](θηi ) = {θηi γi,j | j ∈ [1..ℓi ]}
for some J -substitutions γi,1 , . . ., γi,ℓi . So
[[φ1 ∧ φ2 ]](θ) = {θηi γi,j | i ∈ [1..k], j ∈ [1..ℓi ]}.
By induction hypothesis we have for i ∈ [1..k]
I |= φ2 θηi ↔

ℓi
_

∃vi,j hγi,j i,

j=1

where for i ∈ [1..k] and j ∈ [1..ℓi ] vi,j is a sequence of variables that appear in
the range of γi,j .
Using (1) by appropriate renaming of the variables in the sequences vi,j we
now conclude that
I |= (φ1 ∧ φ2 )θ ↔

ℓi
k _
_

∃yi ∃vi,j (hηi i ∧ hγi,j i),

i=1 j=1

so
I |= (φ1 ∧ φ2 )θ ↔

ℓi
k _
_

∃yi ∃vi,j hηi γi,j i,

i=1 j=1

since the domains of ηi and γi,j are disjoint and for any J -substitutions γ and
δ with disjoint domains we have
I |= hγi ∧ hδi ↔ hγδi.
13

φ is φ1 ∨ φ2 .
If η ∈ [[φ]](θ), then either η ∈ [[φ1 ]](θ) or η ∈ [[φ2 ]](θ), so by induction hypothesis either I |=η φ1 or I |=η φ2 . In both cases I |=η φ1 ∨ φ2 holds.
If error 6∈ [[φ]](θ), then for some J -substitutions η1 , . . ., ηk
[[φ1 ]](θ) = {θη1 , . . ., θηk },
where k ≥ 0, for some J -substitutions ηk+1 , . . ., ηk+ℓ ,
[[φ2 ]](θ) = {θηk+1 , . . ., θηk+ℓ },
where ℓ ≥ 0, and
[[φ1 ∨ φ2 ]](θ) = {θη1 , . . ., θηk+ℓ }.
By induction hypothesis both
I |= φ1 θ ↔

k
_

∃yi hηi i

i=1

and
I |= φ2 θ ↔

k+ℓ
_

∃yi hηi i

i=k+1

for appropriate sequences of variables yi . So
I |= (φ1 ∨ φ2 )θ ↔

k+ℓ
_

∃yi hηi i.

i=1

φ is ¬φ1 .
If η ∈ [[φ]](θ), then η = θ and [[φ1 ]](θ) = ∅. By induction hypothesis I |=θ ¬φ1 ,
i.e., I |=η ¬φ1 .
If error 6∈ [[φ]](θ), then either [[φ]](θ) = {θ} or [[φ]](θ) = ∅. In the former
case [[φ]](θ) = {θε}, so [[φ1 ]](θ) = ∅. By induction hypothesis I |=θ ¬φ1 , i.e.,
I |= (¬φ1 )θ ↔ hεi, since hεi is vacuously true. In the latter case θ ∈ [[φ1 ]](θ), so
by induction hypothesis I |=θ φ1 , i.e., I |= (¬φ1 )θ ↔ f alsum.
φ is ∃x φ1 .
If η ∈ [[φ]](θ), then η ∈ DROPy ([[φ1 {x/y}]](θ)) for some fresh variable y. So
either (if y is not in the domain of η) η ∈ [[φ1 {x/y}]](θ) or for some J -term
s we have η ⊎ {y/s} ∈ [[φ1 {x/y}]](θ). By induction hypothesis in the former
case I |=η φ1 {x/y} and in the latter case I |=η⊎{y/s} φ1 {x/y}. In both cases
I |= ∃y (φ1 {x/y}η), so, since y is fresh, I |= (∃y φ1 {x/y})η and consequently
I |= (∃x φ1 )η, i.e., I |=η ∃x φ1 .
If error 6∈ [[φ]](θ), then error 6∈ [[φ1 {x/y}]](θ), as well, where y is a fresh
variable. By induction hypothesis
I |= φ1 {x/y}θ ↔

k
_

i=1

14

∃yi hηi i,

(2)

where
[[φ1 {x/y}]](θ) = {θη1 , . . ., θηk }

(3)

and for i ∈ [1..k] yi is a sequence of variables that appear in the range of ηi .
Since y is fresh, we have I |= ∃y (φ1 {x/y}θ) ↔ (∃y φ1 {x/y})θ and I |=
(∃y φ1 {x/y})θ ↔ (∃x φ1 )θ. So (2) implies
I |= (∃x φ1 )θ ↔

k
_

∃y∃yi hηi i.

i=1

But for i ∈ [1..k]
I |= ∃yhηi i ↔ ∃yhDROPy (ηi )i,
since if y/s ∈ ηi , then the variable y does not appear in s. So
I |= (∃x φ1 )θ ↔

k
_

∃yi ∃yhDROPy (ηi )i.

(4)

i=1

Now, by (3)
[[∃x φ1 ]](θ) = {DROPy (θη1 ), . . ., DROPy (θηk )}.
But y does not occur in θ, so we have for i ∈ [1..k]
DROPy (θηi ) = θDROPy (ηi )
and consequently
[[∃x φ1 ]](θ) = {θDROPy (η1 ), . . ., θDROPy (ηk )}.
This by virtue of (4) concludes the proof.

✷

Informally, (i) states that every computed answer substitution of φθ validates
it. It is useful to point out that (ii) is a counterpart of Theorem 3 in Clark
[Cla78]. Intuitively, it states that a query is equivalent to the disjunction of its
computed answer substitutions written out in an equational form (using the hηi
notation). In our case this property holds only if error is not a possible outcome.
Indeed, if [[s = t]](θ) = {error}, then nothing can be stated about the status of
the statement I |= (s = t)θ.
Note that in case error 6∈ [[φ]](θ), (ii) implies (i) by virtue of Note 2. On the
other hand, if error ∈ [[φ]](θ), then (i) can still be applicable while (ii) not.
Additionally existential quantifiers have to be used in an appropriate way.
The formulas of the form ∃yhηi also appear in Maher [Mah88] in connection
with a study of the decision procedures for the algebras of trees. In fact, there
are some interesting connections between this paper and ours that could be
investigated in a closer detail.
15

6

Conclusions and Future Work

In this paper we provided a denotational semantics to first-order logic formulas.
This semantics is a counterpart of the operational semantics introduced in Apt
and Bezem [AB99]. The important difference is that we provide here a more
general treatment of equality according to which a non-ground term can be
assigned to a variable. This realizes logical variables in the framework of Apt
and Bezem [AB99]. This feature led to a number of complications in the proof
of the Soundness Theorem 1.
One of the advantages of this theorem is that it allows us to reason about
the considered program simply by comparing it to the formula representing its
specification. In the case of operational semantics this was exemplified in Apt
and Bezem [AB99] by showing how to verify non-trivial Alma-0 programs that
do not include destructive assignment.
Note that it is straightforward to extend the semantics here provided to other
well-known programming constructs, such as destructive assignment, while construct and recursion. However, as soon as a destructive assignment is introduced,
the relation with the definition of truth in the sense of Soundness Theorem 1 is
lost and the just mentioned approach to program verification cannot be anymore
applied. In fact, the right approach to the verification of the resulting programs
is an appropriately designed Hoare’s logic or the weakest precondition semantics.
The work here reported can be extended in several directions. First of all, it
would be useful to prove equivalence between the operational and denotational
semantics. Also, it would interesting to specialize the introduced semantics to
specific interpretations for which the semantics could generate less often an error. Examples are Herbrand interpretations for an arbitrary first-order language
in which the meaning of equalities could be rendered using most general unifiers, and the standard interpretation over reals for the language defining linear
equations; these equations can be handled by means of the usual elimination
procedure. In both cases the equality could be dealt with without introducing
the error state at all.
Other possible research directions were already mentioned in Apt and Bezem
[AB99]. These involved addition of recursive procedures, of constraints, and provision of a support for automated verification of programs written in Alma-0.
The last item there mentioned, relation to dynamic predicate logic, was in the
meantime extensively studied in the work of van Eijck [vE98] who, starting with
Apt and Bezem [AB99], defined a number of semantics for dynamic predicate
logic in which the existential quantifier has a different, dynamic scope. This work
was motivated by applications in natural language processing.

Acknowledgments
Many thanks to Marc Bezem for helpful discussions on the subject of this paper.
16

References
AB99.

K. R. Apt and M. A. Bezem. Formulas as programs. In K.R. Apt, V.W.
Marek, M. Truszczyński, and D.S. Warren, editors, The Logic Programming Paradigm: A 25 Year Perspective, pages 75–107, 1999. Available via
http://xxx.lanl.gov/archive/cs/.
ABPS98. K. R. Apt, J. Brunekreef, V. Partington, and A. Schaerf. Alma-0: An imperative language that supports declarative programming. ACM Toplas,
20(5):1014–1066, 1998.
Cla78.
K. L. Clark. Negation as failure. In H. Gallaire and J. Minker, editors, Logic
and Databases, pages 293–322. Plenum Press, New York, 1978.
Cla79.
E. M. Clarke. Programming language constructs for which it is impossible to
obtain good Hoare axiom systems. J. of the ACM, 26(1):129–147, January
1979.
dB80.
J. W. de Bakker. Mathematical Theory of Program Correctness. PrenticeHall International, Englewood Cliffs, N.J., 1980.
DVS+ 88. M. Dincbas, P. Van Hentenryck, H. Simonis, A. Aggoun, T. Graf, and
F. Berthier. The Constraint Logic Programming Language CHIP. In FGCS88: Proceedings International Conference on Fifth Generation Computer Systems, pages 693–702, Tokyo, December 1988. ICOT.
HL94.
P. M. Hill and J. W. Lloyd. The Gödel Programming Language. The MIT
Press, 1994.
JMSY92. J. Jaffar, S. Michayov, P. Stuckey, and R. Yap. The CLP(R) language
and system. ACM Transactions on Programming Languages and Systems,
14(3):339–395, July 1992.
KK71.
R.A. Kowalski and D. Kuehner. Linear resolution with selection function.
Artificial Intelligence, 2:227–260, 1971.
Kow74. R.A. Kowalski. Predicate logic as a programming language. In Proceedings
IFIP’74, pages 569–574. North-Holland, 1974.
LT84.
J. W. Lloyd and R. W. Topor. Making Prolog more expressive. Journal of
Logic Programming, 1:225–240, 1984.
Mah88. M.J. Maher. Complete axiomatizations of the algebras of finite, rational
and infinite trees. In Proceedings of the Fifth Annual Symposium on Logic
in Computer Science, pages 348–357. The MIT Press, 1988.
Rob65. J.A. Robinson. A machine-oriented logic based on the resolution principle.
J. ACM, 12(1):23–41, 1965.
SS71.
D. S. Scott and C. Strachey. Towards a mathematical semantics for computer languages. Technical Report PRG–6, Programming Research Group,
University of Oxford, 1971.
Van89.
P. Van Hentenryck. Constraint Satisfaction in Logic Programming. Logic
Programming Series. MIT Press, Cambridge, MA, 1989.
vE98.
J. van Eijck. Programming with dynamic predicate logic. Technical Report
INS-R9810, CWI, Amsterdam, 1998.

17

