Under consideration for publication in Theory and Practice of Logic Programming

1

arXiv:1707.04704v1 [] 15 Jul 2017

The Intricacies of Three-Valued Extensional
Semantics for Higher-Order Logic Programs
PANOS RONDOGIANNIS and IOANNA SYMEONIDOU
National and Kapodistrian University of Athens, Athens, Greece
(e-mail: {prondo,i.symeonidou}@di.uoa.gr)
submitted 1 January 2003; revised 1 January 2003; accepted 1 January 2003

Abstract
In (Bezem 1999; Bezem 2001), M. Bezem defined an extensional semantics for positive higherorder logic programs. Recently, it was demonstrated in (Rondogiannis and Symeonidou 2016)
that Bezem’s technique can be extended to higher-order logic programs with negation, retaining
its extensional properties, provided that it is interpreted under a logic with an infinite number
of truth values. In (Rondogiannis and Symeonidou 2017) it was also demonstrated that Bezem’s
technique, when extended under the stable model semantics, does not in general lead to extensional stable models. In this paper we consider the problem of extending Bezem’s technique
under the well-founded semantics. We demonstrate that the well-founded extension fails to retain extensionality in the general case. On the positive side, we demonstrate that for stratified
higher-order logic programs, extensionality is indeed achieved. We analyze the reasons of the failure of extensionality in the general case, arguing that a three-valued setting can not distinguish
between certain predicates that appear to have a different behaviour inside a program context,
but which happen to be identical as three-valued relations. The paper is under consideration for
acceptance in TPLP.
KEYWORDS: Extensional Higher-Order Logic Programming, Negation in Logic Programming.

1 Introduction
Recent research (Wadge 1991; Bezem 1999; Bezem 2001; Kountouriotis et al. 2005; Charalambidis et al. 2013; Rondogiannis and Symeonidou 2016; Charalambidis et al. 2017)
has investigated the possibility of providing extensional semantics to higher-order logic
programming. Under an extensional semantics, predicates denote sets, and therefore one
can use standard set theory in order to understand programs and reason about them. Of
course, extensionality comes with a price: to obtain an extensional semantics, one usually
has to consider higher-order logic programs with a relatively restricted syntax. Actually
this is a main difference between the extensional and the more traditional intensional
approaches to higher-order logic programming such as (Miller and Nadathur 2012; Chen
et al. 1993): the latter languages have a richer syntax and expressive capabilities but they
are not usually amenable to a standard set-theoretic semantics.
There exist two main research directions for providing extensional semantics to higherorder logic programs. The first one (Wadge 1991; Kountouriotis et al. 2005; Charalambidis et al. 2013; Charalambidis et al. 2014) has been developed using domain-theoretic

2

P. Rondogiannis and I. Symeonidou

tools, and resembles the techniques for assigning denotational semantics to functional
languages. The second approach (Bezem 1999; Bezem 2001; Rondogiannis and Symeonidou 2016) relies on the syntactic entities that exist in a program, and is based on
processing the ground instantiation of the program. The two research directions are not
unrelated: it has recently been shown (Charalambidis et al. 2017) that for a broad class
of positive programs, the two approaches coincide with respect to ground atoms.
In this paper we focus exclusively on the second extensional approach. This approach
was initially proposed in (Bezem 1999; Bezem 2001) for positive (i.e., negationless) higherorder logic programs. Recently, it was demonstrated in (Rondogiannis and Symeonidou
2016) that by combining the technique of (Bezem 1999; Bezem 2001) with the infinitevalued semantics of (Rondogiannis and Wadge 2005), we obtain an extensional semantics
for higher-order logic programs with negation. In the extended version (Rondogiannis and
Symeonidou 2017) of the paper (Rondogiannis and Symeonidou 2016) a negative and unexpected result is established: by combining the technique of (Bezem 1999; Bezem 2001)
with the stable model semantics (Gelfond and Lifschitz 1988), we get a semantics that is
not necessarily extensional! It remained as an open problem of (Rondogiannis and Symeonidou 2016) whether the combination of the technique of (Bezem 1999; Bezem 2001)
with the well-founded approach (Gelder et al. 1991) leads to an extensional semantics.
It is exactly this problem that we undertake to solve in the present paper.
We demonstrate that the well-founded extension of Bezem’s technique fails to retain
extensionality in the general case. On the positive side, we prove that for stratified
higher-order logic programs, extensionality is indeed achieved. We analyze the reasons
of the failure of extensionality in the general case, and claim that this is not an inherent
shortcoming of Bezem’s approach but a more general phenomenon. In particular we
argue that restricting attention to three-valued logic appears to “throw away too much
information” and makes predicates that are expected to have different behaviours, appear
as identical three-valued relations. The main contributions of the present paper can be
summarized as follows:
• We demonstrate that the well-founded adaptation of Bezem’s technique, does not
in general lead to an extensional model. In particular, we exhibit a program with
a non-extensional well-founded model. This result, despite its negative flavor, indicates that the addition of negation to higher-order logic programming is not such a
straightforward task as it was possibly initially anticipated. Notice that, as it was
recently demonstrated in (Rondogiannis and Symeonidou 2017), the stable model
adaptation of Bezem’s technique is also non-extensional in general.
• Despite the above negative result, we prove that the well-founded adaptation of
Bezem’s technique gives an extensional two-valued model in the case of stratified
programs. This result affirms the importance and the well-behaved nature of stratified programs, which was, until now, only known for the first-order case.
• We study the more general question of the possible existence of an alternative
extensional three-valued semantics for higher-order logic programs with negation.
We indicate that in order to achieve such a semantics, one has to make some
(arguably) non-standard assumptions regarding the behaviour of negation.
The rest of the paper is organized as follows. Section 2 introduces the basic notions
and the advantages of the extensional approach to the semantics of higher-order logic

The Intricacies of Three-Valued Extensional Semantics for Higher-Order LP

3

programming. Section 3 presents in an intuitive way the main concepts and results of the
paper. Section 4 introduces the syntax and Section 5 the semantics of our source language.
Section 6 demonstrates that Bezem’s approach is not extensional under the well-founded
semantics. In Section 7 it is established that stratified programs have an extensional,
two-valued, well-founded semantics. Section 8 concludes by discussing the restrictions
that any reasonable three-valued semantics would have with respect to extensionality.
The proofs of all results are given in the corresponding appendices.
2 Extensional Higher-Order Logic Programming
In (Wadge 1991) W. W. Wadge suggested that if we appropriately restrict the syntax
of higher-order logic programming, then we can obtain languages that can be assigned
a standard denotational semantics in which predicates denote sets. In other words, for
such syntactically restricted languages one can apply traditional domain-theoretic notions
and tools that have been used extensively in higher-order functional programming. The
most crucial syntactic restriction imposed by Wadge (and also later independently by M.
Bezem (Bezem 1999)), is the following:
The extensionality syntactic restriction: In the head of every rule in a program, each
argument of predicate type must be a variable, and all such variables must be distinct.
Example 1
The following is a legitimate program that defines the union of two relations P, Q (for
the moment we use ad-hoc Prolog-like syntax):
union(P,Q)(X):-P(X).
union(P,Q)(X):-Q(X).
However, the following program does not satisfy Wadge’s restriction:
q(a).
r(q).
because the predicate constant q appears as an argument in the head of a rule. Similarly,
the program:
p(Q,Q):-Q(a).
is problematic because the predicate variable Q is used twice in the head of the rule.
The advantages of extensionality were identified by Wadge and Bezem in their respective papers. First of all, under the extensional approach, program predicates can be
understood declaratively in terms of extensional notions. For example, the program:
map(R,[],[]).
map(R,[H1|T1],[H2|T2]):-R(H1,H2), map(R,T1,T2).
can be understood in a similar way as the well-known map function of Haskell. Moreover,
since under the extensional approach predicates denote sets, two predicates that are
true of the same arguments, are considered indistinguishable. So, for example, if we
define two sorting predicates merge sort and quick sort that have the same type, say
τ , and that perform the same task (possibly with different efficiency), it is guaranteed
that any predicate which operates on relations of type τ will have the same behaviour

4

P. Rondogiannis and I. Symeonidou

whether it is given merge sort or quick sort as an argument. As mentioned in (Wadge
1991) “extensionality means exactly that predicates are used as black boxes - and the
“black box” concept is central to all kinds of engineering”. It is this property that makes
extensional languages so appealing (and is actually one of the greatest assets of traditional
functional programming).
Another important advantage of this declarative approach to higher-order logic programming is that many techniques and ideas that have been successfully developed in
the functional programming world (such as program transformations, optimizations, techniques for proving program correctness, and so on), could be transferred to the higherorder logic programming domain, opening in this way promising new research directions
for logic programming as a whole.
3 An Intuitive Overview of the Proposed Approach
In this paper we consider the semantic technique for positive higher-order logic programs
proposed in (Bezem 1999; Bezem 2001) and we investigate whether it can be applied in
order to provide an extensional well-founded semantics for higher-order logic programs
with negation in clause bodies. In this section we give an intuitive description of Bezem’s
idea and we outline how we use it when negation is added to programs.
Given a positive higher-order logic program, the starting idea behind Bezem’s approach
is to take its “ground instantiation”, in which we replace variables with well-typed terms
that can be created using syntactic entities that appear in the program. For example,
consider the higher-order program below:
q(a).
q(b).
p(Q):-Q(a).
id(R)(X):-R(X).
In order to obtain the ground instantiation of this program, we consider each clause
and replace each variable of the clause with a ground term that has the same type as
the variable under consideration (the formal definition of this procedure will be given in
Definition 8). In this way we obtain the following infinite program:
q(a).
q(b).
p(q):-q(a).
id(q)(a):-q(a).
id(q)(b):-q(b).
p(id(q)):-id(q)(a).
···
One can now treat the new program as an infinite propositional one (i.e., each ground
atom can be seen as a propositional variable). This implies that we can use the standard
least fixed-point construction of classical logic programming (see for example (Lloyd
1987)) in order to compute the set of atoms that should be taken as “true”. In our
example, the least fixed-point will contain atoms such as q(a), q(b), p(q), id(q)(a),
id(q)(b), p(id(q)), and so on.

