Circumscription and Definability

1 Introduction

Firstly, McCarthy defined domain circumscription which reduces the set of individuals (§2). Later, he defined predicate circumscription, which reduces the extensions of some relations (§3) . McCarthy has stated [1980] that domain circumscription is a particular case of predicate circumscription. LEtherington and Mercer, 1987] reaf­ firmed the importance of domain circumscription and contested McCarthy's statement. We show (§8) why this contestation is not fully justified and we provide two im­ provements of McCarthy's translation. To obtain our results, we define (§4) a variant of the strong pointwise circumscription of [Lifschitz, 1988a]. Cases of equiva­ lence with standard circumscrition (§5) allow us to an­ swer the central question in [Doyle, 1985]: when does circumscription define the predicates (§6)? A stronger circumscription, "definabilization" (§7), simplifies the expression, and hopefully the computation, of domain circumscription. We make precise the expression of do­ main circumscription in terms of predicate circumscrip­ tion. Throughout the text we provide the semantics for each kind of "circumscription" defined, thus all of them, including the first order versions, may be considered as preferential entailment notions.

2 Domain circumscription

In many situations only the objects named are supposed to exist. Domain circumscription ([McCarthy, 1980], amended by [Morreau, 1985, Etherington and Mercer, 1987]) formalizes this idea. A theory Tis a set offormu­ las in a first order language £. ell or ell(z0], is a formula

Raymond Rolland

IRMAR, Campus de Beaulieu

35042 RENNES-Cedex, FRANCE. tel.: (33) 99-28-60-19

in£, ell(z] denotes the formula obtained by substituting the free variable z for every free occurrence of zo in ell (z not bound in ell(zo]).

Definitions 2.1 a) Aziomc.(~) denotes {3zo ell(zo]}, together with the set of formulas

{Vx (~] => ell(f(x)])/ f is a function symbol in£}. x is a tuple (z1, ... , z~:) of free variables, k is the arity of/, and ~J is ell(z1] A ... A ell(z~:] (TRUE if k=O) .

b) T , the relativization of T to ~, is T in prenex form, where for each variable symbol y, we replace 'v'y (·.·)by 'v'y (ell(y] => (·. ·)) and

3y (· ··)by 3y (ell(y] A(···)) (thus P(a) by ell(a] A P(a)).

c) Circd(T), the domain circumscription ofT, adds the following axiom schema to T:

for each formula ell in £.

Notations Our models are normal (equality interpreted as identity). If JJ is an interpretation over £, DIJ is its domain. For each predicate P (resp. function/) of arity k in £, the subset IPIIJ of D! (resp. the application /IJ of D! in DIJ) denotes its extension in JJ.

J:.IJ, the language of JJ, adds to £ a name for each element in D IJ"

Definition 2.2 (see e.g. [Enderton, 1972] p.90-91) JJ and 11 are interpretations over £. We denote 11 < JJ, if and only if: 1) D, C DIJ (strict inclusion),

1. for each function fin£, if e E D!, then /IJ(e) = f,(e),
2. for each predicate P in £, IPIIJ n D! = I PI,.

Definition 2.3 'R is a binary relation between interpre­ tations over £. A model JJ ofT is minima/ for 'R when no model11 ofT is such that 11'R JJ .

