cat-dist@mta.ca writes:
This might be a little disingenuous -
Of course, in any topos there will be a monic X=>Y --> P(XxY) , so via the "internal language" X=>Y may be seen as a certain set of sets of ordered pairs. But the point is that via the "internal language" you can (and indeed you may) argue about the structure of a topos in a very "set-like" manner. But of course you are not obliged to do so. So in a very real sense, your (first) example illustrates that your fear is unfounded.
We seem to have got completely sidetracked from either of the points I was trying to make (probably my fault for making it unclear that it was a two points, and for using sloppy language). The (good) category theorist proves "there exists internal homs [in any topos]" [by constructing particualar internal homs, or otherwise]. The (good) set theorist proves "there is a structure satisfying the Peano axioms [is a theorem of first order ZF]" [by constucting one explicitly, or otherwise]. Both can then be asked "which is the real internal hom / set of natural numbers". Both can answer that they didn't claim that there is a particular "real" internal hom / set of natural numbers. [See my P.S.] A (bad) topos theorist might never actually prove "there exists internal homs", but rather continually refer to an explicit construction, rather than its universal properties. A (bad) set theorist may construct a set, and never prove that it satisfies the Peano axioms, but rather keep referring to the explicit construction. In both cases, the bad mathematician has a real problem when asked why they're using their particular construction, as opposed to some isomorphic alternative. In both cases the good mathematician does the right thing---showing the existence of structures with appropriate properties, and then using those properties, rather than refering to any particular structure. This was with regards to the question "Which construction of the natural numbers do you have in mind? Russell's or Van Neumann's?". Now we have a slightly different issue:
point of Peter Freyd's observation was (I think) that a topos theorist without any taste is less likely to stumble upon this question than a set theorist without taste, who might well do so... due to the emphasis upon different fundamental notions in the two approaches.)
I read Peter Freyd's original criticism to be a criticism of the fact that it was *possible* to ask [Quote: `one can ask'] "Does any simple group appear as a zero of the Riemann Zeta function" in ZF, presumably claiming that this cannot be asked in category theory. If we weaken this to just saying that category theory makes some nonsensical statements more clearly nonsensical than they would be in set theory, then I have no objections to his statement. "Makes ... more clearly" is a matter of aesthetics, which is sometimes an important consideration. However, are aesthetics an overriding considerations for foundations? It's not obvious to me that it's even a _foundationally_ important consideration here---as has been pointed out by others, people don't do real mathematics in either first order topos theory or in first order ZF; it is probably impossible to develop a reasonably clear mathematical vernacular in either. Ralph. P.S. In any case, it is entirely possible to carry out formalisation of mathematics in first order ZF in such a way that statements like "A simple group appears as a zero of the Riemann Zeta function" do not have a formalisation. This is an application of the good practice I advocated above. In brief outline (=incomplete): Let Reals(R,+,*,0,1,<) be "R,+,*,0,1,< is a complete Archimedean linearly ordered field"(2), stated in the language of 1st order ZF in the obvious way. Define formalisations of sentences about the reals so as to be formulae in the form(1) Reals(R,+,*,0,1,<) implies phi(R,+,*,0,1,<) along with a _proof_ of a ``type-checking'' sentence ( there exists (R,+,*,0,1,<) such that Reals(R,+,*,0,1,<) and phi(R,+,*,0,1,<) ) if and only if ( for all (R,+,*,0,1,<), if Reals(R,+,*,0,1,<) then phi(R,+,*,0,1,<) ) Now of course, if a sentence about the reals can be seen to make sense, then there should be a straightforward proof that it is independant of any particular presentation of the reals, so that the type-checking statement will be ZF-provable. Clearly, if phi tries to formalise Freyd's statement, then it's type-checking sentence is false and not provable. Note that if phi is a tautology (or a contradiction) then it will have a provable type-checking sentence. We could probably argue until the cows come home about whether or not this is reasonable. (1) Using a trivial (&conservative) extension of ZF would enable us to drop the "Reals(R,+,*,0,1,<) implies". This is probably necessary if we wish to formalise statements with free variables over the reals [I use sentence in the logical sense of not having free variables]. (2) Apologies if I missed an axiom of the real numbers. P.P.S. This is getting off-topic for a category theory list. If people want to carry this on, perhaps we should take this off the categories list.