Definition. Let A(P) be a formula of second order logic, where P is
a tuple of some of the free predicate symbols in A(P).
Let E(P,x) be a wff in which
P and a tuple x of individual variables occur free. The circumscription
of E(P,x) relative to A(P) is the formula 
defined by
[We are here writing A(P) instead of 
for brevity
and likewise writing E(P,x) instead of
].
Likewise the quantifier 
stands for 
.
A(P) may have embedded quantifiers.
Circumscription is a kind of minimization,
and the predicate symbols in A(P) that are not in P itself act as
parameters in this minimization. When we wish to mention
these other predicates we write 
and 
where
Q is a vector of predicate symbols which are not allowed to be varied.
There are two differences between this and (McCarthy 1980). First, in that paper E(P,x) had the specific form P(x). Here we speak of circumscribing a wff and call the method formula circumscription, while there we could speak of circumscribing a predicate. We still speak of circumscribing the predicate P when E(P,x) has the special form P(x). Formula circumscription is more symmetric in that any of the predicate symbols in P may be regarded as variables, and a wff is minimized; the earlier form distinguishes one of the predicates themselves for minimization. However, formula circumscription is reducible to predicate circumscription provided we allow as variables predicates besides the one being minimized.
Second, in definition (1) we use an explicit quantifier for the predicate
variable 
whereas in (McCarthy 1980), the formula was a schema.
One advantage of the present formalism is that now is the
same kind of formula as A(P) and can be used as part of the axiom for
circumscribing some other wff.
In some of the literature, it has been supposed that nonmonotonic reasoning involves giving all predicates their minimum extension. This mistake has led to theorems about what reasoning cannot be done that are irrelevant to AI and database theory, because their premisses are too narrow.
