Theorem dcfromcon 1491

Description: The decidability of a proposition 𝜒 follows from a suitable instance of the principle of contraposition. Therefore, if we were to introduce contraposition as a general principle (without the decidability condition in condc 858), then we could prove that every proposition is decidable, giving us the classical system of propositional calculus (since the principle of contraposition is itself classically valid). (Contributed by Adrian Ducourtial, 6-Oct-2025.)

Hypotheses

Ref	Expression
dcfromcon.1	⊢ (𝜑 ↔ (𝜒 ∨ ¬ 𝜒))
dcfromcon.2	⊢ (𝜓 ↔ ⊤)
dcfromcon.3	⊢ ((¬ 𝜑 → ¬ 𝜓) → (𝜓 → 𝜑))

Assertion

Ref	Expression
dcfromcon	⊢ DECID 𝜒

Proof of Theorem dcfromcon

Step	Hyp	Ref	Expression
1		nnexmid 855	. . . . 5 ⊢ ¬ ¬ (𝜒 ∨ ¬ 𝜒)
2	1	pm2.21i 649	. . . 4 ⊢ (¬ (𝜒 ∨ ¬ 𝜒) → ¬ ⊤)
3		dcfromcon.3	. . . . 5 ⊢ ((¬ 𝜑 → ¬ 𝜓) → (𝜓 → 𝜑))
4		dcfromcon.1	. . . . . . 7 ⊢ (𝜑 ↔ (𝜒 ∨ ¬ 𝜒))
5	4	notbii 672	. . . . . 6 ⊢ (¬ 𝜑 ↔ ¬ (𝜒 ∨ ¬ 𝜒))
6		dcfromcon.2	. . . . . . 7 ⊢ (𝜓 ↔ ⊤)
7	6	notbii 672	. . . . . 6 ⊢ (¬ 𝜓 ↔ ¬ ⊤)
8	5, 7	imbi12i 239	. . . . 5 ⊢ ((¬ 𝜑 → ¬ 𝜓) ↔ (¬ (𝜒 ∨ ¬ 𝜒) → ¬ ⊤))
9	6, 4	imbi12i 239	. . . . 5 ⊢ ((𝜓 → 𝜑) ↔ (⊤ → (𝜒 ∨ ¬ 𝜒)))
10	3, 8, 9	3imtr3i 200	. . . 4 ⊢ ((¬ (𝜒 ∨ ¬ 𝜒) → ¬ ⊤) → (⊤ → (𝜒 ∨ ¬ 𝜒)))
11	2, 10	ax-mp 5	. . 3 ⊢ (⊤ → (𝜒 ∨ ¬ 𝜒))
12	11	mptru 1404	. 2 ⊢ (𝜒 ∨ ¬ 𝜒)
13		df-dc 840	. 2 ⊢ (DECID 𝜒 ↔ (𝜒 ∨ ¬ 𝜒))
14	12, 13	mpbir 146	1 ⊢ DECID 𝜒

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 105   ∨ wo 713  DECID wdc 839  ⊤wtru 1396

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 617  ax-in2 618  ax-io 714

This theorem depends on definitions:  df-bi 117  df-dc 840  df-tru 1398

This theorem is referenced by: (None)