Class Notes

Tom Costello

April 21, 1998

1 Formula Circumscription

We now consider the first order case of circumscription. That is, we consider how we circumscribe first order theories. We do not treat functions and constants in the following as the generalization sheds no new light on our exposition. Thus our signatures will not contain any function or constant symbols.

Definition 1 (≤, < on first order formulas) We introduce the notation γ_{1}, γ_{2} ≤ δ_{1}, δ_{2} for the formula (∀\overline{x}.γ_{1}(\overline{x}) → δ_{1}(\overline{x})) ∧ (∀\overline{y}.γ_{2}(\overline{y}) → δ_{2}(\overline{y})), and γ_{1}, γ_{2} < δ1, δ_{2} for the formula γ_{1}, γ_{2} ≤ δ_{1}, δ_{2} ∧ ¬(δ_{1}, δ_{2} ≤ γ_{1}, γ_{2}), where \overline{x} and \overline{y} are sequences of variables equal in number to the free variables of γ_{1}, δ_{1} and γ_{2}, δ_{2}.

Definition 2 If γ_{1}, γ_{2} is a pair of^{1} formulas of a first order language L, and P_{1} is a predicate symbol^{2} of L, then the circumscription of α minimizing γ_{1}, γ_{2}, formulas in L, varying P_{1}, written Circ_{F} (α; γ_{1}, γ_{2}; P_{1}) is,

α ∧ ∀ψ_{1}.¬ [α′ ∧ γ′_{1}, γ′_{2} < γ_{1}, γ_{2}]

where ψ_{1} is a predicate variable equal in arity to P_{1}. We use α′ to denote the formula, α[ψ_{1}/P_{1}], that is the replacement of the predicate P_{1} in α by a predicate variable ψ_{1}..

We now introduce the semantics for formula circumscription.

Definition 3 Let α be a sentence of L, a first order language with equality, whose predicates are P_{1}, …, P_{n}. Let Z be a subset of P_{1}, …, P_{n}. A model 𝔄 of α is a γ_{1}, … γ_{n}; Z-sub-model of a model 𝔅, written 𝔄 ≤^{γ_{1},...γ_{n};Z} 𝔅, if and only if:

• ∥𝔄∥ = ∥𝔅∥, where ∥𝔄∥ denotes the universe of 𝔄,

• 𝔄[γ_{i}] ⊆ 𝔅[γ_{i}], for i = 1 … n, where 𝔄[γ_{i}] is the interpretation of γ_{i} in 𝔄,

• 𝔄[K] = 𝔅[K], for every predicate constant not in Z.

1We minimize a pair for simplicity. The extension to an arbitrary finite number is the natural one.

2We choose one predicate symbol for simplicity again.

𝔄 is a γ_{1}, … γ_{n}; Z-minimal model of α if and only if it is a minimal model of α under ≤^{γ_{1},...γ_{n};Z}.

Thus, as in the propositional case, every circumscription policy is a finite set of formulas, and it gives rise to a pre-order.

We now consider another way of defining pre-orders on L-structures. We first need the notion of a disjoint union of structures.

Definition 4 Let L be a first order language, with predicates P_{1}, …, P_{n}. If 𝔐 and 𝔑 are L structures with the same universe, then we define the disjoint union of 𝔐 and 𝔑 to be a first order structure 𝔒 over a language P_{1}, …, P_{n}, P′_{1}, …, P′_{n}, such that the interpretation of P_{i} in 𝔐 is the interpretation of P_{i} in 𝔒 and the interpretation of P_{i} in 𝔑 is the interpretation of P′_{i} in 𝔒.

We now define what a first order definable pre-order on L-structures is.

Definition 5 Let L be a first order language, with predicates P_{1}, …, P_{n}, and ≤ a pre-order on structures of L. We say that ≤ is first order definable if there is a first order formula ϕ in a language P_{1}, …, P_{n}, P′_{1}, …, P′_{n}, such that if 𝔐 and 𝔑 are L structures, with the same domain, then the disjoint union of 𝔐 and 𝔑 models ϕ exactly when 𝔐 ≤ 𝔑

We can now show that every first order definable pre-order is captured by a second order sentence, of the same complexity class as circumscription. They each have only universal second order quantifiers, and are thus Π_{1}^{1}, or inductive definitions [Mos74].

Theorem 1 Let L be a first order language, with predicates P_{1}, …, P_{n}, and ≤ a first order definable pre-order on structures of L.

Let A[P′_{1}, …, P′_{n}] be a formula of second order logic, without second order quantifiers, with n second order variables P′_{i}, for i ≤ n.

Then there is a sentence of second order logic Φ with only universal second order quantifiers whose consequences are the formulas entailed in the ≤ minimal models of A[P_{i}/P′_{i}, P′_{j}/P_{j}].

Proof: Let ϕ be the witness of the first order definability of ≤, with its 2 ∗ n free predicate variables being P′_{i}, …, P′_{n}, P′′_{1}, …, P′′_{n}.

If ϕ[P_{i}/P′_{i}, P′_{j}/P_{j}] represents the simultaneous replacement of every P_{i} by P′_{i}, and P′_{j} by P_{j} then,

