All, This is an argument about effective theories and so i would love to hear from the topos-theory crowd. i'll state the argument in lowly computational terms, using two distinct proposals for foundational models of computing: the lambda calculus and the π-calculus. Both the lambda calculus and the π-calculus suffer a dependence on a theory of names (aka variables). Both require two things of whatever theory of names is provided to them: - at least countably infinitely many names - an effective equality on names Now, to this recent proposals[1] add a third constraint, namely - names are atomic -- they have no internal structure To my way of thinking these three constraints are incompatible. i cannot see how to make an effective equality on a countably infinite set of entities that have no internal structure on which to rest the equality check. It seems to me that the only possible expression of the equality is an infinite table which states the results of comparing every single pair of atoms -- which is not going to fit into any realizable model of computation of which i'm aware and understand. Is there a way around this? If there is, i would be eternally grateful to be enlightened. The reason i focus on foundational proposals for theories of computation is that one could drop the atomic requirement and allow names to have internal structure, but because of the other two constraints one is dangerously close to sneaking into a supposedly foundational account a theory of names that is -- itself -- already sufficiently rich to model computation. (For example, in many implementations of lambda or π-calculus, names are ultimately represented as integers.) This would appear to undermine the foundational character of the model of computation in question. This has led me to constructions in which the internal structure of names *reflects* the structure of computations. In fact, this idea has a simple monadic characterization, but that's for another discussion. i've already posted to this list an intuitive account of red/black set theories that also side-step the issue of atoms with no structure which allows to recast the FM-Set-Theory-based accounts of names onto what appears to me to be the only construction that meets all the requirements mentioned above: sufficiently many names, effective equality, restricting internal structure of names to the structure of the proposal at hand. Again, if there is a way to skate around this argumentation or debunk it, please consider this a sincere call for help to do so. Best wishes, --greg [1] See the Gabbay-Pitts papers on using FM-Set Theory for an account of fresh names and alpha-equivalence. -- L.G. Meredith Managing Partner Biosimilarity LLC 1219 NW 83rd St Seattle, WA 98117 +1 206.650.3740 http://biosimilarity.blogspot.com [For admin and other information see: http://www.mta.ca/~cat-dist/ ]