Theorem 2.1 (Davis [1980]) Any model ofT minimal for< is a model of Circd('T).

The converse needs a more sophisticated relation:

Definition 2.4 (see e.g.[Enderton, 1972] p.88-89 and ex. 24 p.97): A subset S of D! is definable with param­ eters in JJ when there exists a formula ell in £1J, of arity k, such that S = lelllw

Definition 2.5 If 11 < JJ and if D, is definable with parameters in JJ, we note 11 < 6 JJ.

Theorem 2.2 ([Morreau, 1985], or §8) The models of Circd('T) are the models of T minimal for < 6 ·

Here is an example showing how domain circumscrip­ tion reduces the domain to the minimum allowed by the axioms of the given theory (note that here, it does not matter whether we use< or < 6 ) .

Example 2.1 Tis P(a) A 3z-,P(z).

Aziomc(~) is ~(a], T .. is ~[a)AP(a)A3z(~[z]A-,P(z)) (SOC) is: T .. => Vz ~[z) (for every ~ in C..) . Choosing (z = a V z = y) as ~[z) in (SOC) gives: Circd(T) = P(a) A 3y(-,P(y) A Vz (z =a V z = y)). The models of Circd(T) are the models ofT with only two elements.

3 Predicate circumscription

Definition 3.1 ([McCarthy, 1986]) a) Let T be a finite set of first order formulas in which the lists of predicates P = (P1, · ·. ·, Pn) and Q = (Ql. · · · ,Qm) occur. The first order circumscription of P in T with Q varying, noted Circ1(T: P; Q) (Circ1(T: P) if Q is empty), adds the following axiom schema toT, (SAC):

{T[p, q) A Vx (p[x] => P(x))} => Vx (P(x) => p[x]), for every p = (Pl.··· ,Pn) , q = (ql. · · ·, qm) lists of first order formulas in C.. .

T[p,q) is T where each occurrence of P; (resp. Qi) is replaced by p; (resp. qi) · p[x) => P(x) is (pl[x1] => P1(x1)) A· ·· A (Pn[Xn) => Pn(Xn)) ·

The square brackets mean that p;[z;) may have free variables not included in x; = {zi,l. · · ·, z; ,kJ (k; arity of P;) (see [Besnard et a/., 1989] and ex. 8.1 below).

b) The second order circumscription Circ2(T: P; Q) adds the following axiom toT, (AC):

Vpq {[T[p, q) A (Vx (p(x) => P(x))) => Vx (P(x) => p(x))},

p and q are lists of predicate variables, each p; (resp. qi) having the arity of P; (resp. Qi ).

Circ denotes either Circ1 or Circ2.

Definition 3.2 Let I' and v be two interpretations over C. . We write I' =P;Q v when I' and v are identical except that there is no condition on the extensions of the Pi's (1 ::; j ::; n) and Qi 's (1 $ j $ m). Furthermore, if each IP;I,.. and IQil,.. is definable with parameters in v , we write I' =~;Q v . If Q is empty, we write =p or=~ ·

=P;Q is an equivalence relation, =~ is reflexive and transitive but it is not symmetrical (ex. 5.3).

Definition 3.3 I' <P;Q v (respectively I' <~;Q v) means I' =P;Q v (respectively I' =~ ;Q v), and IP;I,.. ~ IP;Iv (1 $ i $ n) with some IP;I,.. C IP;Iv·

If Q = 0, we note <p or<~ .

Definition 3.4 (Lifschitz [1986]) T is {P; Q)-we/1 founded when for every model I' of T, not minimal for <P;Q · there exists a model v ofT minimal for <P;Q with v <P;Q I'·

Universal theories are (P; Q)-well founded [Bossu and Siegel, 1985, Etherington et a/., 1985, Lifschitz, 1986].

Theorem 3.1 a) Soundness (see [McCarthy, 1980, Lif­ schitz, 1986]): Every model ofT which is minimal for

<P;Q is a model of Circ(T: P ; Q) .

b) [Lifschitz, 1986] The models of Circ2(T: P; Q) are the models ofT minimal for <P;Q .

c) [Besnard, 1989] The models of Circ1(T: P ; Q) are the models ofT minimal for <~;Q '

A model minimal for <P;Q is minimal for <~;Q'

As it is one of the purposes of this text , we give now an example where a seemingly stronger axiom is in fact equivalent to the circumscription axiom (first order or second order version).

Example 3.1 Tis P(O) A Vz (P(z) => P(s(z))) .

