Subject: Foundations and formalisability

From: categories <[email-masked]>
Date: Thu, 14 Mar 1996 17:12:48 -0400 (AST)

Date: Thu, 14 Mar 1996 21:00:06 GMT
From: Ralph Loader <[email-masked]>

[email-masked] 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.