| 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 862 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 1702 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 4330): then, we can prove
  DECID 
but we cannot prove
DECID
because the converse of nnral 2540 does
not hold.
Actually,
EXMID is not provable in intuitionistic logic since
intuitionistic logic has models satisfying EXMID and
noncontradiction holds (pm3.24 705). (Contributed by BJ, 9-Oct-2019.)
Add explanation on non-provability of EXMID. (Revised by BJ,
11-Aug-2024.) |
