Theorem nndc 846

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 845 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 1642 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 4179): then, we can prove ∀𝑥 ∈ 𝒫 1_o¬ ¬ DECID 𝑥 = 1_o but we cannot prove ¬ ¬ ∀𝑥 ∈ 𝒫 1_oDECID 𝑥 = 1_o because the converse of nnral 2460 does not hold.

Actually, ¬ ¬ EXMID is not provable in intuitionistic logic since intuitionistic logic has models satisfying ¬ EXMID and noncontradiction holds (pm3.24 688). (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 845	. 2 ⊢ ¬ ¬ (𝜑 ∨ ¬ 𝜑)
2		df-dc 830	. . 3 ⊢ (DECID 𝜑 ↔ (𝜑 ∨ ¬ 𝜑))
3	2	notbii 663	. 2 ⊢ (¬ DECID 𝜑 ↔ ¬ (𝜑 ∨ ¬ 𝜑))
4	1, 3	mtbir 666	1 ⊢ ¬ ¬ DECID 𝜑

Syntax hints:  ¬ wn 3   ∨ wo 703  DECID wdc 829

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 609  ax-in2 610  ax-io 704

This theorem depends on definitions:  df-bi 116  df-dc 830

This theorem is referenced by:  bj-dcdc  13715  bj-stdc  13716