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 | ⊢ ( ∃ 𝑦 ∀ 𝑥 ( 𝜑 → 𝑥 = 𝑦 ) ↔ ∃ 𝑧 ∀ 𝑥 ( 𝜑 → 𝑥 = 𝑧 ) ) | |
| Assertion | df-mo | ⊢ ( ∃* 𝑥 𝜑 ↔ ∃ 𝑦 ∀ 𝑥 ( 𝜑 → 𝑥 = 𝑦 ) ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 0 | vx | ⊢ 𝑥 | |
| 1 | wph | ⊢ 𝜑 | |
| 2 | 1 0 | wmo | ⊢ ∃* 𝑥 𝜑 |
| 3 | vy | ⊢ 𝑦 | |
| 4 | 0 | cv | ⊢ 𝑥 |
| 5 | 3 | cv | ⊢ 𝑦 |
| 6 | 4 5 | wceq | ⊢ 𝑥 = 𝑦 |
| 7 | 1 6 | wi | ⊢ ( 𝜑 → 𝑥 = 𝑦 ) |
| 8 | 7 0 | wal | ⊢ ∀ 𝑥 ( 𝜑 → 𝑥 = 𝑦 ) |
| 9 | 8 3 | wex | ⊢ ∃ 𝑦 ∀ 𝑥 ( 𝜑 → 𝑥 = 𝑦 ) |
| 10 | 2 9 | wb | ⊢ ( ∃* 𝑥 𝜑 ↔ ∃ 𝑦 ∀ 𝑥 ( 𝜑 → 𝑥 = 𝑦 ) ) |