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