FOM: Towards a Consensus?

[Soren Riis]

----------------------------------------------------------------
Towards a consensus?
----------------------------------------------------------------
Concerning my posting [Riis; Thu, 5 Feb 1998] "Towards a consensus"
I would like to ask Vaughan Pratt and others to explain
where they think I am mistaken (I am fully aware I grossly ignore
many more refined issues; some of these issues have been put
forward by Robert Black [31 Jan 98] as acknowledged by Harvey 
Friedman [31 Jan 98]. I am also fully aware Friedman and 
Simpson already have been discussing the issue of Cat-fom at a level 
which I think transcend the elementary level at which I am trying 
to clarify things). 

Here is an extract and summary of my position in this debate: 

Fom MUST (and indeed does) address the question of WHICH assumptions 
are "good" (i.e. leads to correct results) and which assumptions 
are "bad" (i.e. might lead to false results). 
The answer to this question is linked to ZFC and in a sense ZFC has 
become the measure of everything. 

Group theory is about groups, Ring theory is about rings, and Category
theory is about Categories. In that sense CAT and Topos theory
are theories. They are NOT theories about mathematics. They are
mathematical theories. 

Set theory ZFC about sets - but more importantly it is a deductive 
powerful theory about the mathematical universe. Topos theory is 
about mathematical "universes". This make all the difference in 
the world when it comes to fom. 
ZFC has a commitment to ONE universe. Topos theory is about many 
universes - HOW CAN YOU AVOID RELATIVISM if you do not single out 
at least a class of universes which for example gives the correct results 
in number theory?? HOW CAN YOU AVOID NOT BEING UNSCIENTIFIC if you are
not aiming for the MAXIMAL deductive strength (by for example accepting 
only intuitionistic arguments)?? 

(side remarks: (1) MAXIMAL deductive strength without compromising the 
likelihood of inconsistency, unsoundness etc.
(2) I have meet a number of category people who only accept 
intuitionistic arguments)

When we judge the correctness of a theorem in group theory, ring theory 
or category theory we are not reasoning inside just another topos. 
We do not check Wiles proof against the axioms of a topos with a 
natural number object. The validity of Wiles proof was not on 
stake when we discovered the bugs in Colins axioms. If it (against 
expectations) should turn out that Wiles proof contain an argument 
which cannot be formalized in ZFC, Wiles proof would be in serious 
trouble - not ZFC.

This is not to say I think Wiles just proved ZFC -> FLT as Vaughan Pratt
suggest. Wiles gave an informal proof, in which I assume there was
no mentioning of any axioms in ZFC. Wiles proved FLT. I am not claiming 
Wiles proof is mistaken if it cannot be formalized in ZFC. Just that the 
proof will be in trouble and a lot of conceptual work will have to be done
in order to save it.

Remark: An important issue (which I only adsressed briefly) is the issue
of "deductive strength". I think this involves much more than just
deductive comparison between systems of set theory ... I think we see 
the ideal of aiming for the highest deductive strength also in weak systems 
a la Van Dreis! ..All this is a different discussion...

-----------------------------------------------------------------------------
The one point topos (answer/excuse to Pratt)
-----------------------------------------------------------------------------
In [Riis; Thu, 5 Feb 1998] I wrote:
>Simpsons challenge was to provide axioms for a Topos which does not
>leave any judgments to the user. If there is a one element topos
>satisfying the axioms, its not the user who have to tell the
>program there is more than one real number.  The challenge was
>to present a system where the user just have to press to button.

Vaughan Pratt answer:
> Ah, I see why you're having trouble with the singleton topos, you're
> identifying its objects with elements of its objects.  This off-by-one
> error in type makes all the difference.

> The result is not to lose theorems as you seem to be assuming but to 
gain
> them: the singleton topos is inconsistent, not theorem-free.  What saves
> topos theory itself from inconsistency is that, while it does not forbid
> the singleton topos, it does not insist on it.

Actually I was not identifying its objects with elements of its objects.
This was more a figure of speech to illustrate my point. I leave it to
you to think about the one point topos as inconsistent. I my universe
it has a model and are thus perfectly consistent. Like the
model containing only one point {false} or the model containing
only {3.14...}. 

I am sure all on this list know that in the CONTEXT OF THE CHALLENGE  
there is a problem allowing the singleton topos. Then why have two people
indicated that this was not a problem and that its me who have a problem. 
Trying to cover up? :-)
Clearly it was just a minor omission from Colin's part. The serious
point (and this has already partially been acknowledged by McLarty) is
that the axioms seems insufficient to meet the challenge. This was 
the main point in my previous posting.

Finally I would like give an excuse to Vaughan Pratt if I confused his 
position with that of John Mayberry. This was not my intention.

Soren Riis

Research Fellow
Fields Institute 
Toronto 
Canada