Definition df-mo

Description: Define the at-most-one quantifier. The expression E* x ph is read "there exists at most one x such that ph ". This is also called the "uniqueness quantifier" but that expression is also used for the unique existential quantifier df-eu , therefore we avoid that ambiguous name.

Notation of BellMachover p. 460, whose definition we show as mo3 . For other possible definitions see moeu and mo4 .

Note that the definiens does not express "at-most-one" in the empty domain. Since the hypothesis relies on ax-6 , this case is excluded anyway. Nevertheless, it was suggested to begin with the definition of uniqueness ( eu6 ) and then define the at-most-one quantifier via moeu . Both eu6 and moeu remain valid in the empty domain.

The hypothesis asserts that the definition is independent of the particular choice of the dummy variable y . Without this hypothesis, mojust would be derivable from propositional axioms alone: one could apply the definiens for E* x ph twice, using different dummy variables y and z , and then invoke bitr3i to establish their equivalence. This would jeopardize the independence of axioms, as demonstrated in an analoguous situation involving df-ss to prove ax-8 (see in-ax8 ).

Prefer dfmo 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 , while this definition was then proved as dfmo ). (Revised by BJ, 30-Sep-2022)

	Ref	Expression
Hypothesis	mojust.1	$$⊢\exists y\forall x\left(\phi \to x=y\right)\leftrightarrow \exists z\forall x\left(\phi \to x=z\right)$$
Assertion	df-mo	$$⊢{\exists }^{*}x\phi \leftrightarrow \exists y\forall x\left(\phi \to x=y\right)$$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		vx	$$setvarx$$
1		wph	$$wff\phi$$
2	1 0	wmo	$$wff{\exists }^{*}x\phi$$
3		vy	$$setvary$$
4	0	cv	$$setvarx$$
5	3	cv	$$setvary$$
6	4 5	wceq	$$wffx=y$$
7	1 6	wi	$$wff\left(\phi \to x=y\right)$$
8	7 0	wal	$$wff\forall x\left(\phi \to x=y\right)$$
9	8 3	wex	$$wff\exists y\forall x\left(\phi \to x=y\right)$$
10	2 9	wb	$$wff\left({\exists }^{*}x\phi \leftrightarrow \exists y\forall x\left(\phi \to x=y\right)\right)$$