So, indeed, the "<" and ">" are just notational constants to syntactically
form the class expression being introduced.
In particular, consider the axiom df-opab $a |- { < x , y > | ph } = { z |
E x E y ( z = < x , y > /\ ph }.
The first "< x , y >" is just notational syntax, whereas the second "< x ,
y >" is a "true" ordered pair (justified by cop and df-op.
As an aside: the reason I am bringing this up is that I am trying to allow
a user to look up the "meaning" of a metamath symbol.
Thus "copab $a class { < x , y > | ph } $." has no "meaning", but only
provides the syntax. I don't have to explain the meaning of < x , y >.
But, df-opab $a |- { < x , y > | ph } = { z | E x E y ( z = < x , y > /\ ph
} gives the meaning/semantics of the syntactical expression { < x , y > |
ph }.
The user might not know the "meaning" of "< x , y >" on the right hand
side, so could request a lookup for its meaning (which is has by df-op).
On Friday, May 30, 2025 at 2:10:21 PM UTC-5 [email protected] wrote:
> 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/14cee126-8a08-4b27-91f9-08333e162fdan%40googlegroups.com.