Circ1(T : P), adds the following axiom schema toT: for each formulap in C..: (SAC) {p[O)A Vz (p[z] => p[s(z)])A Vz (p[z) => P(z))} => Vz (P(x) => p[z]). Let {SAR) be the axiom schema of (Peano's) recurrence: for each p in C.. : {p[O] A Vx (p[x] => p[s(x)])} => Vx (P(x) => p[z]) . Clearly (SAR) entails (SAC), soT U (SAR) entails Circ1(T : P). Here the converse is true (§5) .

4 A strong predicate circumscription

We reinforce and simplify (SAC) the circumscription schema, or the axiom (AC).

Definition 4.1 The first order strong circumscription of P in T, with Q varying, Circf1(T: P ; Q), adds to T the schema (SACf) : T[p, q) => Vx (P(x) => p[x]). The 2nd order version Circf2(T: P; Q), adds (ACf) :: Vpq {T[p, q) => Vx (P(x) => p(x))} toT.

Circf denotes either Circf1 or Circf2.

Circf(T : P; Q) 1- Circ(T : P; Q).

Here is the semantics for this strong circumscription.

Definitions 4.2 We write v -<P;Q I' (respectively v -<~ ;Q I') when v =p;Q I' (respectively v =~;Q I') and IP;I,..- IP;I., =! 0 for at least one i (1 $ i $ n) .

"-" denotes the set difference.

If Q is empty, then we write -<p or -<~ .

Theorem· 4.1 The models of Circf2(T: P ; Q) (respec­ tively Circf1(T: P; Q)) are the models ofT minimal for -<P;Q (respectively -<~ ;Q).

Remarks 4.1 a) The proofs are as the proofs of theo­ rem 3.1.

b) If v <P;Q I' , then v -<P;Q I' ·

1. -<P;Q is neither transitive nor antisymmetrical.

d) (v -<p 1 ,P 2 ;Q I') if and only if

(v -<pl ;P2 ,Q I') or (v -<p2 ;Pl,Q IJ).

1. , c) and d) also hold with 6 -relations.

Example 4.1 Tis (P(a) V P(b)) A afb.

• Circ(T : P) is consistent, being equivalent to afb A (Vz (P(z) ¢> x=a) VVx (P(x) ¢> x=b)) .
• From Circf(T: P) , -,P(a) can be proved (choose x=b as p[z] in (SACf)), as can -.P(b) (choose p[x] = x=a). Thus Circf(T: P) is inconsistent.
• Here are 3 models of T, with the same domain

{a, b, e}: IPII' ={a, b, e}, IPiv ={a}, IPiv' = {b}. v and v', minimal for <p, are models of Circ(T: P): v <p 1-1, v' <p 1-'· v -<P 1-1, v' -<P 1-1, v -<P v' and v' -<P v: there is no model minimal for -<P. Here, the domain is finite and so the 6 -relations coincide with these relations.

Here is a result about strong circumscription (proof: remark 4.1-d, which is obvious):

Now, this strong circumscription is not as new as it may seem, although the presentation and the semantics are new:

Definition 4.3 ([Lifschitz, 1988b]) The strong point­ wise circumscription adds to T the schema (SAPf): Vx -,(P(x) 1\ -,p[x] 1\ T[p, q]), for every tuple of formulas (p, q) in£.

Lifschitz defines only individual strong pointwise cir­ cumscription (for one Pat a time), and uses unions. We allow tuples P in parallel strong circumscription. The­ orem 4.2 shows that these two ways are equivalent. As this circumscription is not pointwise at all, we prefer our name "strong circumscription".

Lifschitz gives an elegant second order formula

Also, the "modal strong circumscription" of [Pedis, 1988], differs from (SACf) only in the fact that P(x) is replaced by KP(x), where K is a modal operator, attenuating this otherwise too strong circumscription.

5 When strong and standard circumscriptions coincide

Definitions 5.1 a) A theory T::: T[P; Q] is stable for extended conjunction in (P; Q) (first order version) if, for every tuple of formulas p, q, p', q' in £ :

