Axiomatic Aspects of Default Inference

This paper studies axioms for nonmonotonic consequences from a semantics-based point of view, focusing on a class of mathematical structures for reasoning about partial information without a predefined syntax/logic. This structure is called a default structure. We study axioms for the nonmonotonic consequence relation derived from extensions as in Reiter's default logic, using skeptical reasoning, but extensions are now used for the construction of possible worlds in a default information structure. In previous work we showed that skeptical reasoning arising from default-extensions obeys a well-behaved set of axioms including the axiom of cautious cut. We show here that, remarkably, the converse is also true: any consequence relation obeying this set of axioms can be represented as one constructed from skeptical reasoning. We provide representation theorems to relate axioms for nonmonotonic consequence relation and properties about extensions, and provide one-to-one correspondence between nonmonotonic systems which satisfies the law of cautious monotony and default structures with unique extensions. Our results give a theoretical justification for a set of basic rules governing the update of nonmonotonic knowledge bases, demonstrating the derivation of them from the more concrete and primitive construction of extensions. It is also striking to note that proofs of the representation theorems show that only shallow extensions are necessary, in the sense that the number of iterations needed to achieve an extension is at most three. All of these developments are made possible by taking a more liberal view of consistency: consistency is a user defined predicate, satisfying some basic properties.


Introduction
Reasoning in general is concerned with drawing conclusions from a set of premises. Mathematical reasoning is monotonic, in the sense that if the set of premises becomes bigger, the set of conclusions also grows larger (or stays the same). Reasoning in daily life, however, is nonmonotonic, because conclusions drawn earlier due to the lack of information may have to be withdrawn later in light of new information. This nonmonotonic phenomenon can be avoided by putting time-stamps on conclusions. Thus, the conclusions drawn earlier and the conclusions withdrawn later have different time-stamps and are treated as different conclusions. The cost of this temporal approach, which will not be discussed further here, is the "frame problem", referring to the issue of keeping track of much of background information that stays unchanged as time goes on.
Nonmonotonicity arises when explicit time-stamps are avoided when we are in fact dealing with time-sensitive, partial information. For example, in databases data are not time-stamped, but they evolve continuously over time.
A well-known formalism for nonmonotonic reasoning is Reiter's default logic [18], in which the so-called extension construction was introduced as a important method to extend current knowledge using default rules. Reiter's treatment is syntactic, in the sense that default rules are used as extended proof rules for first order logic, allowing more conclusions derived provided that the global property of consistency is not violated. It should be of no surprise that this treatment has caused some anomalies, because first order logic was invented for mathematical reasoning rather than commonsense reasoning.
There is a conceptually cleaner view of default reasoning under the paradigm of modal logic with Kripke structure as models [26]. We can think of a state in a Kripke structure as a state of knowledge/information. Possible worlds represent hypothetical worlds which may evolve from a given state. Modal logic can then be adapted for the purpose of reasoning about belief. The role of default is now relegated to the semantic structure as a concrete way for constructing possible worlds using extensions. Nonmonotonic reasoning in this new setting becomes model-checking: given a state (a knowledge base) in the Kripke structure and a belief formula (expressed in modal logic), determine whether or not the belief is supported. Nonmonotonicity corresponds to the fact that a belief supported in the current state may become unsupported in a possible future state.
This semantic view of default reasoning is developed in detail in the so-called default domain theory [19]. The idea is to use Scott's information system [21] as the basic semantic structure for representing information states (the underlying Kripke structure), extended with default rules in order to construct possible worlds. Here are some specific achievements of default domain theory.
-Power default reasoning. Domain theory is a powerful and elegant framework developed by Scott and others for the denotational semantics of programming languages. A routine practice in domain theory is that an object of one type can be embedded/projected to different type in order to facilitate a more appropriate treatment. The idea of power default reasoning [29] is to encode default rules in a higher-order setting so that a nonmonotonic operator at the base level induces a better behaved operator in the higher-order space of Smyth powerdomain. Under power default reasoning, the extension construction has nice structural properties. For example, one can show a dichotomy theorem [29] which states that with respect to a set of default constraints on a Scott domain D lifted as power defaults Γ on the Smyth powerdomain P(D), an element either has a safe, unique Γ -extension, or else the multiple Γ -extensions will all be singleton generated. The Extension Splitting Theorem [29] states that any extension of the union of two compact open sets can be split into the union of two corresponding extensions. This allowed us to prove, among other things, the law of reasoning by cases and the law of cautious monotony, as discussed in [12]. Note that the cases law and cautious monotony law do not hold for standard propositional default logic, which is among the anomalies of default logic discussed in the literature. -Complexity. These structural properties have direct algorithmic consequences.
Based on the Dichotomy Theorem, an algorithm [28] has been developed for skeptical normal default inference in propositional logic to show that the problem is complete for co-NP(3), the third level of the Boolean hierarchy. This contrasts favorably with standard propositional default reasoning based on default logic, which was proved to be Π P 2 -complete [10,4]. -Semantics of disjunctive logic programming. Our domain-theoretic investigation to logic programming started with the basic observation that the information system representation of domains [21] bears a remarkable similarity to the syntax of definite logic programs (the so-called Horn clauses).
Our work [20] shows that a general disjunctive logic programming paradigm can be developed on coherent domains -algebraic cpos on which the intersection of any two compact open sets remains compact open. From the domain-theoretic point of view, these are very general spaces which contain several prominent categories already (such as Scott domains and SFP domains). More concretely, a disjunctive logic program can be regarded as a sequent structure. Such a structure generates spatial locales (the so-called pointless topology [11]), which provide models and proof rules for which completeness is guaranteed [3].
In this paper we continue the semantics-based study of nonmonotonic inference by providing representation theorems for the skeptical nonmonotonic consequence relation. We show that an abstract nonmonotonic relation satisfies the law of cautious monotony (among other reasonable axioms) if and only if it can be generated from a set of normal default rules with unique extensions. We then provide some preliminary discussions on a possible categorical setting in which to discuss properties of these constructions. These developments are made possible by taking a less restricted view of consistency: we view consistency as a user defined predicate, satisfying some basic properties, as precisely captured by information systems -Con. There is no prescribed global notion of consistency; a set of tokens can be consistent in one information system while inconsistent in another. We believe that the meaning for "paraconsistency" ultimately lies in this local, user-defined interpretation.
Related work. The idea of extension was introduced by Reiter [18]. Makinson [13] and others [9] have provided extensive study of many axioms discussed here, sometimes from the belief-revision point of view. Marek, Nerode, and Remmel [14] have studied structures similar to default information structures, from a recursion-theoretic point of view. The first representation result similar to the ones studied here was given in [27]. Hitzler and Seda [22,23], in a sequence of papers, studied logic programming semantics using the tools of Topology and Analysis. The edited volume [25] contains a number of discussions on the role of partiality of information for commonsense reasoning. These are philosophically allied to our domain-theoretic approach to logic programming and nonmonotonic reasoning. Fitting [5,6,7] was among the first ones to introduce order to the study of logic programming in a systematic way. There are also other kinds of representation results in the literature. For example, Marek, Treur, and Truszczynski [15] studied the problem of when a family of theories can be represented as the extension family of normal defaults. Our work differs from this in that we relate default theory to axioms for the nonmonotonic consequence relation, establishing connections between two independent paradigms.

