FQHT: The Logic of Stable Models for Logic Programs with Intensional Functions

1 Introduction

In action theories and commonsense reasoning one frequently deals with so-called non-Boolean fluents that are subject to inertia laws. For example, we may have a fluent loc that refers to spatial location and we may want to say that by default (unless moved) a block b does not change its location from one moment to the next. A convenient way to represent this is to treat loc as a function taking objects and time points as arguments. And a natural way to express the inertia law would be to use a formula such as

where '¬' is default negation; with the intention to express that by default the location of a block b does not change from time t to t + 1.

In answer set programming (ASP) and in many nonmonotonic theories (1) does not adequately capture the inertia law. In ASP for example, if ¬(loc(b, t + 1) ̸= l) is viewed as an abbreviation of ¬¬(loc(b, t+1) = l), then (1) is trivially true by logic. The problem, it seems, arises due to the way that functions and equality are treated in such formalisms. 1

∗Partially supported by the French-Spanish Laboratoire Europ´een Associ´e (LEA) "French-Spanish lab of Advanced Studies in Information Representation and Processing"

†Partially supported by MEC projects TIN2009-14562-C05 and CSD2007-00022.

‡Partially supported by MEC projects TIN2012-39353-C04 and TIN2009-14562-C05 and Junta de Andaluc´ıa projects P09-FQM5233 and TIC115

1 Notice that in the underlying logic we do not have ϕ ≡ ¬¬ϕ.

Agust´ın Valverde‡

Universidad de M´alaga, SP a valverde@ctima.uma.es

In ASP for example there have been different proposals for treating functions. Functions and equality were already included in versions of equilibrium logic proposed as a foundation for logic programs with variables under the stable model semantics [Pearce and Valverde, 2005; Lifschitz et al., 2007]. In the latter case the underlying logic is denoted by SQHT=. It is a quantified version of the logic of hereand-there, based on static (or constant) domains and decidable equality. 2 Another approach is to build a theory of partial functions for ASP; this idea was developed by [Cabalar, 2008; 2011] and [Balduccini, 2012]. Alternatively [Lin and Wang, 2008] works with a new notion of reduct involving manysorted functions.

In this paper, however, we want to consider more recent approaches that treat non-Boolean fluents as intensional functions and allow one to write expressions such as (1). One proposal is by [Lifschitz, 2012] who introduced IF-programs or logic programs with intensional functions that are closely related to causal logic programs. An alternative approach has been suggested by [Bartholomew and Lee, 2012]. This is also intended to capture non-Boolean fluents but is closer in spirit to the usual stable model semantics. It is also a more general framework that applies to first-order theories and allows one to treat also intensional predicates. The authors show how their semantical framework has several applications and enjoys good metatheoretical properties. For instance they show how to capture multi-valued propositional formulas used in nonmonotonic causal theories by [Giunchiglia et al., 2004], they show how to eliminate intensional predicates using intensional functions (and vice versa), and they establish a splitting theorem and a relation to Clark's completion.

Both approaches to intensional functions use a variant of the SM operator first described in [Ferraris et al., 2007]; this defines stable models via a second-order condition. The question arises whether intensional functions can also be understood in terms of preferred models of an underlying (firstorder) monotonic logic, in the same way that ordinary stable models can be understood as preferred or minimal models in the logic QHT of here-and-there [Pearce and Valverde, 2005]. A partial and positive answer to this question for the case of IF-programs is given in [Fari ˜nas del Cerro et al., 2012] where it is proved that the propositional version of a system called bi-state logic is adequate for dealing with the approach of [Lifschitz, 2012]. It turns out however that Lifschitz's semantics is not such a close fit to the usual stable model semantics and the underlying logics of the two semantics diverge considerably. Our aim now is to show how using a new variant of QHT we can define an extended notion of equilibrium model that serves as a logical foundation for theories with intensional functions under the semantics of [Bartholomew and Lee, 2012]. We give a Gentzen style proof theory and establish completeness results for the new logic. The adequacy of the approach is demonstrated by showing how it captures the semantics of Bartholemew and Lee and satisfies a strong equivalence property.

