An axiomatic approach that accounts for examples that come up in logic programming, symbolic computation, affine geometry, and elsewhere is presented. It is shown that if disjunction behaves in an intuitionistic fashion, notions of canonical form for positive constraints can be systematically extended to include negative constraints. As a consequence, completeness theorems involving positive and negative constraints can be proven in a general setting for constraint propagation.>

Parallel algorithms and computational complexity results are given for two problems; computing the relative complement of terms and antiunification. The concepts of antiunification and relative complement are useful for theorem proving, logic programming, and machine learning. The relative complement problem is shown to be NP-complete.>

Gödel's paper on formally undecidable propositions [3] raised the possibility that finite combinatorial theorems could be discovered which are independent of powerful axiomatic systems such as first-order Peano Arithmetic. An important advance was made by J. Paris in the late 1970's; building on joint work with L. Kirby, he used model-theoretic techniques to investigate arithmetic incompleteness and proved theorems of finite combinatorics which were unprovable in Peano Arithmetic [11]. The Paris-Harrington paper [13] gives a self-contained presentation of the proof that a straightforward variant of the familiar finite Ramsey Theorem is independent of Peano Arithmetic. In this paper, we consider a simple finite corollary of a theorem of infinite combinatorics of Erdös and Rado [1] and show it to be independent of Peano Arithmetic. This formulation avoids the Paris-Harrington notion of relatively large finite set and deals with a generalized notion of partition. This shift of focus also provides for simplifications in the proofs and directly yields a level-by-level analysis for subsystems of Peano Arithmetic analogous to that in [12]. We have tried to provide a treatment of the proof whose organization and brevity make it suitable for expository purposes. These results were first discussed in 1982, and almost all the details worked out by a year later. We would like to thank Peter Clote for his later interest and involvement in this web of ideas.

We give two new finite combinatorial statements which are independent of Peano arithmetic, using the methods of Kirby and Paris [6] and Paris [12]. Both are in fact equivalent over Peano arithmetic (denoted by P) to its 1-consistency. The first involves trees and the second linear orderings. Both were “motivated” by anti-basis theorems of Clote (cf. [1], [2]). The one involving trees, however, is not unrelated to the Kirby-Paris characterization of strong cuts in terms of the tree property [6], but, in fact, comes directly from König's lemma, of which it is a miniaturization. (See the remark preceding Theorem 3 below.) The resulting combinatorial statement is easily seen to imply the independent statement discovered by Mills [11], but it is not clear how to show their equivalence over Peano arithmetic without going through 1-consistency. The one involving linear orderings miniaturizes the property of infinite sets X that any linear ordering of X is isomorphic to ω or ω* on some infinite subset of X. Both statements are analogous to Example 2 of [12] and involve the notion of dense [12] or relatively large [14] finite set. We adopt the notations and definitions of [6] and [12]. We shall in particular have need of the notions of semiregular, regular and strong initial segments and of indicators.

Abstract Let P0 be the subsystem of Peano arithmetic obtained by restricting induction to bounded quantifier formulas. Let M be a countable, nonstandard model of P0 whose domain we suppose to be the standard integers. Let T be a recursively enumerable extension of Peano arithmetic all of whose existential consequences are satisfied in the standard model. Then there is an initial segment M′ of M which is a model of T such that the complete diagram of M′ is Turing reducible to the atomic diagram of M. Moreover, neither the addition nor the multiplication of M is recursive.