[FOM] Lorenzo Carlucci, a non-subscriber, writes regarding "naturality issues"

[Martin Davis]

The following interesting message from a non-subscriber has been 
brought to my attention.

Martin
****************************************************************************************************************
As well-known to our community, Friedman introduced the notion of "gap
condition" in order to boost the logical strength of wqo theorems
such as Kruskal theorem. Friedman's "Extended Kruskal Theorem" was
later used in the proof of Robertson and Seymour Graph Minor Theorem
although, as far as I know, its use was later replaced by other methods.

In a 1990 review of Simpson's "Nonprovability of certain combinatorial
properties of finite trees", (The Journal of Symbolic Logic, Vol. 55, No.
2 (Jun., 1990), pp. 868-869), Wilfried Buchholz thus comments on the "gap
condition":

"As far as the reviewer knows, the above mentioned "gap condition" has no
special mathematical relevance but is rather an ad hoc device introduced
solely for the purpose of creating an embeddability relation
$\sqsubseteq'$ such that, on the one side, $\forall n \in \omega WQO(T_n,
\sqsubseteq')$ holds and, on the other side, that this theorem becomes
strong enough to imply (in ACAO) the well-foundedness of the ordinal
notations up to $\psi_O(\Omega_\omega). But nevertheless the gap condition
looks rather natural and does not at all reveal its proof-theoretic
origin. Therefore, one can agree with the author that $\forall n \in
\omega LWQO(T_n, \sqsubseteq') is indeed a 'mathematically meaningful
theorem of finite combinatorics'."

Buchholz is very cautious in writing "As far as the reviewer knows", and
eventually acknowledges that the notion is "mathematically meaningful" and
"rather natural". Yet Buchholz seems to regard the "gap condition" as a
case of successfully hiding a proof-theoretic origin and is dubious about
its "mathematical relevance".

In a very recent paper by Maria Chudnovsky and Paul Seymour ("A
well-quasi-order for tournaments", Journal of Combinatorial Theory. Ser B,
Vol. 101 (2011), 47-53), a wqo result of Simpson's is used in a key way to
prove a wqo result on directed graphs (by the way, I conjecture that the
use of Simpson's result is unavoidable). The authors thus comment on their
proof strategy:

"This is achieved by applying a standard technique from
well-quasi-ordering, first making the enumerations "linked", and then
applying a strengthened version of Higman's theorem with a gap condition."

It is not entirely clear to me whether the "standard technique" refers
only to the trick of making the enumerations "linked" or else to the
application of Higman's theorem with gap condition, yet I find it
interesting to observe how leading researchers in Combinatorics are ready
to accept the use of the gap condition as perfectly natural, without
the -- possibly justified -- cautiousness of a leading researcher in Logic
such as Buchholz.

Obviously in that case the point is that the originally "ad hoc" notion
has been later used to obtain important results of major interest to
mathematicians in a non-foundational area.

I think the well-known quote of Cantor's -- "The essence of mathematics
resides in its freedom'' -- should be kept in mind. Most areas of
mathematics have intimate connections and should not be regarded as
rigidly separate bodies. Also, finding new connections between different
areas is part of the beauty of mathematical research.