2 [Lifschitz et al., 2007] does not explicitly treat function symbols, but in other respects the logic is similar to that of [Pearce and Valverde, 2005]

2 Flexible Quantified Here-and-There logic

We consider a first-order language with constants, functions and equality, L = 〈C, F, P ∪{=}〉, where C is the set of constants, F is the set of function symbols, each with an assigned arity, and P is the set of predicate symbols, each with an assigned arity. Moreover, we assume a countably infinite set of variables, the constant ⊥, the connectives, '∨', '∧', '→', '∃', '∀' and auxiliary parentheses; we will also consider the negation defined from implication by ¬ϕ := ϕ → ⊥ and the biimplication defined by ϕ ↔ ψ := (ϕ → ψ) ∧ (ψ → ϕ). We are going to work only with closed formulas or sentences (those where each variable is bound by some quantifier). A set of sentences is called a theory. We will denote by At = At(C, F, P) the set of ground atoms over the language without equality.

A first order structure for L is a pair (D, I) where D is a non-empty set, the domain of the structure, and I is a mapping such that: I(a) ∈ D for every a ∈ C; I(d) = d for every d ∈ D; if n is the arity of f ∈ F, I(f) : Dn →D; if n is the arity of p ∈ P , I(p) ⊆ Dn . The mapping I is extended recursively to the set of terms over the signature 〈C ∪D, F〉 in the usual way.

We adopt a possible worlds semantics with constant domains and non-rigid constants and functions. 3 A Flexible Quantified HT-interpretation, in short FQHTinterpretation, is a pair I = 〈I h , I t 〉, where (D, I h ) and (D, I t ) are first order structures over the same domain D, such that I h (p) ⊆ I t (p) for every p ∈ P .

The satisfaction relation between an FQHT-interpretation I = 〈I h , I t 〉, a world w ∈ {h, t} and a formula ϕ, is defined recursively:

• I,w ̸|= ⊥
• I, h |= p(s1, . . . , sn) iff (I h (s1), . . . , I h (sn)) ∈ I h (p) and (I t (s1), . . . , I t (sn)) ∈ I h (p)
• I, t |= p(s1, . . . , sn) iff (I t (s1), . . . , I t (sn)) ∈ I t (p).
• I, h |= s1 = s2 iff I h (s1) = I h (s2), I t (s1) = I t (s2).
• I, t |= s1 = s2 iff I t (s1) = I t (s2).
• I,w |= ϕ∧ψ if I,w |= ϕ and I,w |= ψ,

3 There are just two 'worlds', denoted by 'h' and 't'.

• I,w |= ϕ∨ψ if I,w |= ϕ or I,w |= ψ,

• I, t |= ϕ → ψ if, either I, t ̸|= ϕ or I, t |= ψ,
• I,w |= ∀xϕ(x) iff I,w |= ϕ(d) for all d ∈ D.
• I,w |= ∃xϕ(x) iff I,w |= ϕ(d) for some d ∈ D.

The concepts of validity, equivalence and semantic consequence are defined in the same way as for propositional HTlogic: we write I |= ϕ if I, h |= ϕ and I, t |= ϕ; in such a case, we say that I satisfies ϕ or I is a model of ϕ. A formula ϕ is valid, in symbols |= ϕ, if every interpretation is a model of ϕ; this defines flexible quantified here-and-there logic, denoted by FQHT. Two formulas ϕ and ψ are said to be equivalent if ϕ ↔ ψ is valid; equivalently, two formulas ϕ and ψ are equivalent if and only if they have the same FQHT-models. For any set Γ of formulas and any formula ϕ, we write Γ |= ϕ if for every FQHT-interpretation I and every world w we have: I, w |= Γ implies I, w |= ϕ.

There are two main differences with respect to the usual logic QHT of here-and-there. In the latter, constants and functions take the same value at the two points h and t, whereas in FQHT constants and those functions we shall call intensional are non-rigid and can be interpreted differently in the two worlds. A second important difference compared to the usual possible worlds semantics can be seen in the atomic case. Suppose for simplicity that q is a monadic predicate and s is a term. In order to verify that the formula q(s) is satisfied at the point h we need to check not only that q is true for the object that interprets s at h but also for the t-interpretation of s which might be different. This condition is needed to ensure that a formula true at h remains true at t. These differences in the semantics create an obvious difference with respect to the treatment of equality. For example the formula ∀x(x = a ∨ ¬(x = a)) is valid in QHT, but not in FQHT.