The Intricacies of Three-Valued Extensional Semantics for Higher-Order LP

5

Bezem demonstrated that the least fixed-point semantics of the ground instantiation
of every positive higher-order logic program of the language considered in (Bezem 1999;
Bezem 2001), is extensional in a sense that can be explained as follows. In our example, q
and id(q) are equal since they are both true of exactly the constants a and b. Therefore,
we expect that (for example) if p(q) is true then p(id(q)) is also true, because q and
id(q) should be considered as indistinguishable. This property of “indistinguishability”
is formally defined in (Bezem 1999; Bezem 2001) and it is demonstrated that it holds in
the least fixed-point of the immediate consequence operator of the ground instantiation
of every program that abides to the simple extensionality syntactic restriction given in
the previous section (and formally described by Definition 5 later in the paper).
The key idea behind extending Bezem’s semantics in order to apply to higher-order
logic programs with negation, is straightforward to state: given such a program, we first
take its ground instantiation. The resulting program is a (possibly infinite) propositional
program with negation and therefore we can compute its semantics in any standard way
that exists for obtaining the meaning of such programs. For example, one could use
the well-founded semantics (Gelder et al. 1991), the stable model semantics (Gelfond
and Lifschitz 1988), or the infinite-valued semantics (Rondogiannis and Wadge 2005),
and then proceed to examine whether the well-founded model (respectively, each stable
model, or the minimum infinite-valued model) is extensional in the sense of (Bezem 1999;
Bezem 2001) (informally described above).
An open problem posed in (Rondogiannis and Symeonidou 2017) was whether Bezem’s
technique, under the well-founded semantics, always leads to an extensional well-founded
model. As we are going to see in the subsequent sections, this is not the case. In particular,
we exhibit a program containing three predicates s, p and q, such that p and q are
extensionally equal under the well-founded semantics, but s(p) and s(q) have a different
truth value. On the positive side, we prove that every stratified higher-order logic program
with negation has an extensional well-founded model. In this sense, we identify a broad
class of programs that are well-behaved in terms of extensionality.
4 The Syntax of H
In this section we define the syntax of the language H that we use throughout the paper.
H is based on a simple type system with two base types: o, the boolean domain, and
ι, the domain of data objects. The composite types are partitioned into three classes:
functional (assigned to function symbols), predicate (assigned to predicate symbols) and
argument (assigned to parameters of predicates).
Definition 1
A type can either be functional, predicate, or argument, denoted by σ, π and ρ respectively
and defined as:
σ := ι | (ι → σ)
π := o | (ρ → π)
ρ := ι | π
We will use τ to denote an arbitrary type (either functional, predicate, or argument).
As usual, the binary operator → is right-associative. A functional type that is different

6

P. Rondogiannis and I. Symeonidou

than ι will often be written in the form ιn → ι, n ≥ 1. Moreover, it can be easily seen
that every predicate type π can be written in the form ρ1 → · · · → ρn → o, n ≥ 0 (for
n = 0 we assume that π = o). We proceed by defining the syntax of H:
Definition 2
The alphabet of H consists of the following: predicate variables of every predicate type π
(denoted by capital letters such as Q, R, S, . . .); individual variables of type ι (denoted by
capital letters such as X, Y, Z, . . .); predicate constants of every predicate type π (denoted
by lowercase letters such as p, q, r, . . .); individual constants of type ι (denoted by lowercase letters such as a, b, c, . . .); function symbols of every functional type σ 6= ι (denoted
by lowercase letters such as f, g, h, . . .); the inverse implication constant ←; the negation
constant ∼; the comma; the left and right parentheses; and the equality constant ≈ for
comparing terms of type ι.
Arbitrary variables will be usually denoted by V and its subscripted versions.
Definition 3
The set of terms of H is defined as follows: every predicate variable (respectively, predicate
constant) of type π is a term of type π; every individual variable (respectively, individual
constant) of type ι is a term of type ι; if f is an n-ary function symbol and E1 , . . . , En
are terms of type ι then (f E1 · · · En ) is a term of type ι; if E1 is a term of type ρ → π
and E2 a term of type ρ then (E1 E2 ) is a term of type π.
Definition 4
The set of expressions of H is defined as follows: a term of type ρ is an expression of type
ρ; if E is a term of type o then (∼E) is an expression of type o; if E1 and E2 are terms of
type ι, then (E1 ≈ E2 ) is an expression of type o.
We will omit parentheses when no confusion arises. To denote that an expression E
has type ρ we will often write E : ρ. We will write vars(E) to denote the set of all the
variables in E. Expressions (respectively, terms) that have no variables will be referred
to as ground expressions (respectively, ground terms). Terms of type o will be referred to
as atoms. Expressions of type o that do not contain negation, i.e. expressions of the form
(E1 ≈ E2 ) or atoms, will be called positive literals, while expressions of the form (∼E)
will be called negative literals. A literal is either a positive literal or a negative literal.
Definition 5
A clause of H is a formula p V1 · · · Vn ← L1 , . . . , Lm , where p is a predicate constant of
type ρ1 → · · · → ρn → o, V1 , . . . , Vn are distinct variables of types ρ1 , . . . , ρn respectively
and L1 , . . . , Lm are literals. The term p V1 · · · Vn is called the head of the clause, the variables V1 , . . . , Vn are the formal parameters of the clause and the conjunction L1 , . . . , Lm
is its body. A program P of H is a finite set of clauses.
Example 2
The program below defines the subset relation over unary predicates:
subset S1 S2 ← ∼(nonsubset S1 S2)
nonsubset S1 S2 ← (S1 X), ∼(S2 X)
Given unary predicates p and q, subset p q is true iff p is a subset of q.

The Intricacies of Three-Valued Extensional Semantics for Higher-Order LP

7

Example 3
For a more “real-life” higher-order logic program with negation, assume that we have a
unary predicate movie M and a binary predicate ranking M R which returns the ranking
R of a given movie M. Consider also the following first-order predicate that defines a
preference over movies based on their ranking:
prefer M1 M2 ← movie M1, movie M2, ranking M1 R1, ranking M2 R2, R1>R2.
The following higher-order predicate winnow (see for example (Chomicki 2003)) can be
used to select all the “best” tuples T out of a given relation R based on a preference
relation P:
winnow P R T ← R T, ∼(bypassed P R T).
bypassed P R T ← R T1, P T1 T.
Intuitively, winnow returns all the tuples T of the relation R such that there does not exist
any tuple T1 in the relation R that is better from T with respect to the preference relation
P. For example, if we ask the query ?- winnow prefer movie T. we expect as answers
all those movies that have the highest possible ranking. Notice that since winnow is a
higher-order predicate, it can be invoked with different arguments; for example, it can be
used to select out of a book relation, all those books that have the lowest possible price,
or out of a flight relation all those flights that go to London, and so on.
The ground instantiation of a program is described by the following definitions:
Definition 6
A substitution θ is a finite set of the form {V1 /E1 , . . . , Vn /En } where the Vi ’s are different
variables and each Ei is a term having the same type as Vi . We write dom(θ) to denote
the domain {V1 , . . . , Vn } of θ. If all the terms E1 , . . . , En are ground, θ is called a ground
substitution.
Definition 7
Let θ be a substitution and E be an expression. Then, Eθ is an expression obtained from
E as follows:
•
•
•
•
•
•

Eθ = E if E is a predicate constant or individual constant;
Vθ = θ(V) if V ∈ dom(θ); otherwise, Vθ = V;
(f E1 · · · En )θ = (f E1 θ · · · En θ);
(E1 E2 )θ = (E1 θ E2 θ);
(∼E)θ = (∼Eθ);
(E1 ≈ E2 )θ = (E1 θ ≈ E2 θ).

If θ is a ground substitution such that vars(E) ⊆ dom(θ), then the ground expression Eθ
is called a ground instance of E.
Definition 8
Let P be a program. A ground instance of a clause p V1 · · · Vn ← L1 , . . . , Lm of P is a
formula (p V1 · · · Vn )θ ← L1 θ, . . . , Lm θ, where θ is a ground substitution whose domain
is the set of all variables that appear in the clause, such that for every V ∈ dom(θ) with
V : ρ, θ(V) is a ground term of type ρ that has been formed with predicate constants,
function symbols, and individual constants that appear in P. The ground instantiation of
a program P, denoted by Gr(P), is the (possibly infinite) set that contains all the ground
instances of the clauses of P.

8

P. Rondogiannis and I. Symeonidou
5 The Semantics of H

In (Bezem 1999; Bezem 2001) M. Bezem developed a semantics for higher-order logic
programs which generalizes the familiar Herbrand-model semantics of classical (firstorder) logic programs. In this section we extend Bezem’s semantics to the case of higherorder logic programs with negation.
In order to interpret the programs of H, we need to specify the semantic domains in
which the expressions of each type τ are assigned their meanings. The following definition
is a slightly modified version of the corresponding definition of (Bezem 1999; Bezem
2001) and it implies that the expressions of predicate types should be understood as
representing functions. We use [S1 → S2 ] to denote the set of (possibly partial) functions
from a set S1 to a set S2 . The possibility to have a partial function arises due to a
technicality which is explained in the remark just above Definition 11.
Definition 9
A functional type structure S for H consists of two non-empty sets D and A together
with an assignment Jτ K to each type τ of H, so that the following are satisfied:
•
•
•
•

