**Description: **Double negation of
decidability of a formula. Intuitionistic logic
refutes the negation of decidability (but does not prove decidability) of
any formula.
This should not trick the reader into thinking that EXMID is
provable in intuitionistic logic. Indeed, if we could quantify over
formula metavariables, then generalizing nnexmid 836 over would
give "
DECID ", but EXMID
is "DECID ", so proving
EXMID would amount to
proving "
DECID ", which is not
implied by the above
theorem. Indeed, the converse of nnal 1626 does not hold. Since our system
does not allow quantification over formula metavariables, we can reproduce
this argument by representing formulas as subsets of , like we
do in our definition of EXMID (df-exmid 4151): then, we can prove
DECID
but we cannot prove
DECID
because the converse of nnral 2444 does
not hold.
Actually,
EXMID is not provable in intuitionistic logic since
intuitionistic logic has models satisfying EXMID and
noncontradiction holds (pm3.24 683). (Contributed by BJ, 9-Oct-2019.)
Add explanation on non-provability of EXMID. (Revised by BJ,
11-Aug-2024.) |