FOM: Re: Categorical Foundations

[Colin Mclarty]

Reply to message from friedman at math.ohio-state.edu of Sun, 18 Jan
>
>Reply to a message from Mclarty, 10:59AM 1/18/98. The >> are from me.
>
>Mclarty's answer is quite sketchy and cryptic
        
       	I think you are more comfortable with your style of set 
theory, and so fill in more for yourself than you can do with 
categorical set theory.
        
>, and so I must read between
>the lines for an exact interpretation of what these analogs are that he is
>proposing. For this purpose, I use Saunders MacLane and Ieke Moerdijk,
>Sheaves in Geometry and Logic, A First Introduction to Topos Theory,
>Universitext, Springer-Verlag, 1992. If Mclarty has something other than
>what is in this book in mind when he answers me, then he is going to have
>to tell us explicitly how he differs from the MacLane/Moerdijk treatment
>and discussion.
        
       	I should also say how I differ from Lambek and Scott's
INTRODUCTION TO HIGHER ORDER CATEGORICAL LOGIC, in case someone
takes that as their reference, as well as Johnstone's TOPOS THEORY
and my own ELEMENTARY CATEGORIES, ELEMENTARY TOPOSES.
        
       	The differences are largely in choice of subject matter.
I am a bit more of a foundationalist than Mac Lane (much more
than Moerdijk or Johnstone, it seems to me), and less fond of the 
free topos than Lambek and Scott. I entirely agree with myself, but
I am not writing about all the same things here as in my book.
        
       	In my post I presented a calculus course based on categorical
set theory. Not an introduction to topos theory. This is analoguous
to you teaching calculus without Reverse mathematics. Do you cover
Reverse mathematics in your calculus course? 
        
>But there is a mismatch between what you will attempt to get away with
>saying, and almost all other courses in mathematics, and in fact most
>courses in all of science and engineering. 
        
       	No. Try to convince an engineer that the real function Log(x) 
is a set of complex numbers. And yet it is true in many textbooks if 
you take them seriously as ZF set theory: it is a set of pairs of 
reals. This is nonsense on my foundation, as it is in almost all 
courses in mathematics outside logic and set theory.
    
    	Or consider the intersection of the real numbers pi and e.
On my foundation this is strict nonsense. On ZF foundations it makes
perfect sense but is highly sensitive to details of the definitions:
In some textbooks it turns out to be e, in others pi, and in many
it is empty. On your view, students ought to demand to know which it is.
        
>At least mismatch in the sense
>that you will be using jargon that almost noone else knows or uses, and you
>will not be using standard ideas that everybody else knows and uses -
>except as modified by you in order to force it into your framework.
        
      	This just says that most mathematicians today do not teach
category theoretic foundations. Of course every idea is new at some 
time.
        
>There will also be a gross mismatch between the clear intellectual
>experiences of childhood - with the idea of a collection of 2 or 3 objects
>which can be counted - and the large amount of abstract nonsense that you
>need to promulgate.
        
       	You believe that when a child learns to count 2 or 3 cards 
on a table, that child is closer to conceiving of the cumulative 
heirarchy than to conceiving of a singleton 1 and an element as a 
function from 1. I think the child is not very close to either one, 
and can learn either one when the occasion arises.
        
>You have three primitive sorts: natural numbers, sets, and functions. You
>also have to deal with 1 and arrows and the like. And is 1 also 0? And you
>also need domains and codomains. You have a very complicated set of
>primitives. This is already going to cause trouble, confusion,
>difficulties,  and complications. In partcular, the last sentence above of
>yours will strike these students as abstract nonsense. What is 1? What does
>the arrows mean? I don't have this kind of trouble. I only worry about x
>epsilon y. Remember the little children with their collections of 2 or 3
>cards on the table?
        
       	The difference is that I must start out with more generalities
on functions than you. These are all things the students must learn
by the end of the calculus course either way. They do come in sooner 
in my course than yours.
    
    	In return my students are spared learning the von Neumann
ordinals. In fact, I and some of my friends were delighted with the
von Neumann ordinals when we first saw them in advanced courses
on foundations, but they are an acquired taste. And I doubt I would
have liked them much if my freshman calculus teacher had asked me
to learn about. At any rate, their set theoretic definition plays no
role in using the calculus--that is why so many different set
theoretic definitions of  natural numbers are equally acceptable.
        
    
>>	There is a set of natural numbers--I included this above.
>
>*A* set of natural numbers? or *the* set of natural numbers? 
        
       	"The" set N of natural numbers. Now, you and I both know
that N is not the only set with the required properties, it is just
the one I choose to call "N". On your approach you can uniquely 
define a set N, say the finite von Neumann ordinals, but you and I 
both know it is not the only set you could have used. And few 
students will thank you for the reassuring certainty that 3 is 
{0,{0},{0,{0}}}
        
>Students
>should want to know.
        
       	Why? The information is not even needed for a formally 
