| 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 840 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 1637 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 4174): then, we can prove
  DECID 
but we cannot prove
DECID
because the converse of nnral 2456 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.) |
