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).
External decidability: either or may be deduced in the theory. This is a statement in the metalanguage.
Internal decidability: may be deduced in the theory; in other words “ or not ” holds in the object language.
There are another two interpretations, which interpret “or” as exclusive disjunction rather than inclusive disjunction:
External decidability: that exactly one of or holds may be deduced in the theory. This is a statement in the metalanguage.
Internal decidability: may be deduced in the theory; in other words “exactly one of or not holds” holds in the object language.
The versions using exclusive disjunction are equivalent to the versions using inclusive disjunction. This is because implies its double negation, so if “ or not ”, then one can prove that “not or not not ”, which means that or not implies that “( or not ) and (not or not not )”, the latter of which is the exclusive disjunction of and its negation. And exclusive disjunction implies inclusive disjunction by definition.
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 the negation ). 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.
For example, the continuum hypothesis is undecidable in ZFC, assuming that is consistent at all.
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.)
The internal logic of any Heyting category is a type theory in first-order intuitionistic logic; conversely, any such theory has a category of contexts which is a Heyting category.
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.
In dependent type theory, a decidable proposition is a mere proposition which comes with an element , where is the disjunction of two types and , is the negation of type , is the sum type of types and , and is the propositional truncation of type .
Last revised on September 7, 2024 at 13:46:48. See the history of this page for a list of all contributions to it.