Definition df-exmid 4196

Description: The expression EXMID will be used as a readable shorthand for any form of the law of the excluded middle; this is a useful shorthand largely because it hides statements of the form "for any proposition" in a system which can only quantify over sets, not propositions.

To see how this compares with other ways of expressing excluded middle, compare undifexmid 4194 with exmidundif 4207. The former may be more recognizable as excluded middle because it is in terms of propositions, and the proof may be easier to follow for much the same reason (it just has to show 𝜑 and ¬ 𝜑 in the the relevant parts of the proof). The latter, however, has the key advantage of being able to prove both directions of the biconditional. To state that excluded middle implies a proposition is hard to do gracefully without EXMID, because there is no way to write a hypothesis 𝜑 ∨ ¬ 𝜑 for an arbitrary proposition; instead the hypothesis would need to be the particular instance of excluded middle which that proof needs. Or to say it another way, EXMID implies DECID 𝜑 by exmidexmid 4197 but there is no good way to express the converse.

This definition and how we use it is easiest to understand (and most appropriate to assign the name "excluded middle" to) if we assume ax-sep 4122, in which case EXMID means that all propositions are decidable (see exmidexmid 4197 and notice that it relies on ax-sep 4122). If we instead work with ax-bdsep 14639, EXMID as defined here means that all bounded propositions are decidable.

(Contributed by Mario Carneiro and Jim Kingdon, 18-Jun-2022.)

Assertion

Ref	Expression
df-exmid	⊢ (EXMID ↔ ∀𝑥(𝑥 ⊆ {∅} → DECID ∅ ∈ 𝑥))

Detailed syntax breakdown of Definition df-exmid

Step	Hyp	Ref	Expression
1		wem 4195	. 2 wff EXMID
2		vx	. . . . . 6 setvar 𝑥
3	2	cv 1352	. . . . 5 class 𝑥
4		c0 3423	. . . . . 6 class ∅
5	4	csn 3593	. . . . 5 class {∅}
6	3, 5	wss 3130	. . . 4 wff 𝑥 ⊆ {∅}
7	4, 3	wcel 2148	. . . . 5 wff ∅ ∈ 𝑥
8	7	wdc 834	. . . 4 wff DECID ∅ ∈ 𝑥
9	6, 8	wi 4	. . 3 wff (𝑥 ⊆ {∅} → DECID ∅ ∈ 𝑥)
10	9, 2	wal 1351	. 2 wff ∀𝑥(𝑥 ⊆ {∅} → DECID ∅ ∈ 𝑥)
11	1, 10	wb 105	1 wff (EXMID ↔ ∀𝑥(𝑥 ⊆ {∅} → DECID ∅ ∈ 𝑥))

This definition is referenced by:  exmidexmid  4197  exmid01  4199  exmidsssnc  4204  exmid0el  4205  exmidundif  4207  exmidundifim  4208  exmid1stab  4209  pw1dc0el  6911  exmidfodomrlemr  7201  exmidfodomrlemrALT  7202