nLab decidable proposition

Decidable propositions

Decidable propositions

Idea

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).

There are another two interpretations, which interpret “or” as exclusive disjunction rather than inclusive disjunction:

The versions using exclusive disjunction are equivalent to the versions using inclusive disjunction. This is because pp implies its double negation, so if “pp or not pp”, then one can prove that “not pp or not not pp”, which means that pp or not pp implies that “(pp or not pp) and (not pp or not not pp)”, the latter of which is the exclusive disjunction of pp and its negation. And exclusive disjunction implies inclusive disjunction by definition.

Externally decidable propositions in logic

In logic, a proposition pp 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 pp or a refutation of pp (a proof of the negation ¬p\neg{p}). 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 ZFCZFC is consistent at all.

Internally decidable propositions in constructive mathematics

In constructive mathematics, a proposition pp is internally decidable if the law of excluded middle applies to pp; that is, if p¬pp \vee \neg{p} 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, ¬(p¬p)\neg{(p \vee \neg{p})} is always false, but this is not enough to guarantee that p¬pp \vee \neg{p} is true.

For example, consider the Riemann hypothesis (or any of the many unsolved Π 1\Pi_1-propositions? in number theory). This may be expressed as x,P(x)\forall x, P(x) for PP some predicate on natural numbers. For each xx, the statement P(x)P(x) is decidable (that is, x,P(x)¬P(x)\forall x, P(x) \vee \neg{P(x)} 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 AA has decidable equality if every equation between elements of AA (every proposition x=yx = y for x,yx, y in AA) is decidable. A subset BB of a set CC is a decidable subset if every statement of membership in BB (every proposition xBx \in B for xx in AA) is decidable.

Relation between these

In many foundations of constructive mathematics, the disjunction property? holds (in the global context). That is, if pqp \vee q can be proved, then either pp can be proved or qq 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 pp is externally decidable is a statement in the metalanguage, while the claim that pp is internally decidable is a statement in the object language.)

Categorial interpretation

The internal logic of any Heyting category CC is a type theory in first-order intuitionistic logic; conversely, any such theory TT has a category of contexts which is a Heyting category.

Under this correspondence, the contexts of TT correspond to the objects of CC, and the propositions in a given context correspond to the subobjects of that object. Then a proposition in a context XX is externally decidable if and only if it is, as a subobject of XX, either XX itself (corresponding to being provable) or the initial object (corresponding to being refutable). And a proposition in the context XX is internally decidable if and only if, when thought of as a subobject AA of XX, the union of AA and ¬A\neg{A} is XX.

The slice category C/XC/X is two-valued if and only if the context XX is consistent and every proposition in that context is externally decidable. CC is a Boolean category if and only if every proposition in every context is internally decidable.

This makes me think that we should define pp to be externally decidable iff pp 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

In dependent type theory, a decidable proposition is a mere proposition PP which comes with an element lem P:P¬P\mathrm{lem}_P:P \vee \neg P, where AB[A+B]A \vee B \coloneqq [A + B] is the disjunction of two types AA and BB, ¬AA\neg A \coloneqq A \to \emptyset is the negation of type AA, A+BA + B is the sum type of types AA and BB, and [A][A] is the propositional truncation of type AA.

isDecidable(P)isProp(P)×(P¬P)\mathrm{isDecidable}(P) \coloneqq \mathrm{isProp}(P) \times (P \vee \neg P)

Last revised on September 7, 2024 at 13:46:48. See the history of this page for a list of all contributions to it.