JιK = D;
Jιn → ιK = Dn → D;
JoK = A;
Jρ → πK ⊆ [JρK → JπK].

Given a functional type structure S, any function v : JoK → {false, 0, true} will be called
a three-valued valuation function (or simply valuation function) for S. We will use the
term two-valued valuation functions to distinguish the subset of valuation functions which
do not assign the value 0 to any element of JoK, i.e. the functions v : JoK → {false, true}.
It is customary in the study of the semantics of logic programming languages to restrict
attention to Herbrand interpretations. Given a program P, a Hebrand interpretation is
one that has as its underlying universe the so-called Herbrand universe of P:
Definition 10
For a program P, we define the Herbrand universe for every argument type ρ, denoted by
UP,ρ to be the set of all ground terms of type ρ that can be formed out of the individual
constants, function symbols, and predicate constants in the program. Moreover, we define
+
UP,o
to be the set of all ground expressions of type o, that can be formed out of the above
+
symbols, i.e. the set UP,o
= UP,o ∪ {(E1 ≈ E2 ) | E1 , E2 ∈ UP,ι } ∪ {(∼E) | E ∈ UP,o }.
Following (Bezem 1999; Bezem 2001), we take D and A in Definition 9 to be equal to
+
UP,ι and UP,o
respectively. Then, for each predicate type ρ → π, each element of UP,ρ→π
can be perceived as a function mapping elements of JρK to elements of JπK, through syntactic application mapping. That is, E ∈ UP,ρ→π can be viewed as the function mapping
each term E′ ∈ UP,ρ to the term (E E′ ) ∈ UP,π . Similarly, every n-ary function symbol f
n
appearing in P can be viewed as the function mapping each element (E1 , . . . , En ) ∈ UP,ι
to the term (f E1 · · · En ) ∈ UP,ι .
Remark: There is a small technicality here which we need to clarify. In the case where
+
ρ = o, E ∈ UP,o→π is a partial function because it maps elements of UP,o (and not of UP,o
)
to elements of UP,π ; this is due to the fact that our syntax does not allow an expression
of type o → π to take as argument an expression of the form (E1 ≈ E2 ) nor of the form
(∼E). In all other cases (i.e., when ρ 6= o), E represents a total function.

The Intricacies of Three-Valued Extensional Semantics for Higher-Order LP

9

