I ran into another bundling issue, this time with bundled terms. Luckily
this doesn't occur very often because the only term constructors that can
have a bundling violation are df-opab, df-mpt2 and df-oprab (which each
take two or more set arguments), but I have run into a bad axiom in
df-opab. Ignoring bundling, it is pretty clear that we want copab to have
the type (set -> set -> wff) -> class, that is, it takes a binary predicate
and returns a class. So I can define
copab (\x y. ph x y) := { z | E. x E. y (z = <x, y> /\ ph x y) }
(using a bit of HOL syntax to make the lambda obvious). The problem is that
if we let x and y be the same, and ph is a variable of only one argument,
then we get the following:
copab (\x x. ph x) = { z | E. x E. x (z = <x, x> /\ ph x) }
or after bound variable renaming:
copab (\x x'. ph x') = { z | E. x E. x' (z = <x', x'> /\ ph x') }
But these two are not the same; if I unfold the LHS using the original
definition I get
{ z | E. x E. x' (z = <x, x'> /\ ph x') } = { z | E. x E. x' (z = <x', x'>
/\ ph x') }
Notice that the distinctified version of copab always ranges over all pairs
(and ignores the first argument), while the degenerate version only ranges
over diagonal pairs.
I'm torn on the resolution. On the one hand, using { <. x , x >. | ph } to
mean a subset of _I matches the standard usage of the set comprehension
(which allows arbitrary expressions on the left and right), but on the
other hand it is binding x twice and I think that not being able to
translate { <. x , x >. | ph x } as copab (\x x. ph x) is a potential big
problem. It is possible to solve this in a similar fashion as with bundled
theorems, namely, to have a bundled term constructor opab_b : (set -> wff)
-> class defined by
opab_b (\x. ph x) := { z | E. x E. x' (z = <x', x'> /\ ph x') }
but I would prefer to fix opab itself in set.mm so that the second variable
shadows the first. One definition that achieves this is:
df-opab $a |- { <. x , y >. | ph } = { z | E. x E. w ( z = <. x , w >. /\ [
w / y ] ph ) }
Of course, the very first theorem would be to eliminate w and return to the
original definition (but with a $d x y). This change would break dfid3, but
I think this theorem is only a curiosity; I think bundled double binders
should strongly be avoided because of this semantic ambiguity (aka they
don't mean what you think they mean).
Mario
--
You received this message because you are subscribed to the Google Groups
"Metamath" group.
To unsubscribe from this group and stop receiving emails from it, send an email
to [email protected].
To view this discussion on the web visit
https://groups.google.com/d/msgid/metamath/CAFXXJSumBJiNvBsWOCAzazWan9VA1%2B3bPx6v%2BhxmtsPVjYxBzQ%40mail.gmail.com.
