Description: Propositions which are
known to be true or false are called decidable.
The (classical) Law of the Excluded Middle corresponds to the principle
that all propositions are decidable, but even given intuitionistic logic,
particular kinds of propositions may be decidable (for example, the
proposition that two natural numbers are equal will be decidable under
most sets of axioms).
Our notation for decidability is a connective DECID which
we place
before the formula in question. For example, DECID corresponds
to " is decidable".
We could transform intuitionistic logic to classical logic by adding
unconditional forms of condc 848, exmiddc 831, peircedc 909, or notnotrdc 838,
any of which would correspond to the assertion that all propositions are
decidable.
(Contributed by Jim Kingdon, 11-Mar-2018.) |