Default domain theory
This section provides an overview of the basic structure of default domain theory -default information structures. We refer to [21,30] for more discussion on information systems, and [1,2,16] for background on nonmonotonic reasoning.

Information systems
In order to study the properties of nonmonotonic systems, let's first take a look at monotonic systems, as captured in Scott's information systems.
An information system consists of a set A of tokens, a subset Con of the set of finite subsets of A, denoted as Fin(A), and a relation ⊢ between Con and A. The subset Con on A is often called the consistency predicate, and the relation ⊢ is called the entailment relation. Both the consistency predicate and the entailment relation satisfy some axioms due to Tarski, made precise in the following definition.
Moreover, the consistency predicate and entailment relation satisfy the following properties: Although monotonicity for ⊢ is not explicitly given, it is a derivable property. Suppose Y ⊢ a and Y ⊆ X with X ∈ Con. By (4), X ⊢ b for every b ∈ Y . Now apply (5) and we get X ⊢ a. Thus monotonicity is an inherent property of ⊢: The notion of consistency can be easily extended to arbitrary token sets by enforcing compactness, i.e., a set is consistent if every finite subset of it is consistent. By overloading notation, we write X ∈ Con when every finite subset of X is consistent.
The monotonicity of ⊢ induces a monotonic operator F : Con → Con for an information system (A, Con, ⊢): The reflexivity property (4) implies that F is inflationary, in the sense that X ⊆ F (X) for any X ⊆ A. The continuity of F follows from the finiteness (or compactness) of ⊢ on its left-hand-side.
From these we can easily show that for any given subset X of tokens, F has a least fixed-point containing X. F is in fact a closure operator (often denoted as Cn in the literature), with the following defining properties: Idempotency of F follows from the transitivity (5) of ⊢. To show the nontrivial containment F (F (X)) ⊆ F (X), let a ∈ F (F (X)). This means that for and so a ∈ F (X), as required.
The information states of an information system are precisely sets of the form F (X) with X ∈ Con, where Con is understood in the generalized sense to include infinite sets through the compactness condition. Moreover, the set of all information state {F (X) | X ∈ Con} is precisely the set of fixed-points of F .
The importance of information systems lies in the fact that they provide a concrete representation of Scott domains 2 . 1 Here we deliberately dropped the X ∈ Con condition. One can, as in logic, define Con in such a way that X ∈ Con if and only if X ⊢ a for some a ∈ A, as suggested by Peter Aczel in a personal communication. However, this "logical" definition is more limited, in that it insists on the whole set A to be inconsistent. 2 Exactly what a Scott domain is need not concern us here. It should suffice to say that a Scott domain is a complete lattice with the top element removed.

