FOM: categorical dis-foundations Pratt/Franzen

[Colin Mclarty]

Vaughan Pratt wrote:

>In set theory the disjointness of the rationals and the irrationals
>follows immediately from first principles.  In category theory their
>disjointness is not a foregone conclusion by any means (see below),
>and I would not be surprised if the above required wellpointedness.
>I also would expect that this and a few other Lakatosian monsters would
>provide the only occasions where well-pointedness was needed in applying
>topos theory to analysis, if such monsters can even be considered part
>of analysis.

	What Pratt says is essentially true, but playfully put. The
disjointess of Q and R-Q in R, is half of the definition of R-Q (the
other half is that R-Q is maximal among subsets of R disjoint from
Q). But in more general contexts than categorical set theory the
law of excluded middle fails, and since "irrational" is defined by a
negation you can expect some non-classical behavior. In these
contexts Q and R-Q do not jointly exhaust R. In Isbell's setting
the "irrationals" are more than just R-Q, though they are a subset
of R which does not assertably contain anything that is assertably 
in Q. Niether is their intersection with Q assertably empty. In the 
axioms I gave, excluded middle is implied by well-pointedness.


Torkel Franzen wrote some comments on schematic predicate variables
in first order logic. I agree with what he wrote, and I think these
schematic variables are a nice device. But I still say:

	They are not the standard method of first order logic. This
is why textbooks routinely say what Simpson also said--that Peano
arithmetic and Zermelo set theory have no finite axiomatization.
The day may come when people more often say "Zermelo set theory has
no finite axiomatization without schematic variables" but that is
not what they usually say today.

	Friedman himself in his original posting of the axioms
explicitly used axiom schemes, quantifying in the meta-language
over formulas of set theory, rather than using schematic variables.
I have not yet understood his explanation yesterday, that he thought
schematic variables are so familiar that it was better not to just
use them explicitly.

	Simpson yesterday accurately characterized my claim that
Friedman was using infinitely many first order axioms. He said
this was "not necessarily a disadvantage" of my system, but also
not important, and not the main issue. Simpson did not say I was
just wrong--and he has shown no hesitance about that in the past.
So I conclude he did not think I was just wrong. Neither he nor
I thought Friedman was using schematic variables.

	None of this argues against schematic variables, it only
argues that they are not standard, and if you are using them you
should say so. Specifying your logic is part of giving your
axioms.

	This is what I take from Mac Lane saying that formal
axiomatization is a way of making mistakes and not of avoiding
them: formal axiomatization is itself a substantial part of
exploring a given idea. It can reveal much, because it says
much, (and by the same token that means it can be wrong). It
is not a pristine refuge from error, nor can we take the means
of formalization for granted as contributing nothing to the
complexity of a formal theory--there are many different means
available and they do differ in complexity.

	I will reply directly to Friedman's post of yesterday,
but I am at home now and cannot access it, and I am about to rush
out the door to present my view of the Abelian category debate
on fom last fall, at noon at the Center for Philosophy of Science
at Pittsburgh. I will mention the fom, but will only quote people's
published writing.

Colin