No subject

[Soren Riis]

---------------------------------------------------------------
Towards a consensus: 
---------------------------------------------------------------
Recently I had some private communication with people
on Topos and Category side to check whether Lawvere and Tierny 
axioms for an "elementary topos" (as modified by Colin McLarty
in his challenge axioms) meet the challenge of Simpson:

   > Consider the standard undergraduate calculus theorem saying that
   > every continuous real-valued function on [0,1] has a maximum
   > value. ....  I surmise that it's a difficulty for "categorical
   > foundations", because it's probably not provable in topos plus
   > NNO.

Continuing citing Simpson,
  
>  (NNO := natural number object).  What do the topos people have to
>  say about this?  Is my surmise meaningful?  Is it correct?  If it is
>  correct, what additional axioms are appropriate to prove this and
>  other basic theorems of real analysis?  How does all this affect the
>  project of "categorical foundations"?
>  
>  Note: In the above, when I say "appropriate axioms", I'm not
>  necessarily asking for the sharpest possible results, a la reverse
>  mathematics.  I'm only asking for a broad-brush portrait of how the
>  alleged "categorical foundations" would actually work.  Is this too
>  much to ask?  Is it a wrong-headed question?

It is quite clear that the axioms as given by McLarty are satisfied
by a model containing only one point (the terminal category). To make 
sure I double checked this with McLarty as well as other Cat-people on 
the list. They agree. To my sheer frustration one person did not see this 
as problem. His reply: "Of course, you can't get something from nothing.  
If you want to prove that something exists, you must put in some 
assumption to that effect".

Aha - they are Anarkists!! Or is it post-modernism showing us its
ugly face of relativism - in mathematics? I cannot believe what 
I hear. Choose your own assumptions - everything goes!!

Here is a reason why Topos theory (as well as IHOL or HOL)
is unsuitable as fom. It will also be clear why my research
area, Bounded Arithmetic (unlike what have been advocated by 
Nielson) is absolutely unsuitable as fom. That my topic area
is not fom, does not prevent it from being important and
fundamental. This is a different issue.

Perhaps we can begin to calibrate our 
terminology and start to aim for a consensus!! 

----------------------------------------------------------------
Uncontroversial reason why Topos theory is unsuitable as fom
----------------------------------------------------------------
If I want my computer to generate "theorems" in mathematical 
analysis I will have to program it. When the user asks: 
" Does every continuous real-valued function on [0,1] have a 
maximum value" (part of Simpsons Challenge) we would like the computer 
to come out with the answer "yes". The axioms for ACA_0 or 
Zermolo-Frankels axioms for ZFC would work (ignoring complexity
issues). 
Theorems in ordinary mathematics (or for analysis in case of ACA_0) 
would in principle eventually be answered correct by a program 
which search its way through the space of all proofs.

Now imagine someone (call him/her A) is claiming that pure 
predicate LOGIC (or HOL some other system of pure logic) 
is sufficient for analysis. The person would correctly claim that 
predicate logic really seems to underline all of classical mathematics.

I might object that A cannot prove any interesting theorems from
pure predicate logic. The person A then claim that this is what 
mathematicians do all the time. Wiles proof of FLT should, according 
to our friend A, more correctly be viewed as a proof of some tautology 
of the form:  "Assumptions -> FLT". 

Now in fom we are interested in which principles are underlying 
mathematical reasoning. Certainly we will agree with A that the 
principles of logic seems to underline all our activity. If we 
ask A to provide "principles of reasoning" (rules, axioms etc.) which 
captures those needed to prove FLT it is not sufficient to state the 
rules of predicate logic.
If we program the computer with these rules it would eventually print
"Assumptions -> FLT", but it will never get to FLT itself.

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.

Tomorrow we might have a shift of paradigm. Perhaps tomorrow some 
new and more powerful outlook (with more deductive power) will arise. 
No theorem of logic seems to rule this out. Perhaps tomorrow some
one will convince us set theory always will provide the most 
powerful outlook. Perhaps..

Like in other Sciences the deductive power of a theory (i.e. the 
deductive strength of the ontological assumptions) plays a crucial 
role for the quality of the theory (Carl Popper). 
Deductive strength is certainly not the only concern. Truth also
helps. But please allow me to simplify matters a bit. 
 
It should be clear that logic is more general than ZFC.
Logic does not make any ontological assumptions about the world. This 
is its strength, but also its weakness. Predicate logic is in 
Poppers sense a very bad theory.  

Predicate logic provide a general framework within which
valid mathematical reasoning can take place. It teach us very
little on which principles are valid. The questions of what 
principles are legitimate and thus would be acceptable in a 
proof of the Riemann conjecture is a fom question. If a
research area do not address such questions it CANNOT claim to
be fom. 

