From -6257857629392295245
X-Google-Language: ENGLISH,ASCII-7-bit
X-Google-Thread: 10d29f,5dde8bc04e55ff60
X-Google-Attributes: gid10d29f,public
X-Google-ArrivalTime: 2002-08-29 10:00:01 PST
Path: archiver1.google.com!news1.google.com!newsfeed.stanford.edu!news.uchicago.edu!vixen.cso.uiuc.edu!not-for-mail
X-Coding-System: undecided-unix
From: "Vidhyanath Rao" <nathrao+@osu.edu>
Newsgroups: sci.math.research
Subject: Re: Automatic Theorem Prover
Message-ID: <aklihk$j5j$3@charm.magnus.acs.ohio-state.edu>
References: <Pine.LNX.4.44.0208131846250.1580-100000@pu-217-129-13-4.netvisao.pt> <remove.haberg-2308021302110001@du130-226.ppp.su-anst.tninet.se> <ak9cr2$3mp$1@charm.magnus.acs.ohio-state.edu> <remove.haberg-2508021324250001@du131-226.ppp.su-anst.tninet.se> <3d691c80$0$3928$b45e6eb0@senator-bedfellow.mit.edu> <remove.haberg-2608020116200001@du128-226.ppp.su-anst.tninet.se> <c616467c.0208261056.1e39b409@posting.google.com>
Content-Transfer-Encoding: 7bit
X-Priority: 3
X-MSMail-Priority: Normal
X-MimeOLE: Produced By Microsoft MimeOLE V5.50.4807.1700
Approved: Daniel Grayson <dan@math.uiuc.edu>, moderator for sci.math.research
Lines: 78
Date: Thu, 29 Aug 2002 12:30:08 -0400
NNTP-Posting-Host: 130.126.108.30
X-Complaints-To: abuse@uiuc.edu
X-Trace: vixen.cso.uiuc.edu 1030640239 130.126.108.30 (Thu, 29 Aug 2002 11:57:19 CDT)
NNTP-Posting-Date: Thu, 29 Aug 2002 11:57:19 CDT
Organization: University of Illinois at Urbana-Champaign
Xref: archiver1.google.com sci.math.research:4186


"John Harrison" <jo...@ichips.intel.com> wrote in message
news:c616467c.02082...@posting.google.com...
I should perhaps add the disclaimer that I am not interested in first
order vs higher order (which seems to do me, an admitted non-Platonist,
more to do with philosophy than axiomatics/formalization as error
avoiding methods) unless we see classes as extensions of properties, but
then, of course, we can turn that into a two-sorted first order theory
and leave philosphy to philosophers.

> Incidentally, if we are considering merely formalization "in principle"
> of proofs involving intermediate category-theoretic notions, it seems
> likely that the use of universe axioms is not necessary, as a consequence
> of the Reflection Principle. This point is made by Kreisel; cf. Saaty,
> "Lectures on Modern Mathematics III", p118.

A better reference would be Feferman's paper in "Reports of the Midwest
Category Seminar III". That goes into more detail. However, that is old
and predates some constructions that have turned out be crucial in
algebraic topology (and, AFAIK, algebraic geometry). This makes the
above remark more troublesome.

Unfortunately, to explain the problem, I need to be longwinded and tax
everybody's patience. I hope people will excuse it just once.

---

ZF(C) + RP (reflection principle) addes a primitive constant V along
with an axiom scheme that says that a statement in the language of ZF is
true if and only if its relativization to V is. If we interpret the
elements of V as sets and arbitrary 'sets' as classes, this implies all
the axioms of Ackermann's set theory (A. Levy). On the other hand, all
the axioms of ZF are true for sets in Ackermann's set theory +
Regularity (Reinhardt for replacement, Ackermann already had proved
others). So the main difference between the two is that ZFC+RP has more
familiar (and stronger?) class construction methods. But the former is
still sets+classes (but called 'small sets' and 'large sets' in
imitation of categorists' terms).

The rub is that we need to be careful about the replacement axiom in
ZFC+RP. A common step in category theory is to take a functor F : A to C
into a complete category C and a small diagram D in A and then take the
limit of F(D). This cannot be done in ZFC+RP. We have to assume that F
takes small sets of morphisms into small sets, which is true if F is
definable but not in general. (this may help understand the difference:
A well order of reals exists in ZFC, but is not definable). Along the
same lines, we often have to impose grwoth conditions on abstract
categories, such as "every small set of morphisms is contained in a
small subcategory that reflects isomorphisms", redefine 'locally small'
as "every small set of objects is contained in a small full subcategory"
and worry about which constructions preserve such properties. We also
have to worry about existence of transfinite iterations [If F : C to C
is an endofunctor of a cocomplete category with a natural transformation
from Id to F, define F^\alpha by F^{\alpha+1} = F F^{\alpha}, and if
\alpha is limit ordinal, then F^{\alpha} is the colimit of F^{\beta},
\beta < \alpha. These occur in constructions of localizations] and
growth conditions on them. Ditto for simplicial objects from monads
(which may come from localiztions which may be transfinite iterations)
and realizations of such simplicial objects collected into a whole as a
functor. My gut feeling is that this is doable. But >far< from trivial.
For example, Neeman's book on triangulated categories takes scores of
pages to show that localizations of locally small triangulated
categories with suitable properties (that are fulfilled in intended
applications) are still locally small. We will need to modify this for
the new definition of locally small. Nor is this a marginal example:
Neeman's book is intended as a careful treatment of the prerequisites
for Voedovsky's applications to motives.

There is also a technical point: Some constructions involve choice. So
not all functors used may be definiable in the language of ZFC. We can
get around this by taking (ZF + global choice) + RP, which assumes
reflection for statements involving choice function symbol also. This is
a priori richer than ZF+RP+choice. The former is almost certainly a
conservative extension of ZFC, but this still needs to be checked.