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 4034 with exmidundif 4043. 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 4037 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 3963, in which case EXMID means that all propositions are
decidable (see exmidexmid 4037 and notice that it relies on ax-sep 3963). If
we instead work with ax-bdsep 12048, EXMID as defined here means that
all bounded propositions are decidable.
(Contributed by Mario Carneiro and Jim Kingdon,
18-Jun-2022.) |