| 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 2570, therefore we avoid that
ambiguous name.
Notation of [BellMachover] p. 460,
whose definition we show as mo3 2565.
For other possible definitions see moeu 2584
and mo4 2567.
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 2575) and then define the at-most-one quantifier
via
moeu 2584. Both eu6 2575 and moeu 2584
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 2539 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 3919 to prove
ax-8 2116 (see in-ax8 36420).
Prefer dfmo 2541 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 2584, while this definition was then
proved as dfmo 2541). (Revised by BJ,
30-Sep-2022.) | 