3 Equilibrium in FQHT and Intensional Functions

If I is a classical model of a formula ϕ (over a domain D) then, trivially, 〈I, I〉 is an FQHT-model of ϕ; and vice versa, if 〈I, I〉 is an FQHT-model of ϕ, then I is a classical model of ϕ. We will call these kinds of models total models.

We can now introduce a notion of equilibrium model for FQHT. that allows us to define a non-monotonic logic based on FQHT and obtain a characterization of the semantics of programs with intensional functions of Bartholomew and Lee.

Definition 1 Let Π be a theory. A total FQHT-model of Π, 〈I, I〉, is said to be an equilibrium model of Π if there does not exist another model 〈J, I〉 of Π such that J ̸= I.

In [Bartholomew and Lee, 2012], the authors present a new semantics for logic programs using second order formulas. For predicate symbols (constants or variables) u and c, u ≤ c stands for ∀x(u(x) → c(x)) and u = c stands for ∀x(u(x)↔c(x)); if u and c are function symbols, u = c stands for ∀x(u(x) = c(x)). If c = p1 . . . pnf1 . . . fma1 . . . ak is the list of predicates, function and constant symbols in ϕ, and ̂c = ̂ p1 . . . ̂ pn ̂ f1 . . . ̂ fm̂a1 . . . ̂ak is a list of variables of predicates, function and constant symbol such that the arity of pi is equal to the arity of ̂ pi for every i, and the arity of fi is equal to the arity of ̂ fi, then we define the second order formula SM[ϕ], which is used to provide a new concept of stable model, as follows:

where: ̂c < c stands for the conjunction of the formulas ̂c ≤ c for every predicate symbol c and ¬(̂c = c) for every predicate, constant and function symbol c; and ϕ∗ [c/̂c] is defined as follows:

• If ϕ is atomic, ϕ∗ [c/̂c] = ϕ′ ∧ ϕ, where ϕ′ is obtained by replacing every predicate, function and constant with the corresponding variables.
• (ϕ∧ψ)∗ = ϕ∗ ∧ψ∗ , (ϕ∨ψ)∗ = ϕ∗ ∨ψ∗ ,
• (ϕ→ψ)∗ = (ϕ∗ →ψ∗ ) ∧ (ϕ→ψ),
• (∀xϕ)∗ = ∀xϕ∗ , (∃xϕ)∗ = ∃xϕ∗ .

In fact, [Bartholomew and Lee, 2012] introduces the formula SM[ϕ; c] where the list c might not contain all the symbols in ϕ, but only those constants that are considered intensional. We will consider later this general case.

Theorem 1 The interpretation I is a model of SM[ϕ] iff 〈I, I〉 is an equilibrium model of ϕ.

Proof:

• (⇒) Let us assume that the interpretation I over the domain D is a model of SM[ϕ]; trivially, I is a model of ϕ. Let us suppose that 〈I, I〉 is not in equilibrium; then there exists another interpretation J over the same domain such that J ̸= I and 〈J, I〉 |= ϕ.

Let us consider the sets C ′ = {a′ | c ∈ C}, F ′ = {f ′ | f ∈ F}, P ′ = {p′ | P ∈ C}. For every α ∈ At(C ∪D, F, P), α′ ∈ At(C ′ ∪D, F ′ , P ′ ) is the formula obtained by replacing every element c ∈ C ∪F ∪P, by c′ . Let us consider the extension I, of the interpretation I, to the language build over the atoms in At(C, F, P) ∪ At(C ′ , F ′ , P ′ ), defined as follows: for every c ∈ C ∪ F ∪ P

It is easy to prove by induction that I(ϕ∗ [c/c′ ]) = 1 iff 〈J, I〉, h |= ϕ, and therefore, I(ϕ∗ [c/c′ ]) = 1. On the other hand, I(c′ < c) = 1, because J ̸= I, and thus:

which contradicts the assumption that I is a model of SM[ϕ].

