An object of a well-behaved category (such as a topos) is decidable if its equality relation is complemented, as a subobject of .
This means that in the internal logic of the category, it is true that “for any , either or .” Of course, in a Boolean category, every object is decidable.
In constructive mathematics, where Set is not assumed Boolean, one says that a set has decidable equality if it is a decidable object of .
A decidable subobject simply means a complemented subobject. Again, in constructive mathematics, a decidable subobject in is called a decidable subset.
Revised on July 4, 2009 11:54:06
by Toby Bartels