T[p, q] U T[p', q'] 1- T[p 1\ p' 1\ p", q"] for some tuples p", q" of formulas in £ .

p, p', p" have the same length as the tuple of predi­ cates P, and q, q', q" have the length of Q. p 1\ p' 1\ p" denotes the tuple of the p; 1\ p: 1\ p:"s involved.

b) T is stable for extended conjunction in (P; Q) (second order version) if Vp qp' q' 3p" q" {(T[p, q] 1\ T[p', q']) => T[p 1\ p' 1\ p", q"]} is true in T . p, q, p', q', p", q" are tuples of predicate variables of suitable lengths and arities.

If there is no p", T is stable for conjunction in P .

Theorem 5.1 If T is stable for extended conjunction in (P; Q), then Circf(T : P; Q) = Circ(T : P; Q).

Proof: This theorem is true for the 1't and for the 2nd order versions of definitions 3.1, 4.1 and 5.1. We give the 1't order version.

·circf1(T: P; Q) entails Circ1(T: P; Q), we need the converse. Circ1(T: P; Q) is: T and (SAC) . Sup­ pose we also have T[p,q] . T::: T[P, Q], so we get (def­ inition 5.1) T[p 1\ P 1\ p",q"], for some p", q". The instance of (SAC) associated with (p 1\ P 1\ p", q") gives Vx (P(x) => (p[x] 1\ P(x) 1\ p"[x])) . Thus T[p, q] => Vx (P(x) => p[x]), i.e. (SACf)

Horn theories are stable for conjunction in (P; Q) (generalize a well-known result of [van Emden and Kowalski, 1976]). Thus, for Horn theor~es (or for strati­ fied logic programs, see [Moinard, 1990]) we may sim­ plify the circumscription axiom. So in example 3.1, Circf1(T : P), which is T U (SAR) in this case, is equiv­ alent to Circ1(T: P).

Definition 5.2 A theory T has the property of extended intersection in (P; Q) if and only if, for every models 1-1 and v ofT such that v =P;Q 1-1, there exists a model1-1' ofT such that 1-1' =P;Q 1-1 , with IPII'' ~ IPII' n IPiv ·

Theorem 5.2 a) A theory Tis stable for extended con­ junction in (P; Q) (second order version), if and only if T has the property of extended intersection in (P; Q) .

b) IfT is (P; Q)-well founded, then Circ2(T: P ; Q) is equivalent to Circf2(T: P; Q) if and only if T has the property of extended intersection in (P; Q).

Proof: a) Details lengthy, but obvious (see [Moinard and Rolland, 1991].

b) Theorem 5.1 gives one way. Circ2(T: P; Q) = Circf2(T: P; Q) if and only if: for every model1-1' ofT minimal for <P;Q' if 1-1 is a model ofT and 1-1 =P;Q 1-1', we have: IPI~ ~ IPII' (see remark 4.1 b). Let 1-1 and v be two models of T with v =p;Q 1-'· As T is (P; Q)­ well founded, there exists 1-1' model of T, minimal for <P;Q with (1-1' <P;Q 1-' or 1-1' = 1-')· 1-1' =P;Q 1-1, so IPII'' ~ IPiw Also, 1-1' =P;Q v thus IPII'' ~ IPiv and IPII'' ~ IPII' n IPiv·

If Tis (P; Q)-well founded, we may refine this result :

Definition 5.3 T ::: T[P; Q] has the property of unique minimal model in (P; Q) if and only if, for every models 1-1 and v ofT minimal for <P;Q and such that 1-1 =P;Q v, we have IPII' = IPiv (i .e. 1-' =Q v).

Theorem 5.3 a) If T has the property of extended in­ tersection in (P; Q), then T has the property of unique minimal model in (P; Q) .

b) If T is (P; Q)-well founded, then T has the prop­ erty of extended intersection in (P; Q) if and only if T has the property of unique minimal model in (P; Q).

Proof: a) Obvious.