rigorous treatment in ZF. Moschovakis tells me his latest set theory
text gives all definitions up to isomorphism, though his 
primitives and axioms are standard ZFC.
        
> By the way, how is this stated formally? I.e., are you
>leaving out an axiom of extensionality? 
        
       	No. I have extensionality only for subsets of a given set.
And I stated this principle in my post, in clause 1. I can treat it
as an axiom, a definition, or a theorem, depending on exactly how I 
formalize the subject. That is a triviality. 
        
    
>What kind of equality do you have? The same kind as in set theoretic
>foundations? You have more of a problem than set theoretic foundations does
>because you have more sorts. 
    
    	This has come up in other posts. You find multi-sorted 
theories somehow problematic. I find them natural. Computer scientists 
find them natural. And all mathemtaics courses outside of logic
take them for granted. they use typeface to declare the sorts of 
variables:
    
    	"We use letters x, y, z to stand for real numbers, and
    	letters f, g, h for real valued functions of reals..."
    
    	"We use bold face letters for vectors, and italic for scalars..."
    
    	If you like I could formalize the whole in a language with
typed functions, but untyped equality. It is a triviality and would
only take us farther from mathematical practice. 
    
>How do you state and prove such clear
>trivialities as: there is exactly one function from any singleton into any
>other singleton.
    
    	This is my definition of singleton.
    
>Again, putting what I said with slightly different emphasis. What is the
>meaning of equality among functions?
    
    	It means they are the same function. As a theorem: two 
functions are identical iff they have the same graph.
    
>
>>>6. For any condition expressible with for all, there exists, and, or, not,
>>>if then, iff, membership, being a natural number, 0, and successor, if it
>>>holds of 0, and if whenever it holds at a natural number x, it holds of its
>>>successor S(x), then it holds of all natural numbers. Analog?
>>
>>	The same, verbatim
>
>How do you write this on the blackboard? Do you write, for all suitable
>formulas phi, if phi(0) and if for all natural numbers x, phi(x) implies
>phi(S(x)), then for all natural numbers x, phi(x)?
    
    	Sure, why not? And I could take it as an axiom on N, or as
a theorem based on the axiom that functions from N to other sets are
defined by recursion (primitive recursion, on one variable). Whichever
the students find easier. I'd have to see.
    
>You have to explain what a subset of a set is, in addition to an element of
>a set. This are troublesome, and look like abstract nonsense.
    
    	You have to explain the same things. Indeed it is "abstract
nonsense". Have you looked up the index references to "abstract
nonsense" in Lang's ALGEBRA? You use it constantly in algebra. Actually,
though, you have to look in the first two editions of Lang, since by 
the recent third edition mathematicians took abstract nonsense so much 
for granted the joke doesn't work anymore.
    

>I see that probably you can get away with a lot of what you are claiming to
>get away with if you use such a concept of generalized element. But it is
>foundationally incoherent. Remember those little children? They didn't
>think that the elements of that 3 element collection of cards on the table
>was a function!!
        
	I believe most children are agnostic on the formal definition or
axiomatic status of "element".

	Since this course only uses a topos of sets, I have no need
of generalized elements.

>So you are going to have to add something like "the internal logic of the
>topos is Boolean" fairly early in your courses. Plus maybe more. This will
>be received as a bunch of abstract nonsense.

	No, since in this course I am only talking about a topos of sets
I need not distinguish internal and external logic. I need only mention
to the students that subsets of sets have complements--something you will
also tell them.

>The more you sugar coat what you need, the more you slavishly translate set
>theory into an inferior notation.

	I would put it this way: The more I focus on analogues to your
methods, so that you can easily understand, the more the result will
look like your methods. I do not believe this damages my integrity.


>Now here is as promised a summary of the concepts that have to be developed
>in order to make topos theoretic foundations of mathematics really work in
>the way you intend. Note that these concepts are relatively arcane and
>abstract for our undergraduates:

	The concepts that follow are what I would need to teach
students the full range of categorical foundations. Imagine if you had
to start your calculus students with model theory, including models
of ZF--you have to tell them that in some models all sets of reals
are measurable.... 

	The difference is this: Model theory is so different from
ZF that (although many of the same people are expert on both) we are
not much tempted to give a unified treatment. Category theory gives
a uniform account of a great many foundations, quite divergent in their
content, and also unifies them with the standard working methods of
much mainstream mathematics, so we are quite drawn to unified
comprehensive accounts. But we don't have to give one to the first
year calculus class.   


>QUESTION: The book cited above only considers a notion of topos that
>corresponds in logical strength to that of Zermelo set theory with bounded
>separation. What about the axiom scheme of replacement? What does that look
>like in category theoretic terms?

	This has not drawn much interest among categorists. It only
comes up in response to questions from set theorists and the only
analogue I know of looks very much like the set theoretic one: It is
an axiom scheme, saying each suitably functional relation between
genralized elments of A and generalized elments of B is induced by an
arrow from A to B.

Colin