(⇐) The other direction is analogous.

This result may be extended to characterize the general notion of stable model introduced in [Bartholomew and Lee, 2012] with the formula SM[ϕ; c], where c is a list of symbols in ϕ. In the following statement we need the following formulas: if a ∈ C, then δa = ∀x(x = a ∨ ¬(x = a)); if f ∈ F, then δf = ∀x∀y(x = f(y) ∨ ¬(x = f(y))); and if p ∈ P , then δp = ∀x(p(x) ∨ ¬p(x)).

Corollary 1 Let c be a list of constant symbols occurring in ϕ. Then the interpretation I is a model of SM[ϕ; c] iff 〈I, I〉 is an equilibrium model of

3.1 Strong equivalence

FQHT logic also allows us to characterize the strong equivalence concept associated with equilibrium models.

Definition 2 Two sets of formulas, Π1 and Π2 are said to be strongly equivalent if, for every set of formulas ∆, the sets Π1 ∪ ∆ and Π2 ∪ ∆ have the same equilibrium models.

Theorem 2 (Strong equivalence) Π1 and Π2 are strongly equivalent if and only if Π1 and Π2 are equivalent in FQHT.

Proof: The statement is a consequence of the following properties:

The proof is easy and left to the reader.

⊣

Proof of theorem 2:

• Assume that Π1 and Π2 are equivalent in FQHT; in particular, they have the same total models. Let ∆ be set of formulas and 〈I, I〉 an equilibrium model of Π1 ∪ ∆; then it is also a model of Π2 ∪ ∆. Moreover, it is in equilibrium, because if 〈J, I〉 is a different a model of Π2 and ∆, then it would be a model of Π1, and thus of Π1 ∪ ∆, which is impossible, because 〈I, I〉 is an equilibrium model of Π1 ∪ ∆.
• Let us assume that Π1 and Π2 are strongly equivalent and let 〈I h , I t 〉 be a FQHT-model of Π1.

(the formulas δc were defined just before Corollary 1) It is not hard to see that 〈I, I〉 is a model of ∆ and there is no model 〈J, I〉 of ∆ such that J ̸= I. Therefore, 〈I, I〉 is an equilibrium model of Π1 ∪ ∆ and thus of Π2 ∪ ∆; in particular, it is a model of Π2.

1. If I h ̸= I t , then by Lemma 1, 〈I t , I t 〉 is also a model of Π1, and by the previous item it is also a model of Π2. If a ∈ C, we define the formula φa = ∃x(x = a ∧ ¬(x = a)); if f ∈ F, we define the formula φf = ∃x∃y(x = f(y) ∧ ¬(x =

f(y))); and if p ∈ P, we define the formula φp = ∃x(p(x) ∧ ¬p(x)).

Then, let us consider the set

It is easy to check that 〈I h , I t 〉 and 〈I t , I t 〉 are the unique models of ∆ with I t in the 'there' part. Therefore, 〈I t , I t 〉 is not an equilibriummodel neither of Π1 ∪ ∆ nor Π2 ∪ ∆. Since 〈I h , I t 〉 is the unique non-total model of ∆, necessarily 〈I h , I t 〉 must be a model of Π2.

Analogously, we can prove that every model of Π2 is a model of Π1. ⊣

4 Gentzen system

We now introduce a Gentzen system for FQHT logic. This system is similar to that for SQHT= introduced in [Mints, 2010]; they only differ in the rules for equality.

The sequents in the system are pairs Γ ⊢ ∆ where Γ and ∆ are lists of formulas (the order does not matter and the formulas may appear several times). The formulas in the sequents may be non-closed, which is equivalent to considering a set (possibly denumerable) of additional parameters.

4.1 The systemFHTG

Axioms:

Structural rules:

Rules for propositional connectives:

Rules for quantified formulas: In the following rules, y is a variable which does not occur free in Γ ∪ ∆:

In the following rules, t is an arbitrary term, possibly with variables:

Rules for equality: In the following rules, t and s are terms, possibly with variables:

4.2 Soundness and completeness of FHTG

Although the system does not include some standard structural rules, they are valid and may be used without modifying the inference relation. Specifically, the weakening rules and the cut rule may be added to the system; although they are not needed in sequent deductions, they are very useful in theoretical proofs about the system.

