In order to keep the example short we will take into account only the following facts from the earlier section on flying.
Their conjunction is taken as A(ab,flies). This means that what entities satisfy ab and what entities satisfy flies are to be chosen so as to minimize . Which objects are birds and ostriches are parameters rather than variables, i.e. what objects are birds is considered given.
We also need an axiom that asserts that the aspects are different. Here is a straightforward version that would be rather long were there more than three aspects.
We could include this axiom in A(ab,flies), but as we shall see, it won't matter whether we do, because it contains neither ab nor flies. The circumscription formula is then
which spelled out becomes
A(ab,flies) is guaranteed to be true, because it is part of what is assumed in our common sense database. Therefore (42) reduces to
Our objective is now to make suitable substitutions for and so that all the terms preceding the in (43) will be true, and the right side will determine ab. The axiom A(ab,flies) will then determine flies, i.e. we will know what the fliers are. is easy, because we need only apply wishful thinking; we want the fliers to be just those birds that aren't ostriches. Therefore, we put
isn't really much more difficult, but there is a notational problem. We define
which covers the cases we want to be abnormal.
Appendix A contains a complete proof as accepted by Jussi Ketonen's (1984) interactive theorem prover EKL. EKL uses the theory of types and therefore has no problem with the second order logic required by circumscription.