b) Let 1-1 and v be models ofT with 1-1 =P;Q v. There exist models 1-1' and v' of T minimal for <p;Q with (1-' 1 =P;Q l-' 1 IPII'' ~ IPII') and (v' =p;Q v, IPiv' ~ IPiv)· Thus 1-' 1 =P;Q v', and IPII'' = IPiv'·

Example 5.1 T: P(a), P(b) => (P(c) V P(d)), {a:;eb, b=fc, b=fd,c=fd, a=fc, a=fd} {(S1)}.

- Circf(T: P) ::: Circ(T : P) ::: (S1) 1\(Vx (P(x) <::? x=a) (choose p(x) = x=a in AC). - T is not stable for conjunction in P, but T is stable for extended conjunction in P (p"(x) = x =a) . T is P-well founded, and has the property of unique minimal model in P. This example shows that we must use the extended conjunction in theorem 5.2.

Example 5.2 T is:

P(O) v 3x {P(x) 1\ Vy (P(y) => (P(s(y)) 1\ x~s(y)))} , VxVy (s(x)=s(y) => x=y), Vx (s(x)~O) (S2)

- T is not P-well founded (right-hand side of disjunc­ tion) .

- Circ2(T : P):: (S2) 1\Vx (P(x) <=> x=O)

(consistent) .

Circf2(T : P) entails P(O) (choose x = 0 as p(x) in (SACF)), and also -,P(O) (p(x) = x ~ 0), thus it is in­ consistent.

- Thas the property of unique minimal model in P: for every model J.l ofT minimal for <p, IPI~ = {0~}. T does not have the property of extended intersection in P: take D~ = IN= {0, 1, 2, 3, . .. }, s~ successor function in IN, IPI~ = {0}, 0~ = 0; II =p J.l, IPiv = {1, 2, 3, . . . }. J.l and 11 are two models ofT, IPI~ n IPI" = 0, and as T[FALSE] is not true, no model J.l 1 ofT verifies J.l 1 =p J.l and IPI~' ~ IPI~ n IPiv· J.l is minimal for <p, 11 is not (choose IPiv' = {2, 3, 4, ... } ) . 11 -<P J.l, J.l is not mini­ mal for -<P (no model is minimal for -<p ). This example shows that we need the well-foundedness condition in theorem 5.3-b.

Other examples [Moinard and Rolland, 1991] show the importance of the well foundedness condition also for theorem 5.2 b or show that, since theorem 5.2, the main results are false with the first order versions (even with an adapted notion of well-foundedness) . Thus, in the end of this section and in the following section, we deal only with the second order versions. Here we give only a simple example of one problem encountered with first order versions:

Example 5.3 T: P(O) 1\ Vx (P(x) => P(s(x))) .

(cf example 3.1) . It is easy to find two models of Circf1(T : P) with J.l =p 11 and IPI~ ~ IPiv· Choose IN U Z for domain, IPI~ = IN, IPI 11 = IN U Z. The prob­ lem is that J.l =~ 11 is false (IPI~ is not definable with parameters in 11) thus J.l <~ 11 is false.

(Note that 11 =~ J.l is true: IPiv = D~ is definable in JJ).

6 Definability of the circumscribed predicate

Here are two definitions reminded by [Doyle, 1985]. This definability in a theory must not be confused with the definability in a model of definition 2.4.

Definition 6.1 A first order theory T implicitly defines P if and only if whenever J.l and 11 are two models of T such that 11 =p J.l, then they are identical.

Definition 6.2 A first order theory T explicitly defines P if and only if there exists a first order formula~ in L, not involving P, such that: Tl- Vx (P(x) {::} ~) .

The Beth's definability theorem (see [Chang and Keisler, 1973, Doyle, 1985]), states that implicit definability is equivalent to explicit definability. Now, we give a defini­ tion adapted to circumscription with variable predicates:

Definition 6.3 A 2nd order circumscription of P in T with Q varying implicitly defines P if and only if T has the property of unique minimal model in (P; Q).

This is a natural extension of definition 6.1, when "vary­ ing predicates" are involved. As already mentioned, we must use the second order circumscription, but T is a first order theory, and we may consider only first or­ der models. If Q is empty, definition 6.3 coincides with definition 6.1: Circ2(T: P) implicitly defines P ( defini­ tion 6.3) if and only if whenever J.l and 11 are models of Circ2(T : P) such that 11 =p J.l, then J.l = 11 ( cf definition 6.1). So, the theorems 5.2 and 5.3 give:

Theorem 6.1 a) If T is such that Circ2(T: P; Q) is equivalent to Circf2(T: P; Q), then Circ2(T: P; Q) implicitly defines P.

b) If T has the property of extended conjunction in (P; Q) (second order version),then Circ:;i (T: P; Q) im­ plicitly defines P.

c) If Tis (P; Q)-well founded, then ·Circ2(T: P ; Q) implicitly defines P if and only if Circ2(T: P; Q) is equivalent to Circf2(T: P; Q), that is if and only if T is stable for extended conjunction in (P; Q) (second order version).

