Date: Mon, 27 Nov 1995 15:56:07 -0400 (AST)
Subject: local_set_theory

Date: Mon, 27 Nov 95 11:23:50 MET
From: koslowj@iti.cs.tu-bs.de

The following question concerning the book "Toposes and Local Set
Theories" by J. L. Bell was posed by Markus Michelbrink, a logician
from the University of Hannover.  I am just forwarding it to the list.

[Remark. The book has been reviewed for the Journal of Symbolic Logic by
G. C. Wraith shortly after it appeared.  The reviewer comments on the
author's unfortunate bias towards locally small categories.]

Markus has a problem with the footnote on p. 86.  For a local set theory S,
Bell proceeds to define a category C(S).  The footnote says:

"Strictly speaking, for this to be the case we need also show that the
collection of S-maps between any pair of S-sets forms an (intuitive)
set.  Actually, this follows easily from the assumption made initially
that the collection of function symbols of \cal L of a given signature
forms a set: we leave the proof to the reader."

Markus' argument, why this may not be so obvious, is as follows:

Form a local language \cal L with a proper class of ground type
symbols, and fix two arbitrary ground type symbols A' and B'.  For
every ground type symbol A let there be exactly one function symbol
f_A:PA --> P(A' x B').  The function symbols for any signature then
form a set, namely either the empty set, or a singleton.  Now for
any ground type symbol A there is a closed term

   f_A({x_A:true})

of type P(A' x B'), and for distinct ground type symbols A,B these
closed terms are distinct.  Hence we have a proper class of closed
terms of type P(A' x B').

Consider the local set theory S that is generated by the proper class
of sequents

   <\emptyset, f_A({x_A:true})\in {x_B':true}^{x_A':true}>

where A is a ground type symbol. [I.e., we require the f_A-image of A to
be a function from A' to B'.]

S induces an equivalence relation ~S via

   X ~S Y iff |-_S X=Y

This equivalence relation partitions the class of closed terms \tau of
type P(A' x B') with |-_S \tau \in {x_B':true}^{x_A':true}, i.e.,
those terms which represent functions from A' to B' in S.

Question 1: why should this partition have a *set* of representatives?

Question 2: can there be any distinct ground type sumbols A and B such
that f_A({x_A:true} and f_B({x_B:true} are S-equivalent?

[I hope the ASCII transcriptions and the occasional quasi-TeX are
self-explanatory.  Whoever has access to the book should be able to
follow the argument.]

Best regards,

-- J"urgen Koslowski
   Institut f\"ur Theoretische Informatik
   TU Braunschweig
   email: koslowj@iti.cs.tu-bs.de


Date: Tue, 28 Nov 1995 14:23:23 -0400 (AST)
Subject: Re: local_set_theory

Date: Tue, 28 Nov 95 10:12 GMT
From: Dr. P.T. Johnstone <P.T.Johnstone@pmms.cam.ac.uk>

Like Gavin Wraith, I commented adversely on Bell's insistence that
categories should be locally small, when I reviewed his book for the
L.M.S. Bulletin (vol.22 (1990), 101--102). But I failed to notice
the point raised by Michelbrink: I believe he has found a genuine
inconsistency in Bell's account of local set theories.

Peter Johnstone


Date: Tue, 28 Nov 1995 14:24:25 -0400 (AST)
Subject: local set theory

Date: Tue, 28 Nov 1995 09:45:23 -0500 (EST)
From: Andreas Blass <ablass@math.lsa.umich.edu>

This is in response to Michelbrink's question, posted on the network by
Koslowski, about the footnote on page 86 of Bell's "Toposes and Local Set
Theories."  I agree with Michelbrink that the footnote is incorrect, and
I pointed out the problem in my review of the book for Mathematical
Reviews (90e:18002 --- see Reviewer's Remark (3) near the end of the
review).

Andreas Blass