A proposition is decidable if we know whether it is true or false. This has (at least) two interpretations, which we will call ‘internal’ and ‘external’; however, these adjectives are rarely used and must be guessed from the context.
In logic, a proposition in a given theory (or in a given context of a given theory) is externally decidable if there is in that theory (or in that context) a proof of or a refutation of (a proof of ). Of course, this only makes sense if the logic of the theory includes an operation of negation.
Any statement that can be proved or refuted is decidable, and one might hope for a consistent foundation of mathematics in which every statement is decidable. However, Gödel's incompleteness theorem? dashes these hopes; any consistent theory? strong enough to model arithmetic (actually a rather weak form of arithmetic) must contain undecidable statements.
In constructive mathematics, a proposition is internally decidable if the law of excluded middle applies to ; that is, if holds. Of course, in classical mathematics, every statement is decidable in this sense. Even in constructive mathematics, some statements are decidable and no statement is undecidable; that is, is always false, but this is not enough to guarantee that is true.
For example, consider the Riemann hypothesis (or any of the many unsolved -propositions? in number theory). This may be expressed as for some predicate on natural numbers. For each , the statement is decidable (that is, holds), and indeed one can in principle work out which with pencil and paper. However, the Riemann hypothesis itself has not yet been proved (constructively) to be decidable.
A set has decidable equality if every equation between elements of (every proposition for in ) is decidable. A subset of a set is a decidable subset if every statement of membership in (every proposition for in ) is decidable.
In many foundations of constructive mathematics, the disjunction property? holds (in the global context). That is, if can be proved, then either can be proved or can be proved. By Gödel's incompleteness theorem, no consistent foundation of classical arithmetic can have this property, but some consistent foundations of intuitionistic arithmetic (such as Heyting arithmetic?) do.
In any consistent logic with the disjunction property, a proposition is externally decidable if and only if it can be proved to be internally decidable. (Note that the claim that is externally decidable is a statement in the metalanguage, while the claim that is internally decidable is a statement in the object language.)
Under this correspondence, the contexts of correspond to the objects of , and the propositions in a given context correspond to the subobjects of that object. Then a proposition in a context is externally decidable if and only if it is, as a subobject of , either itself (corresponding to being provable) or the initial object (corresponding to being refutable). And a proposition in the context is internally decidable if and only if, when thought of as a subobject of , the union of and is .
The slice category is two-valued if and only if the context is consistent and every proposition in that context is externally decidable. is a Boolean category if and only if every proposition in every context is internally decidable.
This makes me think that we should define to be externally decidable iff is provable whenever it is not refutable, which in a constructive metalogic is weaker than the definition above. But then we lose the relationship with the disjunction property. I guess that we need intuitionistic, classical, and paraconsistent forms of external decidability, just as for two-valuedness.