This gives the answer to the central problem in [Doyle, 1985], asking when P is definable in the circumscribed theory. Also it strengthens the importance of formula (L), given at the end of §4, with standard circumscrip­ tion. (L) does not involve P nor Q, so for well-foundeq theories, (L) gives the explicit second order definition of Pin Circ2(T: P; Q) in all the cases where such a defi­ nition does exist. Note however that (L) being a second order formula is not the ~ of definition 6.2; such a ~ does not necessarily exist because Circ2(T: P; Q) is a second order theory (cf example below) .

Examples In examples 5.1, 5.2 and 5.3, Circ2(T : P) implicitly dE(fines P. We may even give an explicit first order definition (for first or second order circum­ scription) in examples 5.1 (P(x) = x = a) and 5.2 (P(x) = x=O) . In example 5.3, Circ1(T : P) does not implicitly defines P. Also it is a case where no first order explicit definition exists for P in Circ2(T : P) .

7 Definabilization (a stronger circumscription)

Definition 7.1 Def1(T: P; Q), the first order defin­ abilization of P in T with Q varying, adds to T the axiom schema (SADf) : T[p, q] => Vx (P(x) <=> p(x]). The 2nd order version Def2(T: P; Q) adds toT (ADf) :: Vp, q {T(p, q] => Vx (P(x) <=> p(x))}.

Def denotes Def1 or Def2.

Def{T: P; Q) 1- Circf{T: P; Q).

Doyle [1985] uses a similar notion without variable predicate, and calls it "implicit definability" ( cf defini­ tion 6.1). A specific name makes a clear difference be­ tween a theory having this property and the addition of an axiom schema to any theory.

Example 7.1 T: P(a) (Horn theory).

- Circf(T: P) = Circ(T: P) = 'Vx (P(x) <=> x=a). - Def(T: P):: P(a) A Vx (x=a)

(Choose p[x] = x=a, then p[x] = x=x, in (SADf)).

Example 7.2 T: P(a), 3x -.P(x) (cf example 2.1).

- Circf(T : P) :: Circ(T : P) :: Vx (P(x) <=> x = a) A 3x -.P(x). (T is stable for conjunction in P, and IPip = {ap} in every model I' minimalfor <p) .

- Def(T: P)::

p[x] = xjy which gives yja::} Vx (P(x) <=> xjy)).

'Vx (P(x) = x=a) A 3y (yja A Vx (x=a V x=y)). (Choose p[x] = x=a, getting Vx (P(x) = x=a) , then

So definabilization minimizes the extensions of the predicates and the domain, as precised now:

Theorem 7.1 a) If T = T[P, Q] entails T[TRUE,q] for some tuple offormulas q, then Def(T: P ; Q) entails Vx P(x). (TRUE is the tuple (x1 =xt, ... , Xn =xn)).

b) Def(T : P ; Q) 1- Circ(T : P; Q).

{Vx P(x)} u Circ(T : P ; Q) 1- Def(T : P ; Q) .

c) If T 1- T[TRUE, q], then

Def(T : P; Q) :: {Vx P(x)} u Circ(T : P ; Q).

Proof: a) Choose (TRUE, q) as (p,q) in (SADf) or (ADf) (depending of the version).

b) - Obvious.

