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 𝒫 1_o, like we do in our definition of EXMID (df-exmid 4210): then, we can prove ∀𝑥 ∈ 𝒫 1_o¬ ¬ DECID 𝑥 = 1_o but we cannot prove ¬ ¬ ∀𝑥 ∈ 𝒫 1_oDECID 𝑥 = 1_o 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

Step	Hyp	Ref	Expression
1		nnexmid 851	. 2 ⊢ ¬ ¬ (𝜑 ∨ ¬ 𝜑)
2		df-dc 836	. . 3 ⊢ (DECID 𝜑 ↔ (𝜑 ∨ ¬ 𝜑))
3	2	notbii 669	. 2 ⊢ (¬ DECID 𝜑 ↔ ¬ (𝜑 ∨ ¬ 𝜑))
4	1, 3	mtbir 672	1 ⊢ ¬ ¬ DECID 𝜑

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