Intuitionistic Logic Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  ILE Home  >  Th. List  >  nndc Unicode version

Theorem nndc 837
 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.)
Assertion
Ref Expression
nndc DECID

Proof of Theorem nndc
StepHypRef Expression
1 nnexmid 836 . 2
2 df-dc 821 . . 3 DECID
32notbii 658 . 2 DECID
41, 3mtbir 661 1 DECID
 Colors of variables: wff set class Syntax hints:   wn 3   wo 698  DECID wdc 820 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-in1 604  ax-in2 605  ax-io 699 This theorem depends on definitions:  df-bi 116  df-dc 821 This theorem is referenced by:  bj-nnst  13269  bj-dcdc  13270  bj-stdc  13271
 Copyright terms: Public domain W3C validator