- {Vx P(x)} U Circ(T : P; Q) is: T U {Vx P(x)}u (SAC). Vx P(x) gives Vx (p[x] ::} P(x~ , thus (SAC) gives (SADf). Adaptation easy for the 2n order version.

Definitions 7.2 We write II#P;QI' (resp. II#P;QI') when 11 =p;Q 1' (resp. 11 =p;Q I') and IPdP j IPilv for at least one i (1 ~ i ~ n).

Theorem 7.2 The models of Def2(T: P; Q) (respec­ tively Def1(T: P ; Q)) are th'e models ofT minimal for #p;Q (respectively #p;Q).

Proofs obvious. As Doyle [1985] has noted, definabiliza­ tion is generally too strong, here is an example:

Example 7.3 T: P(a)::} P(b) , ajb (Horn theory) . - Circf(T : P) = Circ(T: P) = ajbA 'Vx -.P(x)

- Def(T : P) is inconsistent:

choosing p[x] = (x=a V x=b) proves P(a).

choosing p[x] = x=b proves -.P(a), then

- Here are 3 models of T, with the same domain {a, b} : IPIP = {b}, IPI, = {a,b}, IPip' = 0.

1' 1 <p 1' <p 11 . 1'', minimal for <P and -<.p, is a model of Circ(T : P) and Circf(T: P) . I''# PI', I'#PI-' 1 , etc ... There is no model minimal for #P·

8 From domain to predicate circumscription

We will use only the first order versions ( cf §2). Here is the way McCarthy [1980] uses to transform a domain circumscription into a predicate circumscription:

Definition 8.1 U being a new unary predicate symbol, we note: T u = Axiomc(U) A Tu and T<U>:: Circ1(T u: U) U {Vx U(x)}.

£(U) denotes L augmented by U. Axiomc(U) is also AxiomL(u)(U) , as£ and £(U) have the same function symbols, and we will often note Axiom(U).

Theorem 8.1 (McCarthy [1980]) T <U> simulates the domain circumscription ofT: T <U> entails Circd(T). The converse is true: every formula c) in L entailed by T <U>, is entailed by Circd(T). That is, T <U> is a conservative extension of Circd(T).

In a contestation of this method, Etherington and Mer­ cer [1987] argue that consistency is not guaranteed when adding Vx U(x). However, no example is given. We prove that in fact, if an inconsistency has to appear, then it is detected in the circumscription of U:

Theorem 8.2 If Circ1 (T u : U) is consistent , then T <U> is consistent.

