Dear Gregory, I think the problem resides in what you mean by "no internal structure". If by this you mean that the *set* of names has no internal structure, then it's obviously impossible -- to require the set to have decidable equality is to impose internal structure on it. But it's still possible for the names themselves to be atomic: you can identify the set of names with the set of natural numbers (which has lots of internal structure, including decidable equality) without identifying the individual names with von Neumann-style natural numbers (or Russell-style cardinals, or ...) Peter Johnstone On Thu, 25 Jun 2009, Meredith Gregory wrote:
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
... [For admin and other information see: http://www.mta.ca/~cat-dist/ ]