Description: Alternate version of
Russell's definition of a description binder, which
can be read as "the unique 𝑥 such that 𝜑", where 𝜑
ordinarily contains 𝑥 as a free variable. Our definition
is
meaningful only when there is exactly one 𝑥 such that 𝜑 is true
(see aiotaval 44287); otherwise, it is not a set (see aiotaexb 44281), or even
more concrete, it is the universe V (see aiotavb 44282). Since this
is an alternative for df-iota 6355, we call this symbol ℩'
alternate iota in the following.
The advantage of this definition is the clear distinguishability of the
defined and undefined cases: the alternate iota over a wff is defined
iff it is a set (see aiotaexb 44281). With the original definition,
there
is no corresponding theorem (∃!𝑥𝜑 ↔ (℩𝑥𝜑) ≠ ∅),
because ∅ can be a valid unique set
satisfying a wff (see, for
example, iota0def 44232). Only the right to left implication would
hold,
see (negated) iotanul 6375. For defined cases, however, both
definitions
df-iota 6355 and df-aiota 44277 are equivalent, see reuaiotaiota 44280. (Proposed
by BJ, 13-Aug-2022.) (Contributed by AV,
24-Aug-2022.) |