Proof: Let 1' be a model of Circ1(T u : U), that is a model of Tu, minimal for<~. We define I'U (1' re­ stricted to U): I'U < 1'; Dpu = IUIPu = IUiw I'U is a model of 'Vx U(x) . 1' is a model of Tu, and so is I'U. Let us suppose that there exists 11, model of T u, with 11 <t I'U. Let 1/J be a formula in Lpu with: 11/Jipu = IUiv (see definitions 3.3, 2.4). We define I'': 1' 1 <u 1', IUIP' = 11/Jipu· Let c) be a prenex formula in Lpu, we may prove by induction on the length of c) that: lc)IPu = lc)UIP [Moinard and Rolland, 1991]. First, this proves that I'' is a model . of Tu . Also, 11 is a model of Axiom L ( U), and so is I'', thus I'' is a model of T u . From: IUIP' = 11/Jipu = 11/Julp, we get 1' 1 <t 1' contra­ dicting the fact that 1' is a model ofT u minimal for <t. So there exists no 11 and I'U is a model of T u minimal for <t, i.e. a model of Circ1(T u : U). If there exists a model (I') of Circ1 (T u : U), there exists a model (l'u) ofT <U>. (Proof simpler for the 2nd order version).

Thus, McCarthy's way of expressing domain circum­ scription into predicate circumscription is justified. One of the main problems in any circumscription is the possi­ bility of unexpected inconsistency. Here, if inconsistency arises it is detected in the circumscribing process, not in the addition of the last axiom Vx U(x) which is harmless.

However, there is a little problem remaining. Any known method of circumscription adds axioms to the initial theory. Here, we leave the initial theory for a while (neither T u nor Circ1(T u : U) entails T), and at the end, we recover T . This does not simplify the matter if we are to automatize the process: for this purpose, we do not want to prove any axiom ofT, we need to know that these formulas are true. One theoretical solution meeting this requirement is to introduce T in the circumscription involved. That is why we propose to circumscribe U in TAT u, instead ofT u alone. As U does not occur in T, we get: Circ1(T u : U) AT:: Circ1(T u AT : U) . As T <U> entails T, we have:

Theorem 8.3 T <U>= Circ1(T uAT: U)u{Vx U(x)} . Again, inconsistency cannot be provoqued by the addition of'Vx U(x).

If T is universal, we get a simplification: T <U>: Circ1(Axiom(U) AT : U) u {Vx U(x)}. (Indeed, T entails Tu) .

With this simulation of domain circumscription, we are closer to the other known kinds of circumscription: we add an axiom schema to T . "More work is done by the circumscription of U" (the final addition ofVx U(x) eliminates fewer models) . As with McCarthy's method, if we had an automatic demonstrator including a pred­ icate circumscriptor (we may tend towards this goal), then we would also have a domain circumscriptor. We cannot avoid adding Vx U(x) if we want to use a predicate circumscription (see [Etherington et al., 1985, Etherington and Mercer, 1987]). But now we show how, using definabilization, we may greatly simplify the pro­ cess and avoid the need for Vx U(x).

Theorem 8.4 T <U>= Circ1(T u AT:U)u{Vx U(x)} =. Def1(T u AT: U).

Proof: T u[TRUE] is Tu[TRUE] A Axiom(TRUE), i.e. TA Axiom(TRUE), i.e. T, and T[TRUE] is T because U does not occur in T. Thus: T u[U] A T[U] entails T u[TRUE] A T[TRUE] . Use theorems 7.1 and 8.1.

Example 8.1 T: P(a) A 3x -.P(x) (cf ex. 2.1, 7.2) .

Axiom(U) =. U(a); Tu =. T u =. U(a) A 3x (U(x) A -.P(x)). Circ1(T u : U) = Tu U {[u[a] A 3x (u[x] A -.P(x)) A Vx (u[x] => U(x))] => Vx (U(x) => u[x]), for any formula u in L(U) }. We choose u[x] = (x=a Y x= y), which gives: (U(y) A -.P(y)) => Vx (U(x) => (x = a Y x = y)). Adding Vx U(x), we get -.P(y) => Vx (x = a Y x = y), which together with P(a) A 3x -.P(x) gives: P(a) A 3y (-.P(y) A Vx (x=a Y x=y), that is Circd(T) (cf example 2.1).

Def1(T u : U) = T u U {[u[a] A 3x (u[x] A -.P(x))] => Vx (U(x) ¢} u(x]), for every formula u in L(U) }. We choose u[x] =. (x =a Y x = y), which gives: -.P(y) => Vx (U(x) ¢} (x=aYx=y)), then we choose u(x] =. x=x, which gives: Vx (x=a Y x=y)) .

Theorem 8.5 If T is universal, then we get a sim­ plification: T <U> =. Def1(T A Axiom(U) : U) =. T A Def1(Axiom(U): U) (U does not appear in T).

The axiom schema of definabilization is simpler than the axiom schema of domain circumscription, so this is an application of definabilization.

9 Conclusion

We have precised the definitions, semantics, and possi­ ble uses, of two kinds of "super circumscriptions". We have given new cases where the circumscription schema may be simplified, a result which is of theoretical and practical importance, as it could be of some help in the process of automatization of circumscription. These re­ sults have solved an old question: when does circum­ scription uniquely define the circumscribed predicates? Our answer is complete for well founded theories. At last, we have precised and justified the passage from do­ main circumscription to predicate circumscription. We have shown that this passage is safe: it cannot bring. in­ consistancy. Also we have given two new methods. The first one enhances the role of predicate circumscription, which is useful if we want to use an automatic predicate circumscriptor for domain circumscription. The second one greatly simplifies the schemas involved.

Acknowledgement We are glad to thank Philippe Besnard who initiated this work.