The form of circumscription described in this paper generalizes
an earlier version called minimal inference. Minimal inference
has a semantic counterpart called minimal entailment, and both are
discussed in (McCarthy 1977) and more extensively in (Davis 1980).
The general idea of minimal entailment is that a sentence q is minimally
entailed by an axiom A, written , if q is true in all
minimal models of A, where one model if is considered less than another
if they agree on common elements, but the domain of the larger many contain
elements not in the domain of the smaller.
We shall call the earlier form domain circumscription to contrast it
with the predicate circumscription discussed in this paper.
The domain circumscription of the sentence A is the sentence
where is the relativization of A with respect to
and
is formed by replacing each universal quantifier
in A by
and each existential quantifier
by
.
is the conjunction of sentences
for each constant
a and sentences
for each function
symbol f and the corresponding sentences for functions of higher
arities.
Domain circumscription can be reduced to predicate circumscription
by relativizing A with respect to a new one place predicate
called (say) all, then circumscribing all in ,
thus getting
Now we justify our using the name all by adding the axiom
so that (20) then simplifies precisely to (19).
In the case of the natural numbers, the domain circumscription of true, the identically true sentence, again leads to the axiom schema of induction. Here Axiom does all the work, because it asserts that 0 is in the domain and that the domain is closed under the successor operation.