Theorem 1. (Scott) For any information system A, the collection of its information states |A| under inclusion forms a Scott domain. Conversely, every Scott
domain is order-isomorphic to the partial order of information states of some information system.

Normal default structures
We now introduce the main definitions of default domain theory. Normal default structures are information systems extended with a set of default rules of the form X : a a , with X a finite consistent set, and a a single token of the underlying information system. The idea of a default rule is that one can generate models (states of belief) by finding X as a subset of tokens in a state under construction, checking that a is consistent with the current state, and then adding the token a.

Definition 2. A normal default structure is a tuple
If each default is of the form ∅ : a a , we call the default structure precondition free.
Extensions are a key notion related to a default structure. An extension of an information state x is intuitively an information state y extending x, constructed in such a way that everything in y reflects an agent's belief expressed by defaults. If the current situation is x, then because it is a partial model, it may not contain enough information to settle an issue (either positively or negatively). Extensions of x are partial models containing at least as much information as x, but the extra information in an extension is only plausible, not factual.
The following definition is just a reformulation, in information-theoretic terms, of Reiter's own notion of extension in default logic.
Definition 3. Let A = (A, Con, ∆, ⊢) be a default structure, and x an information state of the information system (A, Con, ⊢). For any S ⊆ A, define Φ(x, S) to be the union i≥0 φ(x, S, i), where (note that F is given in the previous subsection) Call y an extension of x if Φ(x, y) = y. In this case we also write x ǫ A y, with the subscript omitted when the default structure under consideration is clear.
Basic properties of extensions are stated next, which will be used in the proof of main representation theorems in the next section. These properties are parallel to those for Reiter's default logic, and so their proofs are omitted.
Theorem 2. Let A = (A, Con, ∆, ⊢) be a normal default structure, and x, y information states of the information system (A, Con, ⊢). We have 1. x has at least one extension. 2. if x ǫ y then y ⊇ x. 3. if x ǫ y, then y ǫ z if and only if y = z for any information state z. 4. for any information state z, if x ǫ y and x ǫ z, then either y = z or y∪z ∈ Con.
In terms of possible world semantics, normal default structures give rise to Kripke structures in which every state has either a transition to a different state or loops to itself. Moreover, if a state does contain a transition to a new state, then such future states are pairwise incompatible (there is no common future states).