Definition 11
A (three-valued) Herbrand interpretation I of a program P consists of:
+
1. the functional type structure SP , such that D = UP,ι , A = UP,o
and Jρ → πK =
UP,ρ→π for every predicate type ρ → π, called the Herbrand type structure of P;
2. the assignment to each individual constant c in P, of the element I(c) = c; to each
predicate constant p in P, of the element I(p) = p; to each function symbol f in P,
of the element I(f) = f;
+
3. a valuation function vI (·) for SP , assigning to each element of UP,o
an element in
{false, 0, true}, while satisfying the following:
(
false, if E1 6= E2
• for all E1 , E2 ∈ UP,ι , vI ((E1 ≈ E2 )) =
;
true, if E1 = E2



false, if vI (E) = true
.
• for all E ∈ UP,o , vI ((∼E)) = 0,
if vI (E) = 0


true, if v (E) = false
I

We call vI (·) the valuation function of I and omit the reference to SP , since the latter
is common to all Herbrand interpretations of a program. In fact, individual Herbrand
interpretations are only set apart by their valuation functions. If the valuation function
vI (·) is two-valued, then I will also be called a two-valued Herbrand interpretation.

Definition 12
A Herbrand state (or simply state) s of a program P is a function that assigns to each
variable V of type ρ an element of UP,ρ .
Given a Herbrand interpretation I and state s, we can define the semantics of expressions
with respect to I and s.
Definition 13
Let P be a program. Also, let I be a Herbrand interpretation and s a Herbrand state of
P. Then the semantics of expressions with respect to I and s is defined as follows:
•
•
•
•

JcKI,s = I(c) = c, for every individual constant c;
JpKI,s = I(p) = p, for every predicate constant p;
JVKI,s = s(V), for every variable V;
J(f E1 · · · En )KI,s = (I(f) JE1 KI,s · · · JEn KI,s ) = (f JE1 KI,s · · · JEn KI,s ), for every nary function symbol f;
• J(E1 E2 )KI,s = (JE1 KI,s JE2 KI,s );
• J(E1 ≈ E2 )KI,s = (JE1 KI,s ≈ JE2 KI,s );
• J(∼E)KI,s = (∼JEKI,s ).
It is easy to see that the semantic function J·K is well defined, in the sense that, for every
Herbrand state s and every expression E of every argument type ρ, we have JEKI,s ∈ JρK.
Note that this makes JEKI,s a ground expression of the language. Also note, that if E is a
ground expression then JEKI,s = E; therefore, if E is a ground literal, we can write vI (E)
instead of vI (JEKI,s ). Stretching this abuse of notation a little further, we can extend a
valuation function to assign truth values to ground conjunctions of literals; this allows
us to define the concept of Herbrand models for our higher-order programs in the same
way as in classical logic programming.

10

P. Rondogiannis and I. Symeonidou

Definition 14
Let P be a program and I be a Herbrand interpretation of P. We define vI (L1 , . . . , Ln ) =
+
min{vI (L1 ), . . . , vI (Ln )} for all L1 , . . . , Ln ∈ UP,o
. Moreover, we say I is a model of P
if vI (JAKI,s ) ≥ vI (JL1 KI,s , . . . , JLm KI,s ) holds for every clause A ← L1 , . . . , Lm and every
Herbrand state s of P.
Bezem’s semantics is based on the observation that, given a positive higher-order
program, we can use the minimum model of its ground instantiation as a (two-valued)
valuation function defining a Herbrand interpretation for the initial program itself. We
follow the same idea but now for programs with negation: we can use as the valuation
function of a given H program, the Herbrand model defined by any semantic approach
that applies to its ground instantiation. Actually, we demonstrate (see Theorem 1 below)
that any interpretation I of the higher-order program P will be a minimal model of P, if
its chosen valuation function is a minimal model of Gr(P).
We consider two different notions of minimality, based on the truth ordering ≤ and the
Fitting ordering  of truth values, respectively. Recall that ≤ is the partial order defined
by false ≤ 0 ≤ true, while  is the partial order defined by 0  false and 0  true.
Definition 15
If I and J are two Herbrand interpretations of a higher-order program P, we say I ≤ J
(respectively, I  J) if, for all atoms A in UP,o we have vI (A) ≤ vJ (A) (resp., vI (A) 
vJ (A)). If M is a model of P then we say it is ≤-minimal (resp., -minimal) if there does
not exist a different model N of P, such that N ≤ M (resp., N  M ).
Theorem 1
Let P be a program and let Gr(P) be its ground instantiation. Also let M be a partial interpretation1 of Gr(P) and let M be the Herbrand interpretation of P, such that
vM (A) = M (A) for every A ∈ UP,o . Then, M is a Herbrand model of P if and only if M
is a model of Gr(P). Moreover, M is ≤-minimal (respectively, -minimal) if and only if
M is ≤-minimal (respectively, -minimal).
As an application of the above developments we define two special Herbrand interpretations of higher-order programs, employing the well-known perfect model (Apt et al. 1988;
Gelder 1989) and well-founded model (Gelder et al. 1991) of the ground instantiation of
a program, as valuation functions.
Definition 16
Let P be a program and let Gr(P) be the ground instantiation of P. Also, let NGr(P) be the
perfect model1 (if this exists) and MGr(P) be the well-founded model1 of Gr(P). We define
NP to be the two-valued Herbrand interpretation of P such that vNP (A) = NGr(P) (A) for
every A ∈ UP,o . Similarly, we define MP to be the three-valued Herbrand interpretation
of P such that vMP (A) = MGr(P) (A) for every A ∈ UP,o .
Clearly, by Theorem 1, NP (if it exists) is a two-valued minimal model and MP is a
three-valued minimal model of P. In the following sections we investigate their suitability
for providing extensional semantics for H programs. In particular, we examine if each
1

See the Appendix for the relevant definitions.

The Intricacies of Three-Valued Extensional Semantics for Higher-Order LP

11

of them enjoys the extensionality property, formally defined (Bezem 1999; Bezem 2001)
through relations ∼
=v,τ over the set of expressions of a given type τ and under a given
valuation function v. These relations intuitively express extensional equality of type τ , in
the sense discussed in Section 3. For the purposes of this paper only extensional equality
of argument types will be needed, for which the formal definition is as follows:
Definition 17
Let S be a functional type structure and v be a valuation function for S. For every
argument type ρ we define the relations ∼
=v,ρ on JρK as follows: Let d, d′ ∈ JρK; then
d∼
=v,ρ d′ if and only if
1. ρ = ι and d = d′ , or
2. ρ = o and v(d) = v(d′ ), or
3. ρ = ρ′ → π and d e ∼
=v,ρ′ e′ and d e, d′ e′
=v,π d′ e′ for all e, e′ ∈ Jρ′ K, such that e ∼
are both defined.
One can easily verify that, for all d, d′ ∈ Jρ1 → · · · → ρn → oK, e1 , e′1 ∈ Jρ1 K, . . . , en , e′n ∈
Jρn K, if d ∼
=v,ρn e′n and d e1 · · · en , d′ e′1 · · · e′n
=v,ρ1 e′1 , . . . , en ∼
=v,ρ1 →···→ρn →o d′ , e1 ∼
′ ′
are both defined, then v(d e1 · · · en ) = v(d e1 · · · e′n ).
Generally, it is not guaranteed that such relations will be equivalence relations; rather
they are partial equivalences (they are shown in (Bezem 1999) to be symmetric and transitive). Whether they are moreover reflexive, depends on the specific valuation function.
The above discussion leads to the notion of extensional interpretation:
Definition 18
Let P be a program and let I be a Herbrand interpretation of P with valuation function
vI . We say I is extensional if for all argument types ρ the relations ∼
=vI ,ρ are reflexive,
i.e. for all E ∈ JρK, it holds that E ∼
E.
=vI ,ρ
The above notion will be extensively used in the following two sections.

6 Non-Extensionality of the Well-Founded Model
In this section we demonstrate that the adaptation of Bezem’s technique under the wellfounded semantics does not in general preserve extensionality. In particular, we exhibit
below a program that has a non-extensional well-founded model.
Example 4
Consider the higher-order program P:
s
p
q
w
where the predicate variable Q
type o. Before stating formally
an intuitive level are in order.
can view p as representing the

Q
R
R
R

←
←
←
←

Q (s Q)
R
∼(w R)
∼R

is of type o → o and the predicate variable R is of
the non-extensionality result, certain explanations at
Consider first the predicate p of type o → o. One
identity relation on truth values, i.e., as the relation

12

P. Rondogiannis and I. Symeonidou

{(v, v) | v ∈ {false, 0, true}}. It is not hard to see that the predicate q of type o → o, represents exactly the same relation. However, the definition of q involves two applications
of negation, while p is defined directly (without the use of negation).
Consider now the predicate s of type (o → o) → o which can take as a parameter either
p or q. When s takes p as a parameter, we get the following two clauses (by substituting
p for Q and (s p) for R in the above program):
s p ← p (s p)
p (s p) ← (s p)
A recursive definition of this form assigns to (s p), under the well-founded semantics,
the value false. Consider on the other hand the case where s takes q as a parameter.
Then, by doing analogous substitutions, we get the following three clauses:
s q ← q (s q)
q (s q) ← ∼(w (s q))
w (s q) ← ∼(s q)
Under the well-founded semantics, (s q) is assigned the value 0. In other words, despite
the fact that p and q are extensionally equal (see also below), (s p) and (s q) have
different truth values. In conclusion, the adaptation of the well-founded semantics under
Bezem’s technique does not lead to an extensional model in all cases.
Of course, the above discussion is based on intuitive arguments, but it is not hard to
formalize it. The main difficulty lies in establishing that p and q are extensionally equal
because the above program has an infinite ground instantiation Gr(P) (see Appendix B).
The following lemma, whose detailed proof is given in Appendix B, suggests that MP , i.e.
the Herbrand interpretation of our example program P defined by using the well-founded
model MGr(P) of Gr(P) as the valuation function, is not extensional.
Lemma 1
The Herbrand interpretation MP of the program of Example 4 is not extensional.
The consequences that the above lemma has for the investigation of alternative extensional three-valued semantics for higher-order logic programs with negation, will be discussed in Section 8.
A natural question that arises is whether there exists a broad and useful class of programs that are extensional under the well-founded semantics. The next section answers
exactly this question.

7 Extensionality of Stratified Programs
In this section we present the notion of stratified higher-order programs, originally introduced in (Rondogiannis and Symeonidou 2016), and argue that the well-founded model
of such a program enjoys the extensionality property defined in Section 5. In the following
definition, a predicate type π is understood to be greater than a second predicate type
π ′ , if π is of the form ρ1 → · · · → ρn → π ′ , where n ≥ 1.
Definition 19

The Intricacies of Three-Valued Extensional Semantics for Higher-Order LP

13

A program P is called stratified if and only if it is possible to decompose the set of all
predicate constants that appear in P into a finite number r of disjoint sets (called strata)
S1 , S2 , . . . , Sr , such that for every clause H ← A1 , . . . , Am , ∼B1 , . . . , ∼Bn in P, where the
predicate constant of H is p, we have:
1. for every i ≤ m, if Ai is a term that starts with a predicate constant q, then
stratum(q) ≤ stratum(p);
2. for every i ≤ m, if Ai is a term that starts with a predicate variable Q, then for all
predicate constants q that appear in P such that the type of q is greater than or
equal to the type of Q, it holds stratum(q) ≤ stratum(p);
3. for every i ≤ n, if Bi starts with a predicate constant q, then stratum(q) <
stratum(p);
4. for every i ≤ n, if Bi starts with a predicate variable Q, then for all predicate
constants q that appear in P such that the type of q is greater than or equal to the
type of Q, it holds stratum(q) < stratum(p);
where stratum(r) = i if the predicate constant r belongs to Si .
One may easily see that the stratification for classical logic programs (Apt et al. 1988;
Gelder 1989) is a special case of the above definition.
Example 5
It is straightforward to see that the program:
p Q ← ∼(Q a)
q X ← (X≈a)
is stratified. However, it can easily be checked that the program:
p Q ← ∼(Q a)
q X Y ← (X≈a),(Y≈a),p (q a)
is not stratified because if the term (q a) is substituted for Q we get a circularity through
negation. Notice that the type of q is ι → ι → o and it is greater than the type of Q
which is ι → o.
As it turns out, stratified higher-order logic programs have an extensional well-founded
model. The proof of the following theorem can be found in Appendix C.
Theorem 2
The well-founded model MP of a stratified program P is extensional.
Despite the fact that stratified programs lead to an extensional well-founded model,
we have not been able to verify that the same property holds for locally stratified higherorder logic programs (for a formal definition of the notion of local stratification for H
programs, please see (Rondogiannis and Symeonidou 2016)). On the other hand, our
attempts to find a locally stratified program with a non-extensional well-founded model
have also been unsuccessful, and therefore it is not at present clear to us whether this
class of programs is well-behaved with respect to extensionality, or not.

14

P. Rondogiannis and I. Symeonidou
8 The Restrictions of Three-Valued Approaches

In this section we re-examine the counterexample of Section 6 but now from a broader
perspective. In particular, we indicate that in order to achieve an extensional threevalued semantics for higher-order logic programs with negation, one has to make some
(arguably) non-standard assumptions regarding the behaviour of negation in such programs. On the other hand, a logic with an infinite number of truth values appears to be
a more appropriate vehicle for achieving extensionality. In the following discussion, we
assume some basic familiarity with the main intuition behind the approaches described
in (Rondogiannis and Symeonidou 2016) and in (Charalambidis et al. 2014).
Consider again the program of Section 6. Under the infinite-valued adaptation of
Bezem’s approach given in (Rondogiannis and Symeonidou 2016) and also under the
domain-theoretic infinite-valued approach of (Charalambidis et al. 2014), the semantics
of that program is extensional. The reason is that both of these approaches differentiate
the meaning of p from the meaning of q. The truth domain in both approaches is the set:
V = {Fα | α < Ω} ∪ {0} ∪ {Tα | α < Ω}
where Fα and Tα represent different degrees of truth and falsity, and Ω is the first
uncountable ordinal. Under this truth domain, predicate p (intuitively) corresponds to
the infinite-valued relation:
p = {(v, v) | v ∈ V }
while predicate q corresponds to the relation:
q = {(Fα , Fα+2 ) | α < Ω} ∪ {(0, 0)} ∪ {(Tα , Tα+2 ) | α < Ω}
Obviously, the relations p and q are different as sets and therefore it is not a surprise that
under both the semantics of (Rondogiannis and Symeonidou 2016) and (Charalambidis
et al. 2014), the atoms (s p) and (s q) have different truth values. Notice, however,
that if we collapse p and q in three-valued logic (i.e., if we map each Fα to false, each Tα
to true, and 0 to 0), the collapsed relations become identical.
Assume now that want to devise an (alternative to the one presented in this paper)
extensional three-valued semantics for H programs. Under such a semantics, it seems
reasonable to assume that p and q would correspond to the same three-valued relation,
namely {(v, v) | v ∈ {false, 0, true}}. Notice however that from a logic programming
perspective, p and q are expected to have a different operational behaviour when they
appear inside a program. In particular, given the program:
s Q ← Q (s Q)
p R ← R
we expect the atom (s p) to have the value false (due to the circularity that occurs if
we try to evaluate it), while given the program:
s Q ← Q (s Q)
q R ← ∼(w R)
w R ← ∼R
we expect the atom (s q) to have the value 0 due to the circularity through negation.

The Intricacies of Three-Valued Extensional Semantics for Higher-Order LP

15

At first sight, the above discussion seems to suggest that there is no way we can have a
three-valued extensional semantics for all higher-order logic programs with negation.
However, the above discussion is based mainly on our experience regarding the behaviour of first-order logic programs with negation. One could argue that we could devise
a semantics under which (s q) will also return the value false. One possible justification
for such a semantics would be that the definition of q uses two negations which cancel
each other, and therefore we should actually expect q to behave exactly like p when it
appears inside a program. Despite the fact that such a proposal seems somewhat unintuitive to us, we can not exclude it as a possibility. It is worth noting that such cancellations
of double negations appear in certain semantic approaches to negation. For example, for
certain extended propositional programs, the semantics based on approximation fixpoint
theory has the effect of canceling double negations (see for example (Denecker et al.
2012)[page 185, Example 1]). It is possible that higher-order logic programs with negation behave similarly to extended propositional programs, and it is conceivable that one
could construct an extensional three-valued semantics for all higher-order logic programs
with negation, using an approach based on approximation fixpoint theory. This research
direction certainly deserves further investigation.
It is our belief however that the most rigorous approach to extensionality for higherorder logic programs with negation, is through the use of the infinite-valued approach.
It is worth noting that recently, some advantages of the infinite-valued approach versus
the well-founded one, were identified in a different context. More specifically, as it was
recently demonstrated in (Ésik 2015; Carayol and Ésik 2016), the infinite-valued approach
satisfies all identities of iteration theories (Bloom and Ésik 1993), while the well-founded
semantics does not. Since iteration theories (intuitively) provide an abstract framework
for the evaluation of the merits of various semantic approaches for languages that involve
recursion, the results just mentioned give an extra incentive for the further study and
use of the infinite-valued approach.
References
Apt, K. R., Blair, H. A., and Walker, A. 1988. Towards a theory of declarative knowledge. In Foundations of Deductive Databases and Logic Programming, J. Minker, Ed. Morgan
Kaufmann, 89–148.
Bezem, M. 1999. Extensionality of simply typed logic programs. In Logic Programming: The
1999 International Conference, Las Cruces, New Mexico, USA, November 29 - December 4,
1999, D. D. Schreye, Ed. MIT Press, 395–410.
Bezem, M. 2001. An improved extensionality criterion for higher-order logic programs. In
Computer Science Logic, 15th International Workshop, CSL 2001. 10th Annual Conference
of the EACSL, Paris, France, September 10-13, 2001, Proceedings, L. Fribourg, Ed. Lecture
Notes in Computer Science, vol. 2142. Springer, 203–216.
Bloom, S. L. and Ésik, Z. 1993. Iteration Theories - The Equational Logic of Iterative Processes. EATCS Monographs on Theoretical Computer Science. Springer.
Carayol, A. and Ésik, Z. 2016. An analysis of the equational properties of the well-founded
fixed point. In Principles of Knowledge Representation and Reasoning: Proceedings of the
Fifteenth International Conference, KR 2016, Cape Town, South Africa, April 25-29, 2016.,
C. Baral, J. P. Delgrande, and F. Wolter, Eds. AAAI Press, 533–536.
Charalambidis, A., Ésik, Z., and Rondogiannis, P. 2014. Minimum model semantics for
extensional higher-order logic programming with negation. TPLP 14, 4-5, 725–737.

16

P. Rondogiannis and I. Symeonidou

Charalambidis, A., Handjopoulos, K., Rondogiannis, P., and Wadge, W. W. 2013. Extensional higher-order logic programming. ACM Trans. Comput. Log. 14, 3, 21.
Charalambidis, A., Rondogiannis, P., and Symeonidou, I. 2017. Equivalence of two fixedpoint semantics for definitional higher-order logic programs. Theor. Comput. Sci. 668, 27–42.
Chen, W., Kifer, M., and Warren, D. S. 1993. HILOG: A foundation for higher-order logic
programming. Journal of Logic Programming 15, 3, 187–230.
Chomicki, J. 2003. Preference formulas in relational queries. ACM Trans. Database Syst. 28, 4,
427–466.
Denecker, M., Bruynooghe, M., and Vennekens, J. 2012. Approximation fixpoint theory
and the semantics of logic and answers set programs. In Correct Reasoning - Essays on LogicBased AI in Honour of Vladimir Lifschitz, E. Erdem, J. Lee, Y. Lierler, and D. Pearce, Eds.
Lecture Notes in Computer Science, vol. 7265. Springer, 178–194.
Ésik, Z. 2015. Equational properties of stratified least fixed points (extended abstract). In Logic,
Language, Information, and Computation - 22nd International Workshop, WoLLIC 2015,
Bloomington, IN, USA, July 20-23, 2015, Proceedings, V. de Paiva, R. J. G. B. de Queiroz,
L. S. Moss, D. Leivant, and A. G. de Oliveira, Eds. Lecture Notes in Computer Science, vol.
9160. Springer, 174–188.
Gelder, A. V. 1989. Negation as failure using tight derivations for general logic programs. J.
Log. Program. 6, 1&2, 109–133.
Gelder, A. V., Ross, K. A., and Schlipf, J. S. 1991. The well-founded semantics for general
logic programs. J. ACM 38, 3, 620–650.
Gelfond, M. and Lifschitz, V. 1988. The stable model semantics for logic programming.
In Logic Programming, Proceedings of the Fifth International Conference and Symposium,
Seattle, Washington, August 15-19, 1988 (2 Volumes), R. A. Kowalski and K. A. Bowen, Eds.
MIT Press, 1070–1080.
Kountouriotis, V., Rondogiannis, P., and Wadge, W. W. 2005. Extensional higher-order
datalog. In Short Paper Proceedings of the 12th International Conference on Logic for Programming, Artificial Intelligence and Reasoning (LPAR). 1–5.
Lloyd, J. W. 1987. Foundations of Logic Programming. Springer Verlag.
Miller, D. and Nadathur, G. 2012. Programming with Higher-Order Logic, 1st ed. Cambridge
University Press, New York, NY, USA.
Przymusinska, H. and Przymusinski, T. 1990. Semantic issues in deductive databases and
logic programs. In Formal Techniques in Artificial Intelligence. North-Holland, 321–367.
Przymusinski, T. C. 1988. Foundations of deductive databases and logic programming. Morgan
Kaufmann Publishers Inc., San Francisco, CA, USA, Chapter On the Declarative Semantics
of Deductive Databases and Logic Programs, 193–216.
Rondogiannis, P. and Symeonidou, I. 2016. Extensional semantics for higher-order logic
programs with negation. In Logics in Artificial Intelligence - 15th European Conference,
JELIA 2016, Larnaca, Cyprus, November 9-11, 2016, Proceedings, L. Michael and A. C.
Kakas, Eds. Lecture Notes in Computer Science, vol. 10021. 447–462.
Rondogiannis, P. and Symeonidou, I. 2017. Extensional semantics for higher-order logic
programs with negation. CoRR abs/1701.08622.
Rondogiannis, P. and Wadge, W. W. 2005. Minimum model semantics for logic programs
with negation-as-failure. ACM Trans. Comput. Log. 6, 2, 441–467.
Wadge, W. W. 1991. Higher-order horn logic programming. In Logic Programming, Proceedings
of the 1991 International Symposium, San Diego, California, USA, Oct. 28 - Nov 1, 1991,
V. A. Saraswat and K. Ueda, Eds. MIT Press, 289–303.

Appendix A Proof of Theorem 1
Recall that propositional programs consist of clauses of the form p ← L1 , . . . , Ln , where
each Li is either a propositional variable or the negation of a propositional variable; the

The Intricacies of Three-Valued Extensional Semantics for Higher-Order LP

17

Li are called literals, negative if they have negation and positive otherwise. As hinted in
Section 3, we need to consider propositional programs with a possibly countably infinite
number of clauses, as this is the case with the ground instantiation of a higher-order
program. Moreover, we must allow a positive literal Li to also be one of the constants
true and false. The reason for this is that in the ground instantiation of an H program,
there may exist ground expressions of the form (E1 ≈ E2 ) in the bodies of clauses.
These have specific meanings under the semantics of Section 5 and can not be treated as
propositional variables. In the case where the two expressions E1 and E2 are syntactically
identical, the expression (E1 ≈ E2 ) will be treated as the constant true (i.e., it is assumed
that I((E1 ≈ E2 )) = true for every interpretation I of the ground instantiation), and
otherwise as the constant false.
We use, throughout all sections of the Appendix, the standard representation of partial
interpretations of propositional programs by hT, F i, where T and F are disjoint subsets of
the Herbrand base BP of a propositional program P (i.e., the set of propositional variables
appearing in P) denoting the sets of propositional variables considered to be true and
false, respectively, in the interpretation. Naturally, hT, F i is a total interpretation if
T ∪ F = BP .
The truth ordering ≤ and Fitting ordering  of interpretations can be defined in two
equivalent ways:
Definition 20
If I = hT, F i and I ′ = hT ′ , F ′ i are two partial interpretations of a propositional program
P then we say that I ≤ I ′ if T ⊆ T ′ and F ′ ⊆ F , or, equivalently, if I(p) ≤ I ′ (p) for
every propositional variable p of P. Moreover, we say that I  I ′ if T ⊆ T ′ and F ⊆ F ′ ,
or, equivalently, if I(p)  I ′ (p) for every propositional variable p of P.
A model M of a propositional program is as usual considered to be ≤-minimal (respectively, -minimal) if there does not exist a different model N of P, such that N ≤ M
(respectively, N  M ).
Theorem 1
Let P be a program and let Gr(P) be its ground instantiation. Also let M be a partial
interpretation of Gr(P) and let M be the Herbrand interpretation of P, such that vM (A) =
M (A) for every A ∈ UP,o . Then, M is a Herbrand model of P if and only if M is a model
of Gr(P). Moreover, M is ≤-minimal (respectively, -minimal) if and only if M is ≤minimal (respectively, -minimal).
Proof
Step 1 M is a model of Gr(P) ⇒ M is a Herbrand model of P: For every Herbrand
state s of P there exists a ground substitution θ such that θ(V) = s(V), and therefore
s(V) = Jθ(V)KM,s′ , for all states s′ and variables V in P. Also, for every clause A ←
L1 , . . . , Lm in P there exists a respective ground instance Aθ ← L1 θ, . . . , Lm θ in Gr(P).
As M is a model of Gr(P), M (Aθ) ≥ min{M (L1 θ), . . . , M (Lm θ)}. By assumption,
vM (Aθ) = M (Aθ) and vM (Li θ) = M (Li θ) for all i ≤ m. Moreover, it is easy to see (by
a trivial induction on the structure of the expression) that Aθ = JAKM,s , which implies
that vM (Aθ) = vM (JAKM,s ). Similarly, vM (Li θ) = vM (JLi KM,s ), for all i ≤ m. It
follows immediately that vM (JAKM,s ) ≥ min{vM (JL1 KM,s ), . . . , vM (JLm KM,s )}, which
implies that M is a model of P.

18

P. Rondogiannis and I. Symeonidou

Step 2 M is a Herbrand model of P ⇒ M is a model of Gr(P): Every clause in Gr(P)
is a ground instance of a clause A ← L1 , . . . , Lm in P and is therefore of the form
Aθ ← L1 θ, . . . , Lm θ for some ground substitution θ. Consider a Herbrand state s,
such that s(V) = θ(V) for every variable V in P. Because M is a model of P, we have
that vM (JAKM,s ) ≥ min{vM (JL1 KM,s ), . . . , vM (JLm KM,s )}. Again, it is easy to see that
Aθ = JAKM,s and therefore vM (Aθ) = vM (JAKM,s ). Similarly, vM (Li θ) = vM (JLi KM,s )
for all i ≤ m. Additionally, vM (Aθ) = M (Aθ) and vM (Li θ) = M (Li θ) for all i ≤ m, so
M (Aθ) ≥ min{M (L1 θ), . . . , M (Lm θ)}, which implies that M is a model of Gr(P).
Step 3 M is minimal ⇒ M is minimal: Assume there exists a model N of P, distinct
from M, such that N ≤ M (respectively, N  M). Then we can construct an interpretation N for Gr(P) such that for every ground atom A, N (A) = vN (A). It is obvious that
N ≤ M (respectively, N  M ), since N (A) = vN (A) ≤ vM (A) = M (A) (respectively,
vN (A)  vM (A)). Also, N is distinct from M , since N (B) = vN (B) 6= vM (B) = M (B)
for at least one ground atom B. As we showed in Step 2, the fact that N is a model
of P implies that N is a model of Gr(P), which is of course a contradiction, since M
is a ≤-minimal (respectively, -minimal) model of Gr(P). Therefore, M must be a
≤-minimal (respectively, -minimal) model of P.
Step 4 M is minimal ⇒ M is minimal: By the reverse of the argument used in Step
3: Assume there exists a model N of Gr(P), distinct from M , such that N ≤ M
(respectively, N  M ). Then we can construct an interpretation N for P such that
for every ground atom A, N (A) = vN (A). It is obvious that N ≤ M (respectively,
N  M), since vN (A) = N (A) ≤ M (A) = vM (A) (respectively, N (A)  M (A)). Also,
N is distinct from M, since their valuation functions are distinct. As we showed in
Step 1, the fact that N is a model of Gr(P) implies that N is a model of P, which is
of course a contradiction, since M is a ≤-minimal (respectively, -minimal) model of
P. Therefore, M must be a ≤-minimal (respectively, -minimal) model of Gr(P).

Appendix B Proof of Lemma 1
For the proof of Lemma 1, which we present in this appendix, we rely on the method
of (Przymusinska and Przymusinski 1990) for the construction of the well-founded model.
We first give the necessary definitions from (Przymusinska and Przymusinski 1990).
Definition 21
Let P be a propositional program and let J be an interpretation of P. The operator ΘJ (·)
on the set of interpretations of P is defined as follows: for every interpretation I and every
propositional variable p of P,


true, there exists a clause p ← L1 , . . . , Ln in P s.t. for all i ≤ n,




either J(Li ) = true or Li is a positive literal and I(Li ) = true;


ΘJ (I)(p) = false, for all clauses p ← L1 , . . . , Ln in P there exists an i ≤ n, s.t.




either J(Li ) = false or Li is a positive literal and I(Li ) = false;



0,
otherwise.

The Intricacies of Three-Valued Extensional Semantics for Higher-Order LP

19

Moreover we define the following sequence of interpretations:
Θ↑0
J
↑(n+1)
ΘJ
Θ↑ω
J

= hT0 , F0 i = h∅, BP i
= hTn+1 , Fn+1 i = ΘJ (Θ↑n
JT)
S
= hTω , Fω i = h n<ω Tβ , n<ω Fβ i

It is shown in (Przymusinska and Przymusinski 1990) that, for any interpretation J, the
operator ΘJ has a unique least fixed-point given by Θ↑ω
J .
Definition 22
Let P be a propositional program. For every countable ordinal α ≤ γ, we define the
interpretation Mα as follows:
M0
Mα+1
Mα

= hT0 , F0 i = h∅, ∅i
= hTα+1 , Fα+1 i = Θ↑ω
for a successor ordinal α + 1
Mα , S
S
= hTα , Fα i = h β<α Tβ , β<α Fβ i, for a limit ordinal α

Again from (Przymusinska and Przymusinski 1990), there exists the least countable ordinal λ, such that Mλ = Θ↑ω
Mλ and Mλ coincides with the well-founded model MP of the
propositional program P.
We now present the proof of Lemma 1.
Lemma 1
The Herbrand interpretation MP of the program of Example 4 is not extensional.
Proof
We repeat here the program of Example 4 for the reader’s convenience:
s
p
q
w

Q
R
R
R

←
←
←
←

Q (s Q)
R
∼(w R)
∼R

Recall that the predicate variable Q is of type o → o and the predicate variable R is of
type o. The ground instantiation of the above program is infinite, as so:
s p ← p (s p)
s q ← q (s q)
s w ← w (s w)
p (s p) ← (s p)
p (s q) ← (s q)
p (s w) ← (s w)
q (s p) ← ∼(w (s p))
w (s p) ← ∼(s p)
q (s q) ← ∼(w (s q))
w (s q) ← ∼(s q)
q (s w) ← ∼(w (s w))
w (s w) ← ∼(s w)
...
The well-founded model MGr(P) of the above (infinite) propositional program is the valuation function of MP . It has already been argued in Section 6 and Section 8, that

20

P. Rondogiannis and I. Symeonidou

MGr(P) (s p) 6= MGr(P) (s q) and this should be obvious to the reader who is familiar
with the well-founded model semantics; however, for reasons of completeness, we present
a formal argument in the second part of this proof. In the same sections, we claimed
that this is despite the fact that p ∼
=MGr(P) ,o→o q, which we will immediately proceed to
prove. Of course, by Definitions 17 and 18, the facts that MGr(P) (s p) 6= MGr(P) (s q) and
p∼
=MGr(P) ,o→o q, render MP not extensional.
∼M ,o→o q, i.e. that for all A, A′ ∈ UP,o such that A =
∼M ,o A′ ,
First, we show that p =
Gr(P)
Gr(P)
p A∼
=MGr(P) ,o q A′ holds. By definition MGr(P) is a fixed-point of the operator ΘMGr(P) (·),
therefore for any ground atom B we have that MGr(P) (B) equals to true, if there exists a clause B ← L1 , . . . , Ln in Gr(P), such that MGr(P) (Li ) = true for all i ≤ n; it
equals to false if for every clause B ← L1 , . . . , Ln in Gr(P), we have that MGr(P) (Li ) =
false for at least one i ≤ n; and it equals to 0 otherwise. Observe that there exists only one clause in Gr(P) such that p A is the head of the clause, in particular
it is the ground instance p A ← A of the clause p R ← R of P. This suggests that
MGr(P) (p A) = MGr(P) (A) (1). Similarly, the ground instance q A′ ← ∼(w A′ ) of the
clause q R ← ∼(w R) is the only clause in Gr(P) with q A′ as its head atom and from
this we can infer that MGr(P) (q A′ ) = MGr(P) (∼(w A′ )) = ¬MGr(P) (w A′ ) (2). Finally,
the only clause in Gr(P), such that w A′ is the head of the clause, is the ground instance w A′ ← ∼A′ of the clause w R ← ∼R of P, which implies that MGr(P) (w A′ ) =
MGr(P) (∼A′ ) = ¬MGr(P) (A′ ) (3). By (2) and (3) we have MGr(P) (q A′ ) = MGr(P) (A′ ), and,
in conjunction with (1), that MGr(P) (p A) = MGr(P) (q A′ ), because A ∼
=MGr(P) ,o A′ implies,
′
by Definition 17, that MGr(P) (A) = MGr(P) (A ). Therefore, we also have p A ∼
=MGr(P) ,o q A′
∼
and, in consequence, p =MGr(P) ,o→o q.
For the second part, we show that MGr(P) (s p) 6= MGr(P) (s q). We do this in two steps;
first we show that MGr(P) (s p) = false and then that MGr(P) (s q) = 0.
For the first step, it suffices to show that M1 (s p) = Θ↑ω
M0 (s p) = false. For this, we
↑n
prove that Θ↑n
(s
p)
=
false
and
Θ
(p
(s
p))
=
false,
for
all n < ω, by an induction
M0
M0
↑0
on n. The basis case is trivial, as ΘM0 = h∅, UP,o i, assigns the value false to every atom.
For the induction step, we show the statement for n + 1 assuming that it holds for n.
We see that there exists only one clause in Gr(P) such that s p is the head of the clause;
this is the ground instance s p ← p (s p) of the clause s Q ← Q (s Q) of P. By the
↑(n+1)
induction hypothesis, we have that Θ↑n
(s p) =
M0 (p (s p)) = false, therefore ΘM0
false. Similarly, the only clause in Gr(P) with p (s p) as the head of the clause is
the ground instance p (s p) ← (s p) of the clause p R ← R of P. By the induction
↑(n+1)
hypothesis, we have that Θ↑n
(p (s p)) = false.
M0 (s p) = false, therefore ΘM0
For the second step, we perform an induction on α, during which we simultaneously
show that Mα (s q) = 0, Mα (q (s q)) = 0 and Mα (w (s q)) = 0, for all countable
ordinals α. The basis case is trivial, as M0 = h∅, ∅i assigns the value 0 to all atoms. For
the induction step, we first prove the statement for a successor ordinal α+1, assuming that
it holds for all countable ordinals up to α. Indeed, there exists exactly one clause in Gr(P)
with w (s q) as its head atom, in particular the ground instance w (s q) ← ∼(s q)
of the clause q R ← ∼(w R). As ∼(s q) is a negative literal, for every n < ω the
↑(n+1)
value of ΘMα (w (s q)) is defined by Mα (∼(s q)). By the induction hypothesis, we
↑(n+1)

have Mα (s q) = Mα (∼(s q)) = 0, therefore it follows that ΘMα (w (s q)) = 0 and,
because this holds for every n < ω, that Mα+1 (w (s q)) = 0. Moreover, the ground

The Intricacies of Three-Valued Extensional Semantics for Higher-Order LP

21

instance q (s q) ← ∼(w (s q)) of the clause q R ← ∼(w R) is the only clause in
Gr(P) with q (s q) as its head atom. Again, ∼(w (s q)) is a negative literal and so
↑(n+1)
for every n < ω the value of ΘMα (q (s q)) only depends on Mα (∼(w (s q))). By
the induction hypothesis, we have Mα (w (s q)) = Mα (∼(w (s q))) = 0, therefore
↑(n+1)
it follows that ΘMα (q (s q)) = 0. Since this holds for every n < ω, we also have
that Mα+1 (q (s q)) = 0. Finally, there exists only one clause in Gr(P) such that s
q is the head of the clause, in particular the ground instance s q ← q (s q) of the
↑(n+1)
clause s Q ← Q (s Q) of P. We have already shown that ΘMα (q (s q)) = 0 for all
n < ω; moreover, by the induction hypothesis, Mα (q (s q)) = 0. Consequently, for all
↑(n+2)
n < ω, ΘMα (s q) = 0 and thus Mα+1 (s q) = 0. It remains to show Mα (s q) = 0,
Mα (q (s q)) = 0 and Mα (w (s q)) = 0 for a limit ordinal α. In this case, we have that
S
S
Mα = h β<α Tβ , β<α Fβ i. By the induction hypothesis, Mβ (s q) = 0 for all β < α,
S
which means that s q 6∈ Tβ and s q 6∈ Fβ . In other words, s q 6∈ β<α Tβ and s q 6∈
S
β<α Fβ , therefore Mα (s q) = 0. In the same way we can show that Mα (q (s q)) =
0 and Mα (w (s q)) = 0. This concludes the induction and so we have proven that
MGr(P) (s q) = 0.

Appendix C Proof of Theorem 2
Before we proceed with the proof of Theorem 2, we recall some necessary definitions. Note
that the proof makes use of a fixed-point characterization of the perfect model semantics
given in (Przymusinska and Przymusinski 1990), rather than the more traditional definition of (Przymusinski 1988). The following definition of the local stratification of possibly
infinite propositional programs is adapted to allow for the presence of expressions of the
form (E1 ≈ E2 ).
Definition 23
A propositional program P is called locally stratified if and only if it is possible to decompose the Herbrand base BP of P into disjoint sets (called strata) S1 , S2 , . . . , Sα , . . . , α < γ,
where γ is a countable ordinal, such that for every clause H ← A1 , . . . , Am , ∼B1 , . . . , ∼Bn
in P, we have that for every i ≤ m, stratum(Ai ) ≤ stratum(H) and for every i ≤ n,
stratum(Bi ) < stratum(H), where stratum is a function such that stratum(C) = β, if the
propositional variable C ∈ BP belongs to Sβ and stratum(C) = 0, if C 6∈ BP and is a
constant (equivalently, of the form (E1 ≈ E2 )). Any decomposition of the described form
is called a local stratification of P.
In (Przymusinska and Przymusinski 1990), for any interpretation J, the operator ΨJ is
defined and shown to have a unique least fixed-point given by Ψ↑ω
J of the next definition.
This is then used to give an iterated fixed-point characterization of the perfect model of
a locally stratified program.
Definition 24
Let P be a propositional program and let J be an interpretation of P. The operator ΨJ : 2BP → 2BP is defined as follows: for every I ⊆ BP , ΨJ (I) = {p ∈ BP |
there exists a clause p ← L1 , . . . , Ln in P such that, for all i ≤ n, either J(Li ) = true or

22

P. Rondogiannis and I. Symeonidou

Li ∈ I}. Moreover we define the following sequence:
Ψ↑0
J
↑(n+1)
ΨJ
Ψ↑ω
J

=
=
=

∅
ΨJ (Ψ↑n
J )
S
↑n
n<ω ΨJ

We follow the usual convention of identifying a subset of the Herbrand base with a total
(two-valued) interpretation of the program and use the two notions interchangeably.
E.g., a set Ψ↑n
J of the above sequence is considered to be equivalent to the interpretation
↑n
↑n
↑n
hΨ↑n
J , BP − ΨJ i and p ∈ ΨJ is considered to be equivalent to ΨJ (p) = true.
Given a local stratification S1 , S2 , . . . , Sα , . . ., α < γ, of a propositional program P, we
S
define the sets Bα = β<α Sβ for every countable ordinal α ≤ γ. Clearly, BP = Bγ . Then
the perfect model of P can be constructed (Przymusinska and Przymusinski 1990) as the
last interpretation Nγ in an -increasing sequence of partial interpretations of P:
Definition 25
Let P be a propositional program and let S1 , S2 , . . . , Sα , . . . , α < γ, where γ is a countable
ordinal, be a local stratification of P. For every countable ordinal α ≤ γ, we define the
interpretation Nα as follows:
N0
Nα+1
Nα

=
=
=

hT0 , F0 i = h∅, ∅i
hTα+1 , Fα+1 i = hΨ↑ω
Bα+1 − Ψ↑ω
Nα ,S
Nα i, for a successor ordinal α + 1
S
hTα , Fα i = h β<α Tβ , β<α Fβ i, for a limit ordinal α

Theorem 3 (Przymusinska and Przymusinski 1990)
Let P be a propositional program. The sequence N0 , N1 , . . . , Nα , . . . , Nγ is -increasing.
Moreover, Nγ coincides with the perfect model NP of P.
The next lemma and its following corollary are the basis for our proof of Theorem 2.
Lemma 2
Let P be an H program. If P is stratified then the ground instantiation Gr(P) of P is
locally stratified.
Proof
Consider a decomposition S1 , . . . , Sr of the set of predicate constants of P such that the
requirements of Definition 19 are satisfied. This defines a decomposition S1′ , . . . , Sr′ of
UP,o , which is also the Herbrand base of Gr(P), as follows:
Si′ = {A ∈ UP,o | the leftmost predicate constant of A belongs to Si }
It is easy to check that S1′ , . . . , Sr′ corresponds to a local stratification of Gr(P).
An immediate result of the above lemma is that the model NP can be defined for every
stratified program of H:
Corollary 1
Let P be an H program. If P is stratified, then the perfect model NP of P exists and
coincides with its well-founded model MP .

The Intricacies of Three-Valued Extensional Semantics for Higher-Order LP

23

Proof
By Lemma 2, if P is stratified then Gr(P) is locally stratified. Therefore the unique
perfect model NGr(P) of Gr(P) exists (Przymusinski 1988) and NP is defined. Moreover,
the perfect model of a locally stratified propositional program, which is the valuation
function of NP , coincides with its well-founded model MGr(P) (Przymusinski 1988), i.e.
the valuation function of MP . In other words, in this case NP and MP coincide, because
they have the same valuation function.
Theorem 2
The well-founded model MP of a stratified program P is extensional.
Proof
By Corollary 1, if P is stratified then MP coincides with NP . Therefore, it suffices to
show that NP is extensional and for this we rely upon the constructive definition of
NGr(P) from (Przymusinska and Przymusinski 1990) presented above.
Consider a stratification S1 , . . . , Sr of the set of predicate constants of P. As argued in
the proof of Lemma 2, the following decomposition S1′ , . . . , Sr′ of UP,o :
Si′ = {A ∈ UP,o | the leftmost predicate constant of A belongs to Si }
corresponds to a local stratification of Gr(P). Therefore, whenever a ground atom A
begins with a predicate constant p, we will have stratum(A) = stratum(p). Moreover,
by Theorem 3, NGr(P) = Nr .
Since the valuation function of NP is NGr(P) , essentially we need to show that E ∼
=NGr(P) ,ρ
E, for every ground expression E of every argument type ρ. We perform an induction on
the structure of ρ. For the base types ι and o the statement holds by definition. For the
induction step, we prove the statement for a predicate type π = ρ1 → · · · → ρm → o,
assuming that it holds for all types simpler than π (i.e., for the types ρ1 , . . . , ρm , o and,
recursively, the types that are simpler than ρ1 , . . . , ρm ). Let A be any atom of the following
form: A is headed by a predicate constant p and all variables in vars(A) are of types
simpler than π. Let θ, θ′ be ground substitutions, such that vars(A) ⊆ dom(θ), dom(θ′ )
and θ(V) ∼
=NGr(P) ,ρ θ′ (V) for any V : ρ in vars(A). We claim it suffices to show the following
two properties P1 (α) and P2 (α), for all finite ordinals (i.e., natural numbers) α:
P1 (α): If Nα (Aθ) = true then NGr(P) (Aθ′ ) = true.
P2 (α): If Nα (Aθ) = false then NGr(P) (Aθ′ ) = false.
To see why proving the above properties is enough to establish that E ∼
=NGr(P) ,π E, observe
the following: first of all, we assumed that π is of the form ρ1 → · · · → ρm → o, so if
V1 : ρ1 , . . . , Vm : ρm are variables, then E V1 · · · Vm is an atom of the form described
above. As NGr(P) = Nr , if NGr(P) (E θ(V1 ) · · · θ(Vm )) = Nr (E θ(V1 ) · · · θ(Vm )) = true and
property P1 (r) holds, then we can infer that NGr(P) (E θ′ (V1 ) · · · θ′ (Vm )) = true. Because
the relations ∼
=NGr(P) ,ρi are symmetric, θ and θ′ are interchangeable. Therefore the same
argument can be used to infer the reverse implication, i.e. NGr(P) (E θ′ (V1 ) · · · θ′ (Vm )) =
true ⇒ NGr(P) (E θ(V1 ) · · · θ(Vm )) = true, thus resulting to an equivalence. If P2 (r) holds,
the analogous equivalence can be shown for the value false in the same way and so it
follows that E ∼
=NGr(P) ,π E. Finally, r is determined by the stratification of the higher-order

24

P. Rondogiannis and I. Symeonidou

program and is therefore finite, so we only need to prove properties P1 (α) and P2 (α) for
finite ordinals.
We will proceed by a second induction on α.
Second Induction Basis (α = 0) We have N0 = h∅, ∅i. As this interpretation does
not assign the value true or the value false to any atom, both properties P1 (0) and P2 (0)
hold vacuously.
Second Induction Step (α + 1) We first show P1 (α + 1). We have that Nα+1 =
↑ω
↑ω
hΨ↑ω
Nα , Bα+1 − ΨNα i; observe that ΨNα (Aθ) = true if and only if there exists some n < ω
for which Ψ↑n
Nα (Aθ) = true. Therefore, in order to prove P1 (α + 1), we first need to
perform a third induction on n and prove the following property:
′
P1′ (α + 1, n): If Ψ↑n
Nα (Aθ) = true then NGr(P) (Aθ ) = true.

Third Induction Basis (n = 0) Property P1′ (α+1, 0) holds vacuously, since Ψ↑0
Mα = ∅,
i.e. it does not assign the value true to any atom.
Third Induction Step (n+ 1) We now show property P1′ (α+ 1, n+ 1), assuming that
↑(n+1)
P1′ (α + 1, n) holds. If ΨNα (Aθ) = true, then there exists a clause Aθ ← L1 , . . . , Lk in
Gr(P) such that, for each i ≤ k, either Nα (Li ) = true or Li is an atom and Ψ↑n
Nα (Li ) = true.
This clause is a ground instance of a clause p V1 · · · Vm ← K1 , . . . , Kk in the higher-order
program and there exists a substitution θ′′ , such that (p V1 · · · Vm )θ′′ = A and, for any
variable V 6∈ {V1 , . . . , Vm } appearing in the body of the clause, θ′′ (V) is an appropriate
ground term, so that Li = Ki θ′′ θ for all i ≤ k. Observe that the variables appearing in
the clause (p V1 · · · Vm )θ′′ ← K1 θ′′ , . . . , Kk θ′′ are exactly the variables appearing in A
and they are all of types simpler than π. We distinguish the following cases for each Ki θ′′ ,
i ≤ k:
1. Ki θ′′ is of the form (E1 ≈ E2 ): As remarked in Appendix A, an expression of the form
′′
(E1 ≈ E2 ) has the same value in any interpretation. If Nα (Ki θ′′ θ) = Ψ↑n
Nα (Ki θ θ) = true,
by definition we have E1 θ = E2 θ. Since E1 and E2 are expressions of type ι, all variables
in E1 and E2 are also of type ι and, because ∼
=NGr(P) ,ι is defined as equality, we will have
′
′
′
E1 θ = E1 θ and E2 θ = E2 θ . Therefore E1 θ = E2 θ′ and NGr(P) (Ki θ′′ θ′ ) = true will also
hold.
2. Ki θ′′ is an atom and starts with a predicate constant: As we observed, the variables
appearing in Ki θ′′ are of types simpler than π. Because Ki θ′′ θ is an atom, either Nα (Li ) =
↑n
′′
Nα (Ki θ′′ θ) = true or Ψ↑n
Nα (Li ) = ΨNα (Ki θ θ) = true may hold. In the former case,
by the second induction hypothesis we can apply property P1 (α) and it follows that
NGr(P) (Ki θ′′ θ′ ) = true. Similarly, in the latter case, the same conclusion can be reached
by the third induction hypothesis and property P1′ (α + 1, n).
3. Ki θ′′ is an atom and starts with a predicate variable: As in the previous case, it may be
↑n
′′
′′
Nα (Li ) = Nα (Ki θ′′ θ) = true or Ψ↑n
Nα (Li ) = ΨNα (Ki θ θ) = true. Let Ki θ = V E1 · · · Em′
for some V ∈ vars(A). Then B = θ(V) E1 · · · Em′ is an atom that begins with a predicate
constant and, by vars(Ki θ′′ ) ⊆ vars(A), all of the variables of B are of types simpler
than π. Hence, by the second induction hypothesis, B satisfies property P1 (α) and if
Nα (Ki θ′′ θ) = Nα (Bθ) = true then it follows that NGr(P) (Bθ′ ) = true (1). Similarly, by
′′
the third induction hypothesis, B also satisfies property P1′ (α + 1, n), so if Ψ↑n
Nα (Ki θ θ) =
′
Ψ↑n
Nα (Bθ) = true, then the same conclusion, that NGr(P) (Bθ ) = true (1), is reached
again. Observe that the types of all arguments of θ(V), i.e. the types of Ej θ′ for all

The Intricacies of Three-Valued Extensional Semantics for Higher-Order LP

25

j ≤ m′ , are simpler than the type of V and consequently, since V ∈ vars(A), simpler
than π. For each j ≤ m′ , let ρj be the type of Ej and let ρ be the type of V; by
the first induction hypothesis, Ej θ′ ∼
=NGr(P) ,ρj Ej θ′ . Moreover, by assumption we have
′
∼
that θ(V) =NGr(P) ,ρ θ (V). Then, by definition and by (1) NGr(P) (θ(V) E1 θ′ · · · Em′ θ′ ) =
NGr(P) (θ′ (V) E1 θ′ · · · Em′ θ′ ) = NGr(P) (Ki θ′′ θ′ ) = true.
4. Ki θ′′ is a negative literal and its atom starts with a predicate constant: Let Ki θ′′ be of
the form ∼B, where B is an atom that starts with a predicate constant. It is Nα (∼Bθ) =
Nα (Ki θ′′ θ) = Nα (Li ) = true and therefore Nα (Bθ) = false. Moreover, by vars(Ki θ′′ ) ⊆
vars(A), all the variables of B are of types simpler than π, so we can apply the second
induction hypothesis, in particular property P2 (α), to B and conclude that NGr(P) (Bθ′ ) =
false. Then NGr(P) (∼Bθ′ ) = NGr(P) (Ki θ′′ θ′ ) = true.
5. Ki θ′′ is a negative literal and its atom starts with a predicate variable: Let Ki θ′′ =
∼(V E1 · · · Em′ ) for some V ∈ vars(A). Then B = θ(V) E1 · · · Em′ is an atom that begins
with a predicate constant and, by vars(Ki θ′′ ) ⊆ vars(A), all of the variables of B are
of types simpler than π. Also, Nα (∼Bθ) = Nα (Ki θ′′ θ) = Nα (Li ) = true and therefore
Nα (Bθ) = false. Hence, by the second induction hypothesis and in particular property
P2 (α), it follows that NGr(P) (Bθ′ ) = NGr(P) (θ(V) E1 θ′ · · · Em′ θ′ ) = false (1). Observe that
the types of all arguments of θ(V), i.e. the types of Ej θ′ for all j ≤ m′ , are simpler than
the type of V and consequently, since V ∈ vars(A), simpler than π. For each j ≤ m′ ,
let ρj be the type of Ej and let ρ be the type of V; by the first induction hypothesis,
Ej θ ′ ∼
=NGr(P) ,ρ θ′ (V). Then, by
=NGr(P) ,ρj Ej θ′ . Moreover, by assumption we have that θ(V) ∼
definition and by (1), NGr(P) (θ(V) E1 θ′ · · · Em′ θ′ ) = NGr(P) (θ′ (V) E1 θ′ · · · Em′ θ′ ) = false.
Obviously, this makes NGr(P) (∼(θ′ (V) E1 θ′ · · · Em′ θ′ )) = NGr(P) (Ki θ′′ θ′ ) = true.
We have shown that, for each i ≤ k, NGr(P) (Ki θ′′ θ′ ) = true. Since the clause Aθ′ ←
K1 θ′′ θ′ , . . . , Kk θ′′ θ′ is in Gr(P) and NGr(P) is a model of Gr(P), we can conclude that
NGr(P) (Aθ′ ) = true.
This concludes the proof for P1′ (α+1, n). Notice that property P1′ (α+1, n) immediately
implies property P1 (α+1): as mentioned before, Nα+1 (Aθ) = Ψ↑ω
Nα (Aθ) = true if and only
↑n
if there exists some n < ω for which ΨNα (Aθ) = true and then NGr(P) (Aθ′ ) = true follows
from property P1′ (α+1, n). It remains to prove property P2 (α+1). Observe that the atoms
Aθ and Aθ′ both start with the same predicate constant p and recall that we have chosen
a local stratification for Gr(P), such that stratum(Aθ) = stratum(Aθ′ ) = stratum(p).
↑ω
Moreover, we have that Nα+1 = hΨ↑ω
Nα , Bα+1 − ΨNα i, so if Nα+1 (Aθ) = false, it follows
that Aθ ∈ Bα+1 . Because stratum(Aθ) = stratum(Aθ′ ), it must also be Aθ′ ∈ Bα+1 ,
↑ω
′
which implies that Nα+1 (Aθ′ ) can be either true (if Aθ′ ∈ Ψ↑ω
Nα ) or false (if Aθ 6∈ ΨNα ),
but not 0. For the sake of contradiction, assume that Nα+1 (Aθ′ ) = true. As the relations
∼
=NGr(P) ,ρi are symmetric, θ and θ′ are interchangeable, so property P1 (α + 1) applies and
yields NGr(P) (Aθ) = true. Because (by Theorem 3) Nα+1  NGr(P) , this contradicts our
initial assumption that Nα+1 (Aθ) = false. Therefore, it must be Nα+1 (Aθ′ ) = false and
so, again by Nα+1  NGr(P) , it follows that NGr(P) (Aθ′ ) = false.