Lemma 2 If the following rules are added to FHTG, no new sequents can be proved.

Lemma 3 If the cut rule is added to FHTG, no new sequents can be proved.

Lemma 4 The following sequents are provable in FHTG:

Theorem 3 (Soundness) If Γ and ∆ are lists of formulas such that Γ ⊢ ∆ is deducible in FHTG, and I is a model of Γ, then I is a model of a formula ψ ∈ ∆. In particular, if Γ ⊢ ϕ, then Γ |= ϕ

As usual, the soundness proof consists in verifying that every rule preserves the satisfiability of sequents. It is useful to bear in mind that substitution rules only apply if the equality appears on the left hand side; thus, if I, h |= t = s, then the interpretation of t and s is the same element of the domain in both worlds, and thus the interpretation of the formulas ϕ(t) and ϕ(s) is the same. In HTG= ( [Mints, 2010]), the substitution may be apply if ¬(t = s) is false, because in SQHT=, ¬¬(t = s) and (t = s) are equivalent which is not true in FQHT.

Theorem 4 (Completeness) If Γ and ∆ are lists of formulas such that for every model I of Γ there exists ψ ∈ ∆ such that I is a model of ψ, then Γ ⊢ ∆ is deducible in FHTG. In particular, if Γ |= ϕ, then Γ ⊢ ϕ

Proof: We can use the standard proof procedure for completenes of Gentzen systems. From Γ ⊢ ∆, the rules are applied bottom-up for every formula in Γ∪∆, generating a tree of sequents where the branches are expanded if the leaves are not axioms. If the tree is not finite (not all branches of the tree contains axioms), then the sequent Γ ⊢ ∆ cannot be proved and, by Koening's lemma, the tree contain an infinite branch; let Γh be the union of the sets in the left hand side of the sequents in this branch, and let ∆t be the union of the sets in the right hand side of the sequents in the branch. The proof concludes using the sets Γh and ∆t to build a model of Γ which is a countermodel of ∆. First, we note that

and that, by the definition of the tree proof, these sets verify the following saturation conditions:

• Γh ∩ ∆t ̸= ∅ and there is no formula α ∈ Γh s.t. ¬α ∈ Γh.
• If α∧ β ∈ ∆t, then either α ∈ ∆t or β ∈ ∆t.
• If α∧ β ∈ Γh, then α ∈ Γh and β ∈ Γh.
• If α∨ β ∈ ∆t, then α ∈ ∆t and β ∈ ∆t.
• If α∨ β ∈ Γh, then either α ∈ Γh or β ∈ Γh.
• If α→ β ∈ ∆t, then either α ∈ Γh and β ∈ ∆t, or ¬β ∈ Γh and ¬α ∈ ∆t.
• If α → β ∈ Γh, then either ¬α ∈ Γh, or α, ¬β ∈ ∆t, or β ∈ Γh.
• If ¬(α∨ β) ∈ ∆t, then either ¬α ∈ ∆t or ¬β ∈ ∆t.
• If ¬(α∨ β) ∈ Γh, then ¬α ∈ Γh and ¬β ∈ Γh.
• If ¬(α∧ β) ∈ ∆t, then ¬α ∈ ∆t and ¬β ∈ ∆t.
• If ¬(α∨ β) ∈ Γh, then either ¬α ∈ Γh or ¬β ∈ Γh.
• If ¬(α→ β) ∈ ∆t, then either ¬α ∈ Γh or ¬β ∈ ∆t,
• If ¬(α→ β) ∈ Γh, then ¬β ∈ Γh and ¬α ∈ Γh, or
• If ¬¬α ∈ Γh, then ¬α ∈ ∆t.
• If ¬¬α ∈ ∆t, then ¬α ∈ Γh.
• If ∃xα(x) ∈ Γh, then α(y) ∈ Γh for some y.
• If ¬∀xα(x) ∈ Γh, then ¬α(y) ∈ Γh for some y.
• If ∀xα(x) ∈ ∆t, then α(y) ∈ ∆t for some y.
• If ¬∃xα(x) ∈ ∆t, then ¬α(y) ∈ ∆t for some y.
• If ∀xα(x) ∈ Γh, then α(t) ∈ Γh for every t.
• If ¬∃xα(x) ∈ Γh, then ¬α(t) ∈ Γh for every t.
• If ∃xα(x) ∈ ∆t, then α(t) ∈ ∆t for every t.
• If ¬∀xα(x) ∈ ∆t, then ¬α(t) ∈ ∆t for every t.
• If t = s ∈ Γh, and α(t) ∈ Γh, then α(s) ∈ Γh.
• If t = s ∈ Γh, and α(t) ∈ ∆t, then α(s) ∈ ∆t.
• t = t ∈ ∆h for every term t.

