Browse Prior Art Database

A NOTE ON THE LENGTH OF CRAICS INTERPOLANTS

IP.com Disclosure Number: IPCOM000128133D
Original Publication Date: 1980-Dec-31
Included in the Prior Art Database: 2005-Sep-15
Document File: 3 page(s) / 15K

Publishing Venue

Software Patent Institute

Related People

Albert R. Meyer: AUTHOR [+3]

Abstract

There is no recursive bound on the length of the smallest interpolant.

This text was extracted from a PDF file.
This is the abbreviated version, containing approximately 53% of the total text.

Page 1 of 3

THIS DOCUMENT IS AN APPROXIMATE REPRESENTATION OF THE ORIGINAL.

A NOTE ON THE LENGTH OF CRAICS INTERPOLANTS

by Albert R. Meyer Laboratory for Computer Science iWassachusetts Institute of Technology Cambridge, MA September 28, Abstract: There is no recursive bound on the length of the smallest interpolant.

This work was supported in part by the National Science Foundation, grant Nos. MCS7719754 and MCS 8010707, and by a grant to the M.I.T. Laboratory for Computer Science by the IBM Corporation. Let F and G be formulas of first order predicate calculus with equality. If F implies G, there is, according to Craig's well known Interpolation Lemma, a formula C such that F implies C, C implies G, and the only nonlogical syffibols in C are those common to both F and
G. Such a formula C is called an interpolant for F and G.

Mundici [Mundici 803 has recently observed that the length of the smallest interpolant is in general not bounded by any elementary-recursive function (in the sense of Kalmar, cf.[Ritchie 633). Mycielski [personal communication 1990] has conjectured that there is no general recursive bound. A proof of this conjecture is given below.

Let IF1 denote the length of F.

Theorem. For every total recursive function f.-IN-#IN, there exist first order formulas F,G such that F implies G but the smallest interpolant for F and G has length ixceeding AJFJ+JGJ).

To prove the theorem, we first note the familiar fact that partial recursive functions are numeral- wise representable in a finitely axiornatizable fragment of the theory of arithmetic. Specifically, let S be a monadic function symbol and 0 be a constant symbol. Let n+1 denote S(n) for n 'E IN.

Lemma 1. There is a first order formula AX such that for every partial recursive function ip:IN41N, there is a first order formula F ip (x,y) such that

(Equation Omitted)

(Equation Omitted)

Moreover, AX is true in the standard structure of arithmetic.

Proofs of Lemma I appear in many texts, cf. [Miachtey and Young 783 for a recent exposition.

Let he the standard structure of the natural numbers with successor and the constant zero. This structure has a decidable theory. (Its second order monadic theory is even decidable [Buchi 62, Elgot and Rabin 66]). It follows that given n E IN, one can effeciiiely find the smallest first order formula Gn(x) whose only nonlogical symbols are S and 0 such that

(Equation Omitted)

This immediately yields: Lemina 2. There is a total recursive function g.-INI-+IN such that for any In E IN and first order formula G(y) whose only nonlogical symbols are S and 0, if

Massachusetts Institute of Technology Page 1 Dec 31, 1980

Page 2 of 3

A NOTE ON THE LENGTH OF CRAICS INTERPOLANTS

(Equation Omitted)

then

(Equation...