Date: 24 Apr 1993 11:24:52 -0400 (EDT)
Subject: Other considerations
Message-id: <9304241124.memo.2814@BIX.com> Sat, 24 Apr 1993 11:24:52 -0400 (EDT)
Allow me to add yet another perspective on the issues that
need to be addressed by the QED family. I <<personally>>
feel that the foundationalist goals so far expressed are
somewhat unrealistic either now or in the future: what
counts as rigor or "firm foundation" has changed in the past,
and will do so again, undoubtedly because "God has more disk
space" than we do. While I think that these millenialist
aspirations may make a good research program, I prefer a
different avenue, but one at least mentioned previously:
what can we get people interested in?
It may be that our best approach <<is>> to preach a Great
Crusade in search of ultimate surety and foundation, but a
More Modest Proposal might bring out some interesting issues
as well: Let us merely seek to lay bare what methods and
practices generally accepted within a particular field allow
in a completely formal way: i.e. we pick some area where
there is broad acceptance of methods (both inferential and
postulational) and, in the spirit of a suggestion of Victor
Yodaiken, use the language standard of that area (he suggested
Serge Lang's text). If we follow this approach, we need to
select some area where there might be significant agreement
among mathematicians as to the utility of such a program:
I suggest the verification of the simple group classification.
The methods are for the most part clearly agreed upon, it is
the details which are in doubt.
If you are still with me, then you will see a problem which
also faces the Grand Crusade as well as the More Modest
Proposal: how do we input the massive ammount of material?
Clearly getting machine readable versions of all the relevant
materials is the least o our worries: translation into the
chosen base logic is an enormous task, but one which is not
without forerunners in other areas. What we need is some
sort of computer-aided or, more unlikely, completely
automated, Hermeneutical Daemon to use in this project.
This Daemon is more closely related to work in the humanities
on textual analysis than to Automated Reasoning Projects,
and might require yet another group of interested
participants. In short, the More Modest Proposal may lead
to a slightly different Crusade. It does, however, point
up another area of consideration for the QED group.
Michael Thayer (donning his asbestos suit)