Now, we are going to define the countermodel I = 〈I h , I t 〉 and first we build its domain. Let C ∗ = {a∗ | a ∈ C} and F ∗ = {f ∗ | f ∈ F}. Let T(V ∪ C, F) be the set of terms built over the variables in V (the set of free variables in Γh ∪ ∆t) the constants in C and functions in F. If t ∈ T (V ∪ C, F ), we denote by t∗ the term obtained by replacing every constant a ∈ C by a∗ and every function f ∈ F by f ∗ .

In T (V ∪ C, F ) ∪ T (V ∪ C ∗ , F ∗ ) we define the following congruence relation:

• If s1, s2 ∈ T(V ∪C, F), then s1 ≈ s2 if s1 = s2 ∈ Γh.
• If s∗1 , s∗2 ∈ T(V ∪C ∗ , F ∗ ), then s∗1 ≈ s∗2 if either s1 = s2 ∈ Γh or ¬(s1 = s2) ∈ ∆t.

The terms simultaneously in T(V ∪ C, F) and T (V ∪ C ∗ , F ∗ ) are just the variables and for this particular case, the congruence coincides with the equality between variables in both sets of terms, because x = x ∈ Γh for every variable x. On the other hand, the relation ≈ is reflexive, symmetric and transitive (as a consequence of Lemma 4 and the substitution rules for equality) and thus we can consider the quotient set D = T(V ∪ C, F) ∪ T(V ∪ C ∗ , F ∗ )/ ≈, which is the domain of the interpretations we are building. Intuitively, the original language will be interpreted in T(V ∪ C, F) at the world h and will be interpreted in T(V ∪C ∗ , F ∗ ) at the world t.

• For every a ∈ C, I h (a) = [a]; if f ∈ F, we only need to define I h (f) over terms in T(V ∪C, F), specifically, I h (f)([s1], . . . , [sn]) = [f(s1, . . . , sn)].
• For every a ∈ C, I t (a) = [a∗ ]; if f ∈ F, we only need to define I t (f) over terms in T(V ∪ C ∗ , F ∗ ), specifically, I t (f)([s∗1 ], . . . , [s∗n ]) = [f ∗ (s∗1 , . . . , s∗n )].
• If p(s1, . . . , sn) ∈ Γh, then ([s1], . . . , [sn]) ∈ I h (p), ([s1], . . . , [sn]) ∈ I t (p), ([s∗1 ], . . . , [s∗n ]) ∈ I h (p), and ([s∗1 ], . . . , [s∗n ]) ∈ I t (p). If ¬p(s1, . . . , sn) ∈ ∆t, then ([s∗1 ], . . . , [s∗n ]) ∈ I t (p).

The definition of I h (p) and I t (p) in the previous item, may be extended by induction to any formula. Specifically, the following properties are easily proved by induction over ϕ:

1. If ϕ ∈ Γh, then I, h |= ϕ 3. If ϕ ∈ ∆t, then I, h ̸|= ϕ

Therefore, I is a model of Γh and in particular of Γ and it is a countermodel of every formula in ∆t and in particular of every formula in ∆. ⊣

4.3 Comparison with SQHT=

As we have mentioned before, the system FHTG is similar to the systemHTG= introduced in [Mints, 2010], which is a sound and complete system for the logic SQHT= studied by

[Pearce and Valverde, 2005; Lifschitz et al., 2007] as a foundation for answer set programs and equilibrium logic. They differ in the rules for equality, specifically SQHT= includes the following rules in addition to FQHT:

