Hi Mario,
you are absolutely right, df-opap is really very strange.
But I wonder if it is correct at all (also with your suggested
modification). Shouldn't also the first variable be different from the one
used on the right hand side, e.g.
df-opab $a |- { <. x , y >. | ph } = { z | E. a E. b ( ( x = a /\ y = b /\
z = <. a , b >. ) /\ [ a / x ] [ b / y ] ph ) }
By this, the free variables x,y of the left hand side are not mixed up with
the bound variables on the right hand side.
On Wednesday, June 19, 2019 at 10:39:27 AM UTC+2, Mario Carneiro wrote:
>
> 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/f08daa8c-883a-454e-8f25-ea28716c7096%40googlegroups.com.