A[P_{i}/P′_{i}] ∧ ∀P′_{1}, …, P′_{n}.[A ∧ ϕ[P_{i}/P′′_{i}]] → ϕ[P′_{i}/P′′_{i}, P_{j}/P′_{j}]

is the required sentence.

Formulas of the above form has been called generalized circumscription by Lifschitz [Lif84]. Here rather than a set of formulas to minimize, we have a formula, with twice as many free predicate variables as the language has predicate constants, that defines the required pre-order.

We now show that circumscription can’t capture all first order axiomatizable pre-orders by considering an example. The following example is more complicated than it need be.

However, as it currently is it represents a widely used default, rather than a concocted example.

It is the standard order on structures that captures the default used in temporal projection. It uses the situation calculus [MH69], a formalism for reasoning about change. It is a three sorted language, with situations s, fluents f, and actions a. The predicate holds(f, s) states that the fluent f holds at situation s, while the function result(a, s) gives the situation resulting from doing the action a in situation s. A predicate ab(a, f, s) states that the fluent f changed between s and result(a, s). This order on models has been proposed by Reiter and Lin [LR94] and Giunchiglia [Giu96] and Costello [Cos97]. It is widely accepted to be the correct solution to the frame problem for problems involving only temporal projection.

Example 1 Consider a pre-order ≤ on first order structures. Let the language of these structures have three sorts, fluents, actions and situations. The language has two predicates, holds which is a predicate on fluent situation pairs, and ab which is a predicate on action, fluent, situation triples. It also contains a function from action situation pairs to situations, result, and a situation constant S0.

Let 𝔐 and 𝔑 be first order structures for this language. We say that 𝔐 ≤ 𝔑, when if F, A, S are the universes of fluents, actions and situations, in both 𝔐 and 𝔑, and 𝔐[P] is the interpretation of P in 𝔐 then

∀s ∈ S, f ∈ F, a ∈ A.(∀f′ ∈ F.⟨f′, s⟩ ∈ 𝔐[holds] iff ⟨f′, s⟩ ∈ 𝔑[holds]) and
⟨a, f, s⟩ ∈ 𝔐[ab] implies ⟨a, f, s⟩ ∈ 𝔑[ab]

We do not relate structures with different universes.

We note that this is clearly a first order definable pre-order on models, as the formula

(∀f′.holds(f′, s) ≡ holds′(f′, s)) ∧ ab(a, f, s) → ab′(a, f, s)

is the required witness.

This pre-order has an uncountable anti-chain when all the universes, F, A, S are countable. Further, this pre-order has 2^{2^{ℵ_{0}}} upper-sets when all the universes, F, A, S, are countable.

We note that the structures that have a different interpretation of λf.holds(f, S0) are incomparable. Further, every set of structures, for a given triple of universes, which agree on the interpretation of λf.holds(f, S0) form an upper-set. These upper-sets are all clearly disjoint. There are 2^{ℵ_{0}} distinct interpretation of λf.holds(f, S0) and thus there are 2^{2^{ℵ_{0}}} distinct upper-sets.

Proposition 2 The set of upper-sets of the pre-order generated by a first order circumscription policy, restricted to structures with a given countable universe, has cardinality bounded by 2^{ℵ_{0}}.

Proof:

A basis for the upper-sets is given by all instantiations into the minimized formulas. There are at most a countable number of distinct formulas that result from this, as the universe is countable, and the set of formulas is finite, and thus has a finite number of free variables. If the upper-sets of a pre-order have a countable basis, then there are at most 2^{ℵ_{0}} upper-sets, as every upper-set is the result of unions and intersections of upper-sets in the basis.

Theorem 3 There are first order definable pre-orders on of first order structures not captured by circumscription.

Proof: Immediate from Proposition 2 and Example 1.

This is relevant because the example above that circumscription cannot capture is a natural default that has been used in reasoning about action, a domain where circumscription has been widely applied.

2 Conclusion

We show that generalized circumscription as conceived by Lifschitz [Lif84] is strictly stronger in expressive power than formula circumscription, and this extra expressive power is necessary to capture the default of inertia in temporal projection.

References

[Cos97] Ton Costello. Change, Change, Change, three approaches. In Proceeding of the Fifteenth International Joint Conference on Artificial Intelligence (IJCAI97), pages 1426–1431. Morgan Kaufmann, 1997.

[Giu96] E. Giunchiglia. Determing Ramifications in the Situation Calculus. In J. Doyle, editor, Principles of Knowledge Representation and Reasoning: Proc. Fifth International Conference (KR ’96), pages 76–86, 1996.

[Lif84] V. Lifschitz. Some Results on Circumscription. In First Workshop on Nonmonotonic Reasoning, pages 151–164, Stanford University, August 1984.

[LR94] F. Lin and R. Reiter. State Constraints Revisited. Journal of Logic and Computation, 4(5):655–678, 1994.

[MH69] J. McCarthy and P. Hayes. Some Philosophical Problems from the Standpoint of Artificial Intelligence. In D. Michie, editor, Machine Intelligence 4, pages 463–502. Edinburgh University Press, Edinburgh, UK, 1969.

[Mos74] Y. N. Moschovakis. Elementary Induction on Abstract Structures. North-Holland, 1974.