 In terms of consequence relations, circumscription allows us to define, for each predicate P, a non-monotonic relation \(A(P) \nc \phi\) that holds precisely when \(A^{\star}(P) \vDash \phi\). (This basic form of circumscription has been generalized, for, in practice, one needs to minimize the extension of a predicate, while allowing the extension of certain other predicates to vary.) From the point of view of applications, however, circumscription has a major computational shortcoming, which is due to the nature of the second-order language in which circumscription is formulated (see the entry on  Second-order and Higher-order Logic  for details). The problem is that SOL, contrary to FOL, lacks a complete inference procedure: the price one pays for the greater expressive power of SOL is that there are no complete axiomatizations, as we have for FOL. It follows that there is no way to list, in an effective manner, all SOL validities, and hence to determine whether \(A(P) \nc \phi\). 