decidable object

An object XX of a well-behaved category (such as a topos) is decidable if its equality relation XX×XX\to X\times X is complemented, as a subobject of X×XX\times X.

This means that in the internal logic of the category, it is true that “for any x,yXx,y\in X, either x=yx=y or xyx\neq y.” Of course, in a Boolean category, every object is decidable.

In constructive mathematics, where Set is not assumed Boolean, one says that a set XX has decidable equality if it is a decidable object of Set\Set.

A decidable subobject simply means a complemented subobject. Again, in constructive mathematics, a decidable subobject in Set\Set is called a decidable subset.

Revised on July 4, 2009 11:54:06 by Toby Bartels (