The characterization of the semantics of
NAT's in terms of second order logic
theories including circumscription formulas
and proposition 1 in [Lifschitz1995]
allow us to prove the equivalence between
the following axiom sets
.
Now, we use several rules for computing circumscription described in [Lifschitz1993]. The first equivalence below can be proved using formula (19) and proposition 2 in [Lifschitz1993]. The second equivalence uses formula (19) and proposition 3 in that paper.
Using the equivalence (27) in
section 3.2 of [Lifschitz1993], we can
prove that 
is
equivalent to the following formula, which
does not depend on better.
Finally, predicate completion [Lifschitz1993] give us the result of the theorem.
Theorem 1 shows that the nested abnormality
theory described by 
is
equivalent to the second order theory
whose axioms are 
, and
. This means that using theorem
proving methods for first order
logic we can
decide the selectability of any situation
with respect to the strategy described by
axioms to . For
example, we can prove that action
Move(A,T) is selectable at 
(i.e.,
),
but action Move(C,T) is not (i.e.,
).
