| 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 2596, therefore we avoid that
ambiguous name.
Notation of [BellMachover] p. 460,
whose definition we show as mo3 2591.
For other possible definitions see moeu 2610
and mo4 2593.
Note that the definiens does not express "at-most-one" in the
empty
domain. Since the hypothesis relies on ax-6 1996,
this case is excluded
anyway. Nevertheless, it was suggested to begin with the definition of
uniqueness (eu6 2601) and then define the at-most-one quantifier
via
moeu 2610. Both eu6 2601 and moeu 2610
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 2565 would be derivable from propositional axioms
alone:
one could apply the definiens for ∃*𝑥𝜑 twice, using different
dummy variables 𝑦 and 𝑧, and then invoke bitr3i 280 to establish
their equivalence. This would jeopardize the independence of axioms, as
demonstrated in an analoguous situation involving df-ss 3921 to prove
ax-8 2144 (see in-ax8 36764).
Prefer dfmo 2567 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 2610, while this definition was then
proved as dfmo 2567). (Revised by BJ,
30-Sep-2022.) | 