Other considerations

• Mail folder: QED
• Next message: guttman@linus.mitre.org: "Re: Incentive to write proofs "
• Previous message: John Harrison: "Incentive to write proofs"

Date: 24 Apr 1993 11:24:52 -0400 (EDT)
From: mthayer@BIX.com
Subject: Other considerations
To: qed@mcs.anl.gov
Message-id: <9304241124.memo.2814@BIX.com> Sat, 24 Apr 1993 11:24:52 -0400 (EDT)
Content-Transfer-Encoding: 7BIT
X-Cosy-To: qed@mcs.anl.gov
Sender: qed-owner
Precedence: bulk

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)