Intuitionistic Logic Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  ILE Home  >  Th. List  >  df-exmid Unicode version

Definition df-exmid 4123
 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 4121 with exmidundif 4133. 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 4124 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 4050, in which case EXMID means that all propositions are decidable (see exmidexmid 4124 and notice that it relies on ax-sep 4050). If we instead work with ax-bdsep 13236, 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
StepHypRef Expression
1 wem 4122 . 2 EXMID
2 vx . . . . . 6
32cv 1331 . . . . 5
4 c0 3364 . . . . . 6
54csn 3528 . . . . 5
63, 5wss 3072 . . . 4
74, 3wcel 1481 . . . . 5
87wdc 820 . . . 4 DECID
96, 8wi 4 . . 3 DECID
109, 2wal 1330 . 2 DECID
111, 10wb 104 1 EXMID DECID
 Colors of variables: wff set class This definition is referenced by:  exmidexmid  4124  exmid01  4125  exmidsssnc  4130  exmid0el  4131  exmidundif  4133  exmidundifim  4134  exmidfodomrlemr  7071  exmidfodomrlemrALT  7072  exmid1stab  13351
 Copyright terms: Public domain W3C validator