There is an intuition that not all human reasoning can be translated into deduction in some formal system of mathematical logic, and therefore mathematical logic should be rejected as a formalism for expressing what a robot should know about the world. The intuition in itself doesn't carry a convincing idea of what is lacking and how it might be supplied.
We can confirm part of the intuition by describing a previously unformalized mode of reasoning called circumscription, which we can show does not correspond to deduction in a mathematical system. The conclusions it yields are just conjectures and sometimes even introduce inconsistency. We will argue that humans often use circumscription, and robots must too. The second part of the intuition--the rejection of mathematical logic--is not confirmed; the new mode of reasoning is best understood and used within a mathematical logical framework and co-ordinates well with mathematical logical deduction. We think circumscription accounts for some of the successes and some of the errors of human reasoning.
The intuitive idea of circumscription is as follows: We know some objects in a given class and we have some ways of generating more. We jump to the conclusion that this gives all the objects in the class. Thus we circumscribe the class to the objects we know how to generate.
For example, suppose that objects a, b and c satisfy the predicate P and that the functions f(x) and g(x,y) take arguments satisfying P into values also satisfying P. The first order logic expression of these facts is
The conjecture that everything satisfying P is generated from a, b and c by repeated application of the functions f and g is expressed by the sentence schema
where is a free predicate variable for which any predicate may be substituted.
It is only a conjecture, because there might be an object d such that P(d) which is not generated in this way. (4) is one way of writing the circumscription of (2). The heuristics of circumscription--when one can plausibly conjecture that the objects generated in known ways are all there are--are completely unstudied.
Circumscription is not deduction in disguise, because every form of deduction has two properties that circumscription lacks--transitivity and what we may call monotonicity. Transitivity says that if and , then . Monotonicity says that if (where A is a set of sentences) and , then for deduction. Intuitively, circumscription should not be monotonic, since it is the conjecture that the ways we know of generating P's are all there are. An enlarged set B of sentences may contain a new way of generating P's.
If we use second order logic or the language of set theory, then circumscription can be expressed as a sentence rather than as a schema. In set theory it becomes.
but then we will still use the comprehension schema to form the set to be substituted for the set variable .
The axiom schema of induction in arithmetic is the result of applying circumscription to the constant 0 and the successor operation.
There is a way of applying circumscription to an arbitrary sentence of predicate calculus. Let p be such a sentence and let be a predicate symbol. The relativization of p with respect to (written ) is defined (as in some logic texts) as the sentence that results from replacing every quantification that occurs in p by and every quantification that occurs in p by . The circumscription of p is then the sentence
This form is correct only if neither constants nor function symbols occur in p. If they do, it is necessary to conjoin for each constant c and for each single argument function symbol f to the premiss of (5). Corresponding sentences must be conjoined if there are function symbols of two or more arguments. The intuitive meaning of (5) is that the only objects satisfying P that exist are those that the sentence p forces to exist.
Applying the circumscription schema requires inventing a suitable predicate to substitute for the symbol (inventing a suitable set in the set-theoretic formulation). In this it resembles mathematical induction; in order to get the conclusion, we must invent a predicate for which the premise is true.
There is also a semantic way of looking at applying circumscription. Namely, a sentence that can be proved from a sentence p by circumscription is true in all minimal models of p, where a deduction from p is true in all models of p. Minimality is defined with respect to a containment relation . We write that if every element of the domain of M1 is a member of the domain of M2 and on the common members all predicates have the same truth value. It is not always true that a sentence true in all minimal models can be proved by circumscription. Indeed the minimal model of Peano's axioms is the standard model of arithmetic, and Gödel's theorem is the assertion that not all true sentences are theorems. Minimal models don't always exist, and when they exist, they aren't always unique.
(McCarthy 1977) treats circumscription in more detail.