[FOM] Inference Avoidance?

[Harvey Friedman]

This message is suggested by Tennant's 10/7/06 9:46PM
http://www.cs.nyu.edu/pipermail/fom/2006-October/010907.html

Can one identify any basic inference rule which is not used in actual
mathematical practice? Or at least whose use is particularly rare?

This kind of question is far more delicate than it would appear on the
surface. 

1. It requires a detailed model of mathematical practice, as the
mathematical literature does not consist of anything resembling formal
proofs, and any two practicing professional mathematicians use significantly
different proof styles when they convey their informal and semiformal
proofs. 

2. Even after the required detailed modeling, there is the problem of
actually gathering the data. I.e., finding - which means constructing -
formal proofs and looking to see what is happening.

3. Fortunately, because of major advances in what is now called proof
assistants, deep and complicated formal proofs have now been constructed of
major mathematical theorems. And many of these formal proofs have been saved
in formats that allow for detailed examination.

4. There are now several different proof assistants, all with the strongest
possible adherents, that are based on detailed models of mathematical
practice. These models differ in detail, but perhaps they have enough in
common not to cause problems with the investigations proposed here.

5. Over the years, there have been FOM postings from adherents and
practitioners devoted to Isabelle and to Mizar, and perhaps others. It would
be fascinating to see such scholars post on this topic, armed with the
formal proofs that they have either personally constructed or have been made
available to them. 

6. My own gut feeling is that there is no basic inference rule which is
avoided in mathematical practice - no matter how silly that inference rule
may appear in isolation. But that is just a guess.

7. Even if my hunch in 6 is right, there is still the question of the
relative frequency of the various inference rules. Of course, this may
depend, to some unclear extent, on the person creating the formal proofs
with the proof assistants - rather than anything intrinsic in the informal
or semiformal proof they start off with. This remains to be seen.

Harvey Friedman