In both logics, the axiom of decidable equality is valid,

however, in SQHT= the formulas

for every pair of terms t and s are also valid; in general these formulas are not valid in FQHT. Therefore, in FQHT the equality relation is not decidable in this more general sense.

An interesting consequence is that if consider both systems without the equality predicate, we obtain the same logic, although we have flexibility in one but not in the other; that is, the flexibility, and in consequence the semantics for intensional functions is only relevant in the presence of equality.

4.4 Choice rules

Choice rules are a familiar construction in answer set programming. For example the expression {p(x)} is used as shorthand for the rule {p(x) ∨ ¬p(x) ←} and is called a choice rule. The failure of (2) in FQHT allows us to formulate choice rules for intensional functions. For example, following [Bartholomew and Lee, 2012] we can express a choice condition such as

and abbreviate this by

Using their example, {f = 1} expresses that by default the function f takes the (rigid) value 1. In action formalisms, some fluents like spatial location are known as non-Boolean and subject to inertia laws. Using the idea of intensional functions one can express an inertia law for location succinctly by

stating that by default the location of an object a does not change over time. This, as [Bartholomew and Lee, 2012] observe, is strongly equivalent to

In SQHT=, (3) is valid, so that (4) and (5) make no sense. They do make sense in FQHT and in either system (5) and (6) are immediately equivalent by propositional logic.

4.5 Comparison with IF-programs

As [Bartholomew and Lee, 2012] point out, their approach differs considerably from that of [Lifschitz, 2012] and neither semantics is stronger than the other. Our results help to shed light on some of the logical differences. For example, the propositional fragment of FQHT is just the logic HT of here-and-there, while the logical basis for IF-programs is given by a system called bi-state logic, BiS, [Fari˜nas del Cerro et al., 2012]. While each logic has theorems that are not valid in the other, every HT-model of a formula is also a BiS-model of it. Moreover, a special kind of stability condition over BiS-models may be defined such that for generalised logic programs they become equivalent to equilibrium or stable models, [Fari˜nas del Cerro et al., 2012].

5 Concluding remarks

We have introduced a logic FQHT that is suitable for reasoning about programs and theories with intensional functions. In particular, using FQHT as a basis, we have shown how to define a variant of equilibrium logic that is in agreement with the stable model semantics for intensional functions proposed by [Bartholomew and Lee, 2012]. This is a different approach to the one proposed in [Lifschitz, 2012] but it gives intuitively correct results and has some good metatheoretical properties. As our logical treatment confirms, it is conceptually close to the usual logic and semantics of stable models and answer sets.

Strong equivalence is a key property in ASP and nonmonotonic theories. Characterising it by means of a logical system enables one to use ordinary logical deduction to deal with problems of theory replacement and optimisation. We have provided a complete proof procedure for FQHT in the form of a Gentzen system. By the strong equivalence theorem, this system is suitable for checking whether theories with intensional functions are equivalent in the robust or strong sense, i.e. under all possible extensions.

Our results reveal two features that are at first sight quite surprising. The first is that the semantics of intensional functions results from the usual semantics simply by accommodating the non-rigid designation of terms, or allowing flexible interpretations as we called them (with a corresponding adjustment in the truth condition for the atomic case). The second is that from a logical point of view this change makes a difference only where equality is concerned: the equalityfree fragments of FQHT and SQHT= are equivalent. In view of these features it should be obvious how we can accommodate intensional and extensional functions (and predicates) within a single theory, namely by requiring the constant and function symbols of the latter kind to be rigid designators as in the standard possible worlds semantics. In formalising knowledge in a given domain, one simply allows for two sorts of terms in the language and applies the appropriate semantics to each kind.

In logic there is a very considerable literature on problems of rigid versus non-rigid designation which we cannot review here. However, for a detailed discussion and references regarding quantified modal logic, the reader is referred to [Garson, 2001]. To our knowledge there are no previous works that discuss non-rigid designators in the logic of here-and-there. Several questions suggest themselves for the future; in particular, how to obtain an axiomatic system for FQHT. We would also like to study the behaviour of this logic over expanding domains as well as consider whether important metatheorems such as interpolation continue to hold in FQHT.