FOM: Comments on Riis

[Carsten Butz]

Dear Soren,

this is my response to your postings on fom dated
Thu, 5 Feb 1998 14:57:53 and
Fri, 6 Feb 1998 15:16:16.

In my opinion you get some things wrong, even though you carefully
state a position which is held by many people. 

(IHOL, once again)
You argue partly against IHOL as a foundation. You are partly
right. The reason might be that we have not been very precise. Let me
state again what (according to me) IHOL is. For the exact reference I
refer to [Lambek-Scott] again (p.130/131).
It is, I agree, more like a language, which has
- basic types, including the type \Omega (for the truth values)
  and a so called one-element type.
- type forming operations \times (product) and P (power-object)
- some (typed) constants, function and relation symbols.
On top of this "signature" there is a usual language of higher order
logic. The rules for the entailment relation include
- structural rules like weakening and modus ponens
- logical rules that support intuitionistic logic
- and extra logical rules that contain
  comprehension
  extensionality
  and rules for product types.
Nothing else.

A theory could then contain some more axioms like axioms for
booleaness or whatever you like.

(Categorical) models of these type theories are (elementary)
toposes. Are they enough to do intuitionistic analysis? No, of course
not in general, since we need something like the natural numbers. So
what we need is a type N for the natural numbers, and the three Peano
axioms. This is certainly enough. Then we get elementary toposes with
a natural number object. But then it is out of the question that we
can do analysis. 
  If you do not believe that, I cannot help you. Believe me as a
colleague! You as well should know that what is needed to get of the
ground are really the natural numbers. I do not understand your
hesitation. 

(Consensus?)
  You ask for a consensus. The minimal consensus we can achieve is
that topos theory (similar as set-theory) is the mathematical
discipline that studies categorical models of intuitionistic higher
order theories. If you damn set-theory from foundation as well (as
Harvey Friedman did, if I remember correctly) I can live with a
similar statement for topos theory (for the moment).

  This brings back a question I raised that was never answered: You
probably think that fom (as opposed to set-theory) is about THE
underlying universe of sets? I guess, yes, and you say something like
this in your mail. Topos theorists do the same: They work in a base
topos, usually called SETS (or S).

(Computers)
  Your whole mail is based on your example using a programmed
computer. 
  I disagree with everything you say. To quote from your mail:
[begin quote]
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.
[end quote]
A computer can never ever produce truth. It can only generate
according to rules. So if you program it with ZF and the standard
classical rules of inference, it will eventually answer your question
with yes, as it will if you programmed it with an inconsistent
theory. Your program will not give an answer to ?AC, or to a question
about large cardinals, and my program (since I programme
intuitionistic deduction rules) will not give an answer to the
maximum-value principle. What is this supposed to show? In my opinion
it just shows nothing. 

(Interesting theorems)
  You are hunting for good theorems? Good so. 

(Deductive strength)
[begin quote]
- 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)
[end quote]

I didn't know that one is unscientific if one questions some of the
"standard" principles. Your claim for maximal deductive strength is
unfortunately empty as well: Accepting the axiom of choice, its
negation, Martins axiom, or some large cardinal axiom or
whatever does not make them true, whatever this means. It is nice,
gives strong results, but from the point of view of foundations very
questionable. In contrast, minimal deductive strength gives a strong
foundational position, the same applies to weak axioms. This is the
reason why Harvey Friedmans program has my sympathy. 

(Category theory as a theory)
[begin quote]
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. 
[end quote]
You forgot something in your list: The axioms of ZF are as well just a
theory. But for ZF you allow two ways to look at: As a mathematical
theory, and as foundations. Whereas you do not allow this for category
theory. I disagree. As I argued before, viewed as foundations, the
axioms of a category capture the intuition of
operation/movement/action. They are, as well, a mathematical theory. 

[begin quote]
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 
[end quote]
Partly right (see above), partly wrong: We always assume the existence
of a base topos, the topos in which we live. This is our commitment to
ONE universe, i.e., one topos. 

(Mysticism and LSD)
I have no answers to you, I am confused how someone can write
something like this, so I just quote from your mail and leave it to
others to respond.
[begin quote]
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.
[end quote]
By the way, statements like this caused me to raise the (slightly
misunderstood) question about truth. 

(Victory and Consense)
[begin quote]
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.
[end quote]

I am disapointed that you cannot separate consense from victory. My
statement was certainly not victory (as well not surrender). 

(Ontological commitment)
  Here is something we might agree on. Any fom'er has to say about
what his foundational axioms are: Set-based fom'ers say about
collections, category-based fom'ers say about collections and
operations on collections (I used for good reasons in an earlier
posting the word domain instead of collections).
  What is so wrong for you with this second position? 

(FLT)
[begin quote]
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.
[quote]

Again, in my opinion you are wrong. X (to avoid the problem of
credits) did not prove FLT. As a logician, you should know that this
is impossible. Any proof, really any claimed proof has to say which
rules it used (name a calculus), and then, give the proof. And this
proof will start with assumptions (about the natural numbers, in this
case). If Mister X wants his "proof" be checked, at one point or
another he will have to say on which assumptions it is based. And he
will come up with something like ZF, Peano arithmethic or something
else. He has to.
  Of course, he will say (this is the character of these kind of
assumptions) "they are evident". Still, there they are. 

(Normative and Descriptive character of fom)
  The original character of the questions in fom are of descriptive
character: The aim was to describe the basic assumptions on which our
mathematical reasoning relies. This implies some axioms which we might
believe in, and rules for deduction. (In this respect, first order
logic, or being more precise, the calculus of first order logic, is
perfectly fom, well, may be better, fot, foundation of thought.)
  After some time, after one has agreed on some of the points, or
after one has at least clarified where the differences are,
fom gets as well a normative character, in the sense that one tends
to formulate one's results/proofs in a way that they could be
formalized in one of the formal set-ups.  
  As Moshe' Machover (Fri, 6 Feb 1998 22:06:53) has pointed out
correctly, the rules we accept can change, as can the axioms we
accept.


Best regards,

  Carsten Butz

Carsten Butz
Research Associate
Department of Computer Science, University of Aarhus (Denmark)
Research interests: Categorical logic, topos theory, homological algebra
WWW: http://www.brics.dk/~butz/