This is an archived page and is no longer updated.
Please visit our current pages at https://rvs-bi.de

A Note on a Note on a Lemma of Ladkin: Confessions of a Miscreant, namely

Peter B. Ladkin

Research Report RVS-RR-96-15
Abstract:
Antony Galton claimed that a Lemma of mine is false. I analyse the structure of the models of the axioms M1 and M3 of Allen and Hayes. Then I prove the Lemma that Galton claimed was false. (Galton's theorem, however, is true.) I tell the story of how the discrepancy arose, and indulge in a little moralising about theorems that appear on the record without proofs.

In (1), Antony Galton gives five axioms, M1-M5, proposed by Allen and Hayes (2) for the meets relation between intervals of time. Ladkin (3, Chapter 5) described explicitly all the possible models for these axioms. A version of (3, Chapter 5) appeared in (4), which contained a Lemma 2: that the axiom Existential M5 followed from M1-M3 as they appeared in (4).

The Naked Truth

Galton claims Lemma 2 from (4) is false. Galton shows correctly that M5 does not follow from the other axioms he gives. However,....... but before the reader begins to share my self-Righteous Indignation, I had better make my

True Confessions

namely, The problem was discovered and fixed in my thesis (3, Chapter 5). For the story, see below. To nail the lid shut, I shall analyse first

The Models of M1 and M3

I use /\, \/, ¬, => for the Boolean connectives, # for exclusive-or, :A:, :E: for the quantifiers, :in: for the set-membership relation, and elide e.g, p||q /\ q||s as p||q||s. The axioms I gave in (4) are Define the formulas

p ~¹ q   if and only if   :E: s : p||s /\ q||s
p ~² q   if and only if   :E: s : s||p /\ s||q

Lemma 1:     M1 =>
                          (:E: s : p||s /\ q||s) <=> (:A: s : p||s <=> q||s)   /\
                          (:E: s : s||p /\ s||q) <=> (:A: s : s||p <=> s||q)

The proof is straightforward. Lemma 1 implies the following. For a formula R with two free variables p and q, let Equiv(R) be the following sentence:

(:A: p : R(p,p)) /\ (:A: p, q : R(p,q) => R(q,p)) /\ (:A: p, q, r : R(p,q) /\ R(q,r) => R(p,r))

where (for the syntactically correct) R(x,y) denotes the formula R with every free occurrence of p replaced by x and every free occurrence of q replaced by y. Equiv(R) says that R is an equivalence relation.

Lemma 2:   M1 => Equiv(~¹) /\ Equiv(~²)

Let M = <X,R> be a model for M1. That is, X is a set and R satisfies the sentence M1. Let the domains of ~¹ and ~² in M be S¹ and S², respectively. Let A¹, respectively A² be the sets of equivalence classes of ~¹, respectively ~². We may thus define a function

F: A¹ -> A²

by the condition

F(a) = b   if and only if   (a :in: A¹ /\ b :in: A² /\ (:E: p :in: a, q :in: b : p||q ))

It follows that

Lemma 3:     Let M = <X,R> be a model for M1.
                          Then F(a) = b   if and only if   (a :in: A¹ /\ b :in: A² /\ (:A: p :in: a, q :in: b : p||q ))

It follows from Lemma 3 that if M1 is true, and || is irreflexive (¬ :E: p : p||p), that for every pair of sets <a,b> such that F(a) = b, the relation || forms a complete bipartite graph on <a,b>. (Standard terminology is K(#a, #b), where #x is the cardinal number of the set x. Actually, the arguments are usually written as subscripts, but not in HTML :-). In other words, the relation || is isomorphic to a disjoint union of bipartite graphs:

Lemma 4:     Let M = <X,R> be a model for (M1 /\ ¬ :E: p : p||p).
                          Then ( R ~ DisjointUnion { K(#a, #b) : a :in: A¹ /\ b :in: A² /\ F(a) = b } )

where ~ denotes 'isomorphic to'.

The Allen-Hayes axiom

implies that || is irreflexive (6). (Take p=q=r=s. If p||p then p||p||p therefore :E: t : p||t||p, contradicting the exclusive-or.) Hence Lemma 4 applies to the conjunction of M1 with M2. Lemma 4 allows a finer understanding of what the axiom M1 contributes to the structure of its models than has so far appeared in the literature.

Lemma 5:     Let M = <X,R> be a model for M1.
                          Then X \ S¹ = { p : ¬ :E: s : p || s } /\ X \ S² = { p : ¬ :E: s : s || p }

Lemma 5 makes it easy to see what additional structure the axiom M3 contributes. It follows that, given M1 and M3, the relations ~¹ and p ~² are equivalence relations on the entire domain D of ||.

Lemma 6:     Let M = <X,R> be a model for M1 /\ M3.
                          Then (S¹ = S² = X)

Proving The Infamous Lemma and a Little More

I now prove the strengthened version of Lemma 2 of (4). The alert reader will have noticed that Axiom M2L is a little weird. Firstly,

Lemma 7:   M3 => (M2L <=> :A: p, s : (p||s # :E: t : p||t||s # :E: t : s||t||p))

from which it follows that

Lemma 8:   M3 and M2L are inconsistent.

The easy argument proceeds thus. Let p = s. Then the second and third clause of the exclusive-or are now identical and since A # A is inconsistent for any A, the first clause is true and thus p||p. But this implies p||p||p and thus :E: t : p||t||p, which contradicts the exclusive-or. QED.

Lemma 2 of (4) follows directly from Lemma 8:

Corollary 9: M1 /\ M2L /\ M3 => M5(E-form)

because everything follows from an inconsistency. I am vindicated, but embarrassed. Suppose we weaken M2L to get rid of this trivial inconsistency.

Unlike M2, M6L does not by itself imply that || is irreflexive, but M6L in conjunction with M3 does imply that || is symmetric.

Lemma 10:   M3 => (M6L <=> :A: p, s : (¬p=s) => (p||s # :E: t : p||t||s # :E: t : s||t||p))

M3 is used to assure the existence of appropriate q and s for the antecedent of M6L, and then the antecedent and the quantifier are simplified. QED. Thus

Lemma 11:   M3 /\ M6L => (:A: p, q : p||q => q||p)

The argument is as follows. The consequent is trivially true for q = p. So let ¬ p = q and apply Lemma 10 with s = q:

p||q => (¬ :E: t : p||t||q /\ ¬ :E: t : q||t||p) => (¬ :E: t : q||t||p /\ ¬ :E: t : p||t||q) => q||p. QED

Finally, it turns out that || contains the universal irreflexive relation:

Lemma 12:   M3 /\ M6L => (:A: p, q : ¬(p = q) => p||q)

The argument is as follows. Let p and q be arbitrary unequal members of D. Suppose :E: t : p||t||q. But p||t||q => q||t||p by symmetry; consequently it follows that :E: t : q||t||p. The converse is similarly trivial. Thus :E: t : p||t||q <=> :E: t : q||t||p. But by Lemma 10 at most one of these can hold. Therefore neither of them do and thus by Lemma 10 again it follows that p||q. QED.

Thus, even the weakening of M2L necessary for consistency with M3 is too strong to be at all useful. The equivalent of Corollary 8 for M6L of course holds:

Corollary 13: M3 /\ M6L => M5(E-form)

The Story

I confess, I didn't realise at the time how useless M2L or its more reasonable form M6L were. Pat Hayes points out (8) that M2L looks very much like the axiom for linearity of points, or points-with-intervals (where points are 'degenerate' intervals (2)).

Galton compared my axioms with those in (2) and graciously overlooked the difference (9). But as a result, he interpreted me as claiming a false lemma. I'd prefer to be judged as having said something useless rather than something wrong, hence my endeavor to set the record straight(er).

But I claim not to be quite as daft as it may look. Pat Hayes (it's all his fault, of course) sent me by email a preliminary version of (2), which contained M2L (sabotage!!). Pat wryly points out that it should have taken me just a short while to spot the error (8). However, because M2L looked prima facie reasonable, and I didn't quite know what the axioms meant at the time, I worked syntactically from the axioms to prove Lemma 2 and also the other theorems. This also formed Chapter 5 of my Ph. D. thesis (4). After the camera-ready copy of the AAAI paper had gone to the printers, my thesis advisor Ralph McKenzie called me up to say that my Lemma 2 was somehow false since M5 could not follow from the other axioms. I noted that I'd given a trivial syntactic proof, but we couldn't see what was wrong at the time. He called me back a day later to inform me of the typo. (I was proud - Ralph is known for solving other people's research problems in real time, but he took a whole day to find my error :-). Ralph had, as Galton did, read the axiom he thought should be there, rather than the axiom that was there. I went through the paper to ensure that the other theorems were correct, and changed the chapter of my thesis to reflect the correct axioms and eliminate the Lemma. I believe that was all in May 1987.

I was very embarrassed (and still am) to have in print a typographical error in the axioms and a Lemma which was dependent for this typo on its truth. But I figured that the real point was the model theory, which remained accurate, and thought it would be too pompous to announce the error in print (although I believe I mentioned it in the AAAI talk), because there wasn't any evidence at the time that people actually cared that much about the work.

The Moral(s)

Which just goes to show that one cannot predict the consequences of one's work. And also that I'm less concerned now about being pompous. I'm glad that Antony set the record straight, and that I have finally set it even straighter.

The incident does, however, illustrate what I believe to be the perils of AAAI and IJCAI Proceedings, namely, they are considered to be publications of record. However, many papers that appear in those proceedings contain claimed "theorems" whose proof the referees had not seen. And, in some cases, for which a correct proof did not exist when the paper was submitted. I don't see how this situation is compatible with AAAI and IJCAI being publications of record.

The situation could be remedied as follows. Papers with theorems be submitted with an Appendix containing full proofs of those theorems, the Appendix not to appear in the Proceedings but to be used by the referees. The referees should also, as in mathematics, read the proofs to ensure they're correct. (This may mean either extra work or fewer papers, but I see no way around it.)

This procedure wouldn't catch all the problems. For example, I submitted (4) with the proofs in an Appendix, but of course checking proofs doesn't catch typos.

For those who think my suggestion stems from pomposity fed by embarrassment, let me say that I know of one often-quoted theorem from AAAI conferences which did not have a correct proof at the time of submission, and another, also well-quoted but less so, which has never been given a correct proof by its author. And this led to further problems, because the imprecision in the statement of the theorems meant that when I and a mathematical colleague tried to figure out from the papers exactly what had been claimed as a theorem, we couldn't. It was just too imprecise. In the one case, however, it was fixable. In the other case, the 'proof' sketch given in an accompanying technical report, had one taken it seriously, would have sufficed to 'prove' some false results also. (To my knowledge, Roger Maddux was the first to observe a correct proof of this theorem as a corollary of joint work we were doing in 1988.)

Claiming theorems which one has not yet proved has one of three social consequences.

One may think that this is no big deal, because interesting theorems will be subject to inspection and corrected anyway if they are wrong (e.g, Galton's observation). This suggestion has its flaws. First, observe that Galton's paper appeared nine years after mine. Nine years is plenty of time for a lot of people to be misled. Secondly, observe that this method does not remedy premature claims of true theorems. It works even less well for roughly-true theorems with imprecise statements and no proof, as Maddux and I found in 1988. Providing counterexamples to imprecise theorems and proofs is a mug's game. It's hard to attract people's attention to statements of the form `If you mean this, here's a problem; whereas if you mean that, here's this other problem; whereas ......'

So how do we set the record straight? Maybe bodies organising conferences could make all supposed-proofs for theorems in their conferences available on the WWW, and offer graduate students $2 per for finding mistakes or mistaken reasoning à la Knuth. I leave the evolutionary consequences for the reader to observe :-)

Does the reader have a suggestion? Please let me know.

References

References link back to the first mention.
Back to top

(1): Antony Galton, Note on a Lemma of Ladkin, Journal of Logic and Computation 6(1):1-4, February 1996. Back

(2): James F. Allen and Patrick J. Hayes, Short Time Periods, in Proceedings of the 10th International Joint Conference on Artificial Intelligence, pp981-983, International Conference on Artificial Intelligence, Inc., 1987. Back

(3): Peter Ladkin, The Logic of Time Representation, Ph.D. Thesis, Group in Logic and the Methodology of Science, University of California at Berkeley, December 1987. Also Kestrel Institute Technical Report KES.U.87.13, November 1987, also available from http://www.rvs.uni-bielefeld.de/~ladkin/. Back

(4): Peter Ladkin, Models of Axioms for Time Intervals, in Proceedings of the Sixth National Conference on Artificial Intelligence, AAAI-87, pp234-239, American Association for Artificial Intelligence, 1987. Back

(5): Ralph N. McKenzie, Personal Communication, May (??) 1987. Back

(6): James F. Allen and Patrick J. Hayes, Moments and Points in an Interval-Based Temporal Logic, Computational Intelligence 5:225-238, 1989. Back

(7): James F. Allen and Patrick J. Hayes, A Common-Sense Theory of Time, in Proceedings of the 9th International Joint Conference on Artificial Intelligence, pp528-531, International Conference on Artificial Intelligence, Inc., 1985. Back

(8): Pat Hayes, Personal Communication, September 1996. Back

(9): Antony Galton, Personal Communication, September 1996. Back