Description: Define Russell's
definition description binder, which can be read as
"the unique x such that φ," where φ ordinarily contains
x as a free
variable. Our definition is meaningful only when there
is exactly one x such that φ is true (see iotaval 4821);
otherwise, it evaluates to the empty set (see iotanul 4825). Russell used
the inverted iota symbol ℩ to represent
the binder.
Sometimes proofs need to expand an iota-based definition. That is,
given "X = the x for which ... x ... x ..." holds, the proof
needs to
get to "... X ... X ...". A general strategy to do this is
to use
iotacl 4833 (for unbounded iota). This can be easier
than applying a
version that applies an explicit substitution, because substituting an
iota into its own property always has a bound variable clash which must
be first renamed or else guarded with NF.
(Contributed by Andrew Salmon, 30-Jun-2011.) |