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

Theorem nndc 851
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 850 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 1647 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 4190): then, we can prove 𝑥 ∈ 𝒫 1o¬ ¬ DECID 𝑥 = 1o but we cannot prove ¬ ¬ ∀𝑥 ∈ 𝒫 1oDECID 𝑥 = 1o because the converse of nnral 2465 does not hold.

Actually, ¬ ¬ EXMID is not provable in intuitionistic logic since intuitionistic logic has models satisfying ¬ EXMID and noncontradiction holds (pm3.24 693). (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 850 . 2 ¬ ¬ (𝜑 ∨ ¬ 𝜑)
2 df-dc 835 . . 3 (DECID 𝜑 ↔ (𝜑 ∨ ¬ 𝜑))
32notbii 668 . 2 DECID 𝜑 ↔ ¬ (𝜑 ∨ ¬ 𝜑))
41, 3mtbir 671 1 ¬ ¬ DECID 𝜑
Colors of variables: wff set class
Syntax hints:  ¬ wn 3  wo 708  DECID wdc 834
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 614  ax-in2 615  ax-io 709
This theorem depends on definitions:  df-bi 117  df-dc 835
This theorem is referenced by:  bj-dcdc  14071  bj-stdc  14072
  Copyright terms: Public domain W3C validator