FOM: Re:set/cat foundations

[Robert Tragesser]

        I am grateful for HF's
comments,  and have some more questions for him
(et al.).  What I hope to get across is just
what I see set-theoretical reductions leaving
behind, as losing (viz, the intensional),  but which
seems to be something if not f.o.m.,  then
f.o.m.t. [[HF's proposal -- t for thought]] ought
to be very interested in indeed. 

        I certainly do appreciate his remark,--

_[[H.Friedman]]_
[[No one has managed to uncover any accepted fundamental 
principles of construction that aren't trivially 
set theoretic. They become trivially set theoretic 
as soon as one tries to "get rigorous." What would be 
interesting is if one could point to a context 
where, when one tries to "get rigorous,"
one does something that is distinctly not 
set theoretic. And I mean: distinctly not set 
theoretic in the eyes of an expert in standard f.o.m.
who knows how powerful and flexible the usual set 
theoretic foundations is.]]
_[[End H. Friedman]__

[An aside:  I'd still like to know why it doesn't make
sense to ask for a nontrivial explanation of why it is
that "principles of construction" are ubiquitously
set-theoretic.  I think my craving for an explanation
here has to do with having no good feeling for how
one rationalizes "epsilon" and "set of".  By contrast,
I am comfortable with the idea that a process of
"getting rigorous" leads to formaliztion in higher
order logic. (Hence my question about Montague on
higher order logic and set theory.) 
        I'd love to see a step by step experimental
"rigorization"
of a piece of informal mathematics where the rigorizer
must feign no knowledge of "epsilon",  but is led
inexporably to it. . .that is, up to the point where
it must be invented or the path to full rigor fails.
   
Then,

_[Harvey Friedman]__
Obviously, set theory is conceptual mathematics, which 
is one of many
reaons I don't have an adequate grasp of this sentence.
_[End Harvey Friedman]_

        What I have in mind is something perhaps as
trivial as decoding mathematical concepts into the
language consisting of epsilon,  logical constants...
Suppose you give a set-expression defining "ordered pair",
but never say or picture "ordered pair".  Or,
at a greater extreme, say,  you develop local 
differential geometry in
set,  but you never go outside the language of
pure set.   You never say what concepts you
mean to be capturing,  you never say what the 
subject matter is.  
        I think that there is something very
substantial missing from this picture of
mathematics where only pure set talk finally
countsa.-- The flesh and the soul of mathematics
is what is missing.  
        Whatever (more exactly) is missing (concepts, 
 intensions,
ideas. . . ) typically have sufficient cogency that
one can mathematically reason,  and reason well
and powerfully,  without any anticipation of 
set-theoretic background. . .     

_[HARVEY FRIEDMAN]__
[[I have in my possession Foundations of Geometry, 
David Hilbert, as tranlated by Open Court Classics,
 1988. Not only is there no problem giving
standard set theoretic foundations for the entire 
book; it even was written by Hilbert with set 
theoretic ideas in mind, and mentioned explicitly!!]]
_[[END HARVEY FRIEDMAN]__

        Again,  I meant something trivial.  These are in
fact not formal logical proofs.  (Hilbert gives no
logical syntax,  or any exact presentation of logical
ideas.)  The proofs of theorems 4,5,6,  say,  make use of
drawings of triangular figures and lines.  In
fact the drawings function in these proofs to replace
the logical syntax and rules of inference 
(but not missing geometrical axioms --
that's not my/the point).  _Those- proofs cannot be
 "formalized".
But they can _be replaced by_ formal proofs,  I would not
wish to dispute that!
        But its that intensional stuff which is crucial
to the mathematical enterprise.

        I can't but agree that it seems very interesting
that there is an amazing sense in which theorems as 
intensionally different as Bolzano-Weierstraas and the
Ramsey coloring thms are logically equivalent.
        This is a great story,  but it is only half of
the great story.-- We must also understand and
exactly conceptualize what is so profoundly different
in the theorems (THE WAYS IN WHICH THEY ARE INEQUIVALENT).
        Think of it this way.  When one is working on a
problem one really likes to see a theorem expressed
in as many different (but provably equivalent) ways --
that increases one's creative power.  At the same time,
one wants to have those differenceS in view (and in a highly
conceptual way) because they matter.  In the end
they matter most if we want to know more than that such
and such is the sOlution to the problem at issue.  They
matter -- that intensional stuff when we want to 
understand [the solution. . .}

robert tragesser