Now Topos theory (and even more Category theory) provide a 
very general setting for semantics underlying for example
intuitionistic reasoning. It also have a lot of merit because
of its high success as a language. We should not forget that
this language was spoken by some distinguished mathematicians
directly descended from Grothendieck's program. Among them
many fields medalists. This is also why "down to earth" category 
theory has a good name in Oxford where I was a student.
Category theory has obvious got a lot of flexibility. This is 
undoubtly also why the use of Category Theory in semantics 
in computer science seems so successful. Like any other language, 
the language of Category theory makes virtually no ontological 
commitment. This is of course wonderful for anarkists and relativists
but it would be a disaster as a reference point of what constitutes
correct reasoning.

The lack of ontological commitment and relativism helps making 
Category theory more general than set theory - in a similar
sense as predicate logic is more general than set theory. 

It is this generality which some Cat-fom people value as a virtue when 
it comes to discussions of fom.  
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.
When we judge the correctness of a theorem in group theory, ring theory 
or category theory we are not reasoning in just another topos. 
We do not check Wiles proof against the axioms of a topos with a 
natural number element. 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 formalised in ZFC, Wiles proof would be in serious 
trouble - not ZFC.

Topos theory cannot serve as fom (like predicate logic 
cannot). Its virtue (its generality) leave most foundational 
questions to the "user". This is completely unacceptable from a 
fom perspective. 

If we feed the axioms for a Topos into our computer and let it
reason about say FLT, it would not come out with any interesting
result unless we - the user - have specified which "principles
of reasoning" would count as valid. The attempt to ORGANIZE
and ANALYZE these basic principles is a very important part of fom.
Topos theory is NOT doing nor trying to do this. This alone disqualify 
topos theory as fom. 

People who are interested in fom are interested in axiomatizing 
and clarifying which "assumptions" can be removed from the
antecedent in a formal proof. This problem is left to the user by 
cat psedo-fom. 
Let me illustrate how this comes across in recent exchanges:

John Mayberry wrote:
"a proof is a valid argument to establish that its conclusion is a true 
proposition. If there is no such thing as truth, then there is no such 
thing as proof".

To which we got the following post-modern reply from
Vaughan Pratt:

"Your premise seems to be that every axiom of every proof system is
absolutely true.  For if not you would have proofs of theorems with no
basis for inferring that the proved theorems were absolutely true".

For John Mayberry a valid argument is MUCH more than a logical valid
argument. It has to be in agreement with reality. We do not make up
the facts of mathematics. John Mayberry believes Wiles proved FLT.

Vaughan Pratt answer suggest he (at least partially) takes the 
view that Wiles proved FLT in some proof system i.e. that Wiles
proved "assumptions -> FLT"

An even more provocative versions of relativistic philosophy has been 
suggested by a friend and college Carsten Butz:

> And, yes, we are logicians, we appreciate in particular
> intuitionistic logic, and not just because it is the logic that holds
> in the objects we study (toposes), also because we find the logic and
> the ideas of constructive/intuitionistic mathematics appealing.

Butz also writes: 
> Another remark: I once spoke to a computer scientist about the
> intermediate-value theorem and he said: "Of course, I do not believe in
> this theorem, why should I?" As far as I remember, the
> person had a good mathematical background, so you cannot just say that
> he was too stupid to get the result.

Mysticism undoubtly have some appeal - Perhaps I will need to take
LSD to experience Butz position fully. Personally I believe the tax 
payers are paying me to do Science i.e. produce deductive powerful 
theories and present a coherent outlook at the world. 

Intuitionism as a research object is fine and undoubtly can be justified. 
So can research in LSD. As a position for our reasoning (i.e. what we 
require when we check the correctness of our proofs and judge our 
theorems) Intuitionism, or taking LSD are not wellsuited instruments. 
If you disagree you are probably not doing mathematics 
in the style it is taught in Maths departments. Fine but in that case 
your personal research experience is irrelevant for fom.

Now it seems that people like Colin believe that the axioms of a 
Topos with a natural number object suffices for doing analysis. 
>From my perspective this is simply untrue. Certainly as the challenge 
axioms stands at this moment - I have checked this. If Colin 
(to my surprise) can overcome Topos theorys lack of ontological 
commitment and come up with some axioms (which works) the serious 
discussion can begin!!

You can of course do analysis in a suitable (boolean) topos. This is NOT 
what is at stake. You can draw diagrams from here to eternity. It
might be a wonderful tool, but the axioms which are suitable for 
analysis must contain more ontological commitment. It is not
enough just iterating a stuck of basic primitives. This is, as far
as I can see, all the axioms of a topos with a Natural Number Object 
are doing.

Butz wrote [Butz, 4 Feb 98]:
> One of the 'advantages' of an axiomatization of toposes is that a
> finite set of axioms is enough, no axiom scheme. Again, this means
> 'some' sort of simplicity, still it is debatable. 

PLEASE before you (Colin or someone else) claim victory - Could you  
STATE the axioms in a form where the axioms meets Simpsons challenge. 
The axioms got so far have all grossly failed. 
You have had quite some time to meet the challenge. I offer my 
help to help check the axioms for bugs before they appear on our list. 
I hope you will succeed in meeting the challenge so we can have a 
serious discussion.
Up to this point the challenge have only been meet by waffle..

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.

Soren Riis