On Fri, May 30, 2025 at 5:47 PM [email protected] <[email protected]> wrote:
> We have the assertion: copab $a class { < x , y > | ph } $.
>
> My question is how does one know that < x , y > refers to: cop $a class <
> A , B > $.
>
It doesn't! In fact, copab is just a composite syntax containing the tokens
"{", "<.", variable x, ",", variable y, "|", variable ph, "}" in that
order. It is connected to cop in two ways:
* As a visual aid, since this is often how people write ordered pair
abstractions (although it visually suggests that it is a special case of an
`{ A | ph }` form and that does not exist because the binding structure is
weird)
* Because it uses the exact same constant tokens as those used in cop, this
is a potential ambiguity in the grammar. It is actually not ambiguous,
exactly because `{ A | ph }` is not legal and `{ x | ph }` can only have a
variable on the left, which can't start with a `<.` token, but this is one
of the most difficult cases in the proof of unambiguity. See
https://us.metamath.org/downloads/grammar-ambiguity.txt for more on this;
copab is treated in the "type 3" section.
The detailed syntax breakdown looks like this, which should clarify the
atomic nature of copab: (note also that x and y have to be set variables
here, not classes, which is why the cv steps are missing)
wph ph
vx setvar x
vy setvar y
copab class { <. x , y >. | ph }
--
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 visit
https://groups.google.com/d/msgid/metamath/CAFXXJSt%2BsPWijMHzy-SM_9kQLvDrMQ%3DtnbT463-LJvUc1wR8JA%40mail.gmail.com.
