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

Theorem nndc 852
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 851 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 1660 does not hold. Since our system does not allow quantification over formula metavariables, we can reproduce this argument by representing formulas as subsets of 𝒫 1o, like we do in our definition of EXMID (df-exmid 4210): then, we can prove 𝑥 ∈ 𝒫 1o¬ ¬ DECID 𝑥 = 1o but we cannot prove ¬ ¬ ∀𝑥 ∈ 𝒫 1oDECID 𝑥 = 1o because the converse of nnral 2480 does not hold.

Actually, ¬ ¬ EXMID is not provable in intuitionistic logic since intuitionistic logic has models satisfying ¬ EXMID and noncontradiction holds (pm3.24 694). (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 851 . 2 ¬ ¬ (𝜑 ∨ ¬ 𝜑)
2 df-dc 836 . . 3 (DECID 𝜑 ↔ (𝜑 ∨ ¬ 𝜑))
32notbii 669 . 2 DECID 𝜑 ↔ ¬ (𝜑 ∨ ¬ 𝜑))
41, 3mtbir 672 1 ¬ ¬ DECID 𝜑
Colors of variables: wff set class
Syntax hints:  ¬ wn 3  wo 709  DECID wdc 835
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-in1 615  ax-in2 616  ax-io 710
This theorem depends on definitions:  df-bi 117  df-dc 836
This theorem is referenced by:  bj-dcdc  14908  bj-stdc  14909
  Copyright terms: Public domain W3C validator