Networks, System Safety,

Embedded and Distributed Systems

Research Group of Prof. Peter Bernard Ladkin, Ph.D.

Embedded and Distributed Systems

Research Group of Prof. Peter Bernard Ladkin, Ph.D.

Antony Galton claimed that a Lemma of mine is false. I analyse the structure of the models of the axioms

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).

- Lemma 2 of (4) is true; I shall prove a considerably stronger version;
- I nowhere stated nor claimed the false lemma Galton attributes to me;
- Galton's observation was first noted by Ralph McKenzie (5)

- the axiom
**M2**of (4) is not identical to the axiom**M2**quoted and used by Galton; - in fact, it contains a typo, but;
- I didn't know at the time of printing.

**M1***:A: p, q, r, s : (p||q /\ p||s /\ r||q => r||s)***M2L***:A: p, q, r, s : (p||q /\ r||s) => (p||s # :E: t : p||t||s # :E: t : s||t||p)***M3***:A: p : :E: q, r : q||p||r***M4***:A: p, q, r, s : (p||q||s /\ p||r||s) => r=q***M5(E-form)***:A: p, q : (p||q => :E: r, s, t : r||p||q||s /\ r||t||s)*

**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:

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

by the condition

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

**M2***:A: p, q, r, s : (p||q /\ r||s) => (p||s # :E: t : p||t||s # :E: t : r||t||q)*

**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)

**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.

**M6L***:A: p, q, r, s : (p||q /\ r||s /\ ¬p=s) => (p||s # :E: t : p||t||s # :E: t : s||t||p)*

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*:

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)**

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.

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.

- Either the theorem is false, in which case one is misleading one's colleagues; or
- The theorem is true, and by claiming it prematurely one is preempting others from getting genuine credit for providing the correct proof; or
- The theorem is not precisely stated, thus preempting others from completing precise work in the same domain.

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 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