Axioms for nonmonotonic consequence
There is little disagreement about what properties should a (monotonic) entailment relation have: these were given by Tarski, as captured in information systems. The situation is quite different for the nonmonotonic consequence relation. To motivate the discussion, we first take a look at the skeptical nonmonotonic consequence relation determined by a normal default information structure with a trivial ⊢. The default structures will have only three components, as (A, Con, ∆), with ⊢ understood as X ⊢ a if and only if a ∈ X. The closure operator F will now be the identity function: F (X) = X. Definition 4. The skeptical nonmonotonic consequence relation |∼ A with respect to a normal default structure (A, Con, ∆) is defined as X |∼ A a if a belongs to every extension y of X. Here X is a finite consistent subset of A, and a ∈ A.
Since extensions exist in normal default structures, we have X |∼ A a ⇐⇒ a ∈ {y | Xǫ A y}.
The next example shows that |∼ A is not monotonic: X |∼ A a and X ⊆ Y does not imply Y |∼ a. Failing monotonicity, what other properties can we say about |∼ A ? For sake of brevity, we write, for finite sets X and Y , X |∼ Y to mean that X |∼ b for every b ∈ Y . Certainly we have X |∼ X for every consistent finite set X. The only non-trivial property we can say about |∼ in general seems to be cautious cut: X |∼ T & T, X |∼ Y ⇒ X |∼ Y. We call it cautious cut because the standard cut axiom takes the following form: This is equivalent to cautious cut when monotonicity is assumed, but cut is stronger in the nonmonotonic case.
We need the following property to prove cautious cut.
Lemma 1. For any finite consistent sets P, Q of a default structure (A, Con, ∆), if P ǫ R and Q ⊆ R, then (P ∪ Q) ǫ R.
A proof for this can be found in [27]. Proof. Let X |∼ A T and T, X |∼ A Y for finite consistent sets X, T, Y . We have We need to show that Y ⊆ {e | Xǫ A e}. Let e be an extension of X. We have T ⊆ e since X |∼ A T . By Lemma 1, e is an extension of X ∪ T . However, Y is a subset of every extension of X ∪ T ; in particular, Y ⊆ e. Therefore, Y is a subset of every extension of X, as required for X |∼ A Y . 2 We take the properties satisfied by |∼ A as the minimal set of properties that any nonmonotonic consequence relation should satisfy. This brings us to the notion of abstract nonmonotonic system. Definition 5. An abstract nonmonotonic system is a triple (A, Con, |∼), where Con is a collection of finite subsets X of A, called the consistent sets, |∼ is a subset of Con × Con, called the relation of nonmonotonic entailment, which satisfies the following axioms: Note that Axiom 4 is reflexivity, and Axiom 5 is cautious cut. The rest of the properties are routine. Axioms 4 and 6 together allow us to view a nonmonotonic system as one generated from instances of the form X |∼ {a}. One can then define X |∼ Y if and only if X |∼ {b} for every b ∈ Y . X |∼ ∅ is vacuously true. [27]). For any a normal default structure (A, Con, ∆), (A, Con, |∼ A ) is an abstract nonmonotonic system, where the relation |∼ A is given in Definition 4.

Theorem 4 (Zhang and Rounds
We will not go through the formality of the proof here, but only note that cautious cut follows from Theorem 3, and Axiom 3 follows from the fact that extensions always exist and each one of them is a consistent set.

Representation theorems
Theorem 4 says that any normal default structure determines an abstract nonmonotonic system -a nonmonotonic relation satisfying a minimal set of properties including reflexivity and cautious cut.
The more interesting question is the converse: is it true that every abstract nonmonotonic system can be represented concretely as one derived from a normal default structure? In other words, for each abstract nonmonotonic system (A, Con, |∼), is there a normal default structure (B, Con, ∆) such that |∼ = |∼ B ?
We show that the converse of Theorem 4 is indeed true. Such a representation result bears much resemblance to the fundamental Cayley's Theorem for finite groups, saying that any finite group is isomorphic to a permutation group. The next theorem says that every abstract nonmonotonic relation is determined by some normal default structure. This shows that the framework of default rules with extensions, although a concrete nonmonotonic formalism, is expressive enough to represent any reasonable nonmonotonic consequence relation.
Theorem 5. Let (A, Con, |∼) be an abstract nonmonotonic system. There is a normal default structure B = (B, Con * , ∆) satisfying the following properties: for any X ⊆ B, X ∈ Con if and only if X ⊆ A and X ∈ Con * , 3. for every X, Y ∈ Con, X |∼ Y if and only if X |∼ B Y.
Conditions 2 states that Con * is a conservative extension of Con, and condition 3 says that |∼ B is a conservative extension of |∼. Example 2. An example will be helpful to illustrate the idea of the proof. Consider the abstract nonmonotonic system (A, Con, |∼) with A = {a, b}, Con = 2 A and |∼ generated by requiring ∅ |∼ {a} and ∅ |∼ {b} (i.e., reflexivity and cautious cut is always assumed; note that we have neither {a} |∼ {b}, nor {b} |∼ {a}). We would like to construct a default structure B = (B, Con * , ∆) which determines this nonmonotonic entailment relation 3 .
The idea is to introduce, for each consistent set X, a new token [X], similar to the powerset construction in automata theory. The consistency predicate Con * is defined in such a way that it extends Con, but new tokens are inconsistent with each other. Moreover, for a set containing a new token [X] to be consistent, every other element in the set must be a nonmonotonic consequence of X. Therefore, the consistent sets in Con * are sets (as well as their subsets) of the form We now describe a general procedure to construct the required default structure B = (B, Con * , ∆) from an abstract nonmonotonic system (A, Con, |∼).
The token set B is A∪{[X] | X ∈ Con}. The idea is to introduce a new token for each consistent set X and use sets of given tokens to encode new tokens. Note that we need only introduce [X] for (consistent) finite sets X in the powerset of A here, even though A may be infinite.
We have two kinds of default rules. One is for each X ∈ Con, and the other is {[X]} : a a for each nonmonotonic instance X |∼ a with a ∈ X. Thus For any subset W of B, W ∈ Con * if and only if all of the following three conditions hold: 1. W ∩ A ∈ Con, i.e., the old tokens in W form a consistent set in Con;

at most one token of the form [X] is in
It is straightforward to check that the consistency predicate defined this way has the required properties. Each individual token is indeed consistent. For any subset Z of W ∈ Con * , we have Z ∈ Con * by examining the three conditions above.
The remaining task is to show that the default structure B has the properties as stated in Theorem 5. This will be achieved in several lemmas.
An auxiliary notation is needed. We define X := {t | X |∼ {t}}, i.e., X is the set of all nonmonotonic consequences of X. Lemma 2. Let (A, Con, |∼) be an abstract nonmonotonic system. We have, for any consistent set X, Proof. We prove the non- Given any a in X, we can rewrite this as The axiomatization of the nonmonotonic operator ( ) has been studied in depth, notably by Makinson and others. Here we only indicate that it is not monotonic (of course), and it is not necessarily true that X = X.
Lemma 3. Let P, Q be finite consistent sets in an abstract nonmonotonic system (A, Con, |∼) and B = (B, Con * , ∆) the corresponding default structure. If Proof. It is easy to see that the set Q ∪ {[Q]} is consistent with respect to Con * .
We need to verify the defining equality ρ(Q) = i≥0 φ(P, ρ(Q), i). By definition, The only applicable rules in ∆ are of the form X : [X] [X] with X ⊆ P ; but only [Q] will meet the consistency requirement. Therefore, φ(P, ρ(Q), 1) = P ∪ The second iteration φ(P, ρ(Q), 2) is the set This time all and only tokens in Q \ Q gets added to φ(P, ρ(Q), 1), since the applicable default rules are of the form This proof conveys the additional information that extensions such as ρ(Q) can be attained in two iterations. This offers an explanation of why default reasoning need not be hard (see [24] as well), because deep iterations for building extensions may not be needed. Proof. Suppose W is an extension of P . We have W = P since otherwise P : [P ] [P ] is applicable, forcing [P ] to be added to W .
By design (of ∆), the first token added to φ(P, W, 1) must be of the form The consistency constraint requires that P ⊆ Q. It also requires that no other tokens of the form [X] belong to W . So in the second iteration one can (and must) apply all defaults of the form Proof (Theorem 5). The first two items are obvious from the definition of B. We show the third item: for every X, Y ∈ Con, X |∼ Y if and only if X |∼ B Y. Let X, Y be consistent subsets of A such that X |∼ Y . By Lemma 3 and Lemma 4, extensions of X in B are precisely sets of the form Q ∪ {[Q]} with Q ⊆ X ⊆ Q. For any such Q, we have, by Lemma 2, X ⊆ Q. Therefore Y ⊆ Q and Y is a subset of every extension of X in B. This proves X |∼ B Y.
Suppose, on the other hand, X |∼ B Y for subsets X, Y of A. By Lemma 3 and Lemma 4, This means Y ⊆ X, by Lemma 2. Therefore, X |∼ Y . 2

Cautious monotony and unique extension
The axiom of cautious monotony, considered by Gabbay, Kraus, Lehmann, and Magidor and others [8,12], takes the form (We will drop the { } for singletons and write X |∼ a & X |∼ b ⇒ X, a | ∼ b as well.) This axiom intuitively says that a nonmonotonic consequence can always be added as a premise without affecting what was originally entailed.
It is arguably one of the most fundamental assumptions for a nonmonotonic knowledge base to work: if your knowledge base X can support several beliefs, say a, b, then you should be able to adjoin these beliefs to enlarge the knowledge base to X ∪{a, b}. Now, applying the reflexivity axiom -Axiom 4 of Definition 5, we get X ∪ {a} |∼ b.
An easy induction shows that cautious monotony is equivalent to the more general form X |∼ Y & X |∼ Z ⇒ X, Y |∼ Z, with X, Y, Z being finite (consistent) sets. If an abstract nonmonotonic system (A, Con, ∆) satisfies cautious monotony, we will call it a cumulative nonmonotonic system.
Here is an example showing that the skeptical nonmonotonic consequence relation derived from a generic default structure need not satisfy cautious monotony.
Example 3. Consider the default structure (A, Con, ∆) with There is a unique extension for ∅: {a, b}. ). This prevents an existing consequence (such as a) from being present in all extensions of the changed situation.
Cautious monotony, however, does hold when extensions are unique. The reason is that in this case, a nonmonotonic consequence can be added without changing the (unique) extension.
Theorem 6 (Zhang and Rounds [27]). Let (A, Con, ∆) be a normal default structure such that extensions are unique for any information state. Then the derived nonmonotonic consequence relation |∼ A is cumulative, i.e., it satisfies cautious monotony.
In the rest of the section we show (which is new) that the converse of the above is also true, leading to another representation result.
Theorem 7. For any cumulative nonmonotonic system (A, Con, |∼), there exists a normal default structure B = (B, Con * , ∆) with the following properties: for any X ⊆ B, we have X ∈ Con if and only if X ⊆ A and X ∈ Con * , -for every X, Y ∈ Con, it is the case that X |∼ Y if and only if X |∼ B Y, -there exists a unique extension for every information state of B.
Since any cumulative nonmonotonic system is an abstract nonmonotonic system in the sense of Definition 5, Theorem 5 tells us that it can be represented by a normal default structure. The point of Theorem 7 is that, we can require the normal default structure to have unique extensions, which the construction given earlier for Theorem 5 does not provide 4 .
A lemma is needed to support the new construction.
Lemma 5. Let (A, Con, |∼) be a cumulative nonmonotonic system. For finite consistent sets P, Q of A, if Q ⊆ P ⊆ Q, then P = Q.
Proof. Lemma 2 gives P ⊆ Q and we need to show the other way round. Suppose Q |∼ a. We need to show that P |∼ a. Since P ⊆ Q, we have Q |∼ P . Applying cautious monotony to Q |∼ P and Q |∼ a, we get P ∪ Q |∼ a. This is the same as P |∼ a since Q is a subset of P , by assumption. 2 One can see from the proof of Theorem 5 that there is a 1-1 correspondence among sets Qs with Q ⊆ P ⊆ Q and extensions of P , labeled by [Q]. The previous lemma suggests that we should now collect all such [Q]s in one extension, with the proviso that Q ⊆ P and P = Q. This is in fact the key idea for the proof of Theorem 7. Let (A, Con, |∼) be an abstract nonmonotonic system satisfying cautious monotony. Define B = (B, Con * , ∆), where -W ∈ Con * if and only if all of the following three conditions hold: 1. W ∩ A ∈ Con, i.e., the old tokens in W form a consistent set in Con; 2. for each pair [X], [Y ] of (new) tokens in W , X = Y ; 3. if [X] ∈ W , then X |∼ W ∩ A.
Note that the difference from the previous construction is in the consistency predicate Con * . Two distinct tokens [X], [Y ] need not to be in conflict, as long as X = Y . Theorem 7 is now an immediate consequence of the following lemma.
Lemma 6. Let B = (B, Con * , ∆) be the normal default structure for a cumulative nonmonotonic system (A, Con, |∼) (as given in the procedure above). Every finite consistent set P ⊆ A has a unique extension, which is Proof. As a sanity check, we see that δ(P ) is indeed consistent. Suppose W is an extension of P in B. We show that W = δ(P ). By definition, W satisfies the equality W = i≥0 φ(P, W, i). Clearly W = P , since P : [P ] [P ] is one of the default rules in ∆. But the first default rules applied must add tokens of the form [X], so W contains a token of the form [Q], with Q ⊆ P . Consistency requires further that P ⊆ Q, since P ⊆ W . By Lemma 5, Q ⊆ P and P ⊆ Q implies Q = P . [R] may be applicable, with R = P and R ⊆ P (note the relaxed condition here). This shows φ(P, W, 3) = δ(P ), and there is no additional applicable default rules from now on. 2