FOM: Scope of FOM?

[John Pais]

FOM is a list addressing Foundations of Mathematics (f.o.m.). However, it is
not clear to me (a fairly new list member) from recent posting exactly how
broad the f.o.m. scope is. It seems that two important main threads involve:

1. What follows from what--intuitively or "naturally" (as indicated by R.
Tragesser).
2. What follows from what--formally (e.g. as indicated by H. Friedman and S.
Simpson).

So, assuming 1 is permitted, then we also have:

3. Given a candidate of type 1, i.e. an intuitive representation of a piece of
mathematics, and a candidate of type 2, i.e. a formal representation of the
same piece of mathematics, then set evaluative criteria through which both
types of representations can be compared and contrasted in terms of how
'effectively' and 'faithfully' each captures the mathematics itself
(presumeably representation independent).

4. Create and evaluate hybrid representations 'optimized' in various ways and
for different purposes on their type 1 and type 2 features.

Based on my limited FOM experience it seems that 4. has been addressed only
very weakly by restricting attention (FOM list scope?) to representations of
type 2, with some discussion of inevitably emerging type 1 features. In my
opinion, serious attention to 4. is very important for *communicating*
mathematics within the community of mathematicians: researchers, teachers, and
learners.

My intent is not to try to diminish the importance of precisely and formally
codifying mathematics, but to specifically focus on Mac Lane's qualification
(in Mathematics: Form and Function, p. 377) that doing mathematics involves
"not the *practice* of absolute rigor, but [the maintenance of]  a *standard*
of absolute rigor."

p. 378
"Moreover, there are good reasons why Mathematicians do not usually present
their proofs in fully formal style. It is because proofs are not only a means
to certainty, but also a means to *understanding* [my italics]. Behind each
substantial formal proof their lies an idea, or perhaps several ideas. The
idea, initially perhaps tenuous [e.g. intuitive], explains why the result
holds. The idea becomes Mathematics only when it *can be* [my italics] formally
expressed, but that expression must be so couched as to reveal the idea; it
will not do to bury the idea under the formalism."

p. 379
"...Proofs serve both to convince and to explain--and they should be so
presented."

So, let me respectfully ask Harvey and Steve, is the 'foundational' activity I
describe above in 3 and 4 within the scope of the FOM list?

Thanks,
John Pais