| Description: Define the at-most-one
quantifier. The expression ∃*𝑥𝜑 is read
"there exists at most one 𝑥 such that 𝜑". This is also
called
the "uniqueness quantifier" but that expression is also used
for the
unique existential quantifier df-eu 2568, therefore we avoid that
ambiguous name.
Notation of [BellMachover] p. 460,
whose definition we show as mo3 2563.
For other possible definitions see moeu 2582
and mo4 2565.
Note that the definiens does not express "at-most-one" in the
empty
domain. Since the hypothesis relies on ax-6 1969,
this case is excluded
anyway. Nevertheless, it was suggested to begin with the definition of
uniqueness (eu6 2573) and then define the at-most-one quantifier
via
moeu 2582. Both eu6 2573 and moeu 2582
remain valid in the empty domain.
The hypothesis asserts that the definition is independent of the
particular choice of the dummy variable 𝑦. Without this
hypothesis, mojust 2537 would be derivable from propositional axioms
alone:
one could apply the definiens for ∃*𝑥𝜑 twice, using different
dummy variables 𝑦 and 𝑧, and then invoke bitr3i 277 to establish
their equivalence. This would jeopardize the independence of axioms, as
demonstrated in an analoguous situation involving df-ss 3917 to prove
ax-8 2116 (see in-ax8 36397).
Prefer dfmo 2539 unless you can prove the hypothesis from
fewer axioms in
special cases. (Contributed by Wolf Lammen, 27-May-2019.) Make this
the definition (which used to be moeu 2582, while this definition was then
proved as dfmo 2539). (Revised by BJ,
30-Sep-2022.) | 