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.