Use of parentheses for new definitions

[Ender Ting]

I'm considering to generalize my definition UpWord S (for strictly increasing words on alphabet S) to AdjRelWord S R (which would have R instead of hard-coded <, and so could be used on other partial orders).

I do not quite get if I need to put parentheses like ( AdjRelWord S R ); the decimal constructor ~cdc has none, the sum syntax ~csu has nothing between its two classes too, while ~cpred wraps its arguments in parentheses. In theory, the classes should already be unambiguously decodable as a prefix code, but I am not certain.

[Matthew House]

metamath-knife -g is pretty helpful for testing the grammar for ambiguities. In this case, it has no complaints if I add $c AdjRelWord $.  cadjrelword $a class AdjRelWord S R $. to set.mm, so it's presumably fine. And as you mention, its syntax is analogous to cdc in any case.

(Though conventionally, when I see "class functions" in main set.mm taking multiple arguments, they're written with full ( , ) particles, e.g., if ( ph , A , B ); Pred ( R , A , X ); frecs ( R , A , F ); wrecs ( R , A , F ); rec ( F , I ); seqom ( F , I ); sup ( A , B , R ); inf ( A , B , R ); and OrdIso ( R , A ). Odd ones include seq M ( .+ , F ) and seq_s M ( .+ , F ).)

On Thu, Jan 15, 2026 at 7:43 AM Ender Ting <freelance...@gmail.com> wrote:

I'm considering to generalize my definition UpWord S (for strictly increasing words on alphabet S) to AdjRelWord S R (which would have R instead of hard-coded <, and so could be used on other partial orders).

I do not quite get if I need to put parentheses like ( AdjRelWord S R ); the decimal constructor ~cdc has none, the sum syntax ~csu has nothing between its two classes too, while ~cpred wraps its arguments in parentheses. In theory, the classes should already be unambiguously decodable as a prefix code, but I am not certain.

--
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 metamath+u...@googlegroups.com.
To view this discussion visit https://groups.google.com/d/msgid/metamath/59a18a7f-a665-402e-82ff-8d727bd67d04n%40googlegroups.com.

[Thierry Arnoux]

In the mean time I have proposed df-chn in my Mathbox, which I believe is exactly what you need: a chain in the sense of order theory.

If there was to be a rule, I'd say parentheses are used for classes, and left away for wffs.

For example: `( A + B )` (df-ov) is a class and has parentheses, while `A < B` is a (df-br) is a wff and does not.

Same for example for df-fv, df-dif, df-un, df-in (classes, parentheses), and df-clel, df-ne, df-ss, df-po, (wff, no parentheses), etc.

BR,
_
Thierry

To view this discussion visit https://groups.google.com/d/msgid/metamath/CADBQv9b0uCHKnYPxRDDURFtXi2sAqvPfA8bti5AsxFAJHG6U7Q%40mail.gmail.com.

[David A. Wheeler]

> On Jan 15, 2026, at 12:15 PM, 'Thierry Arnoux' via Metamath <meta...@googlegroups.com> wrote:
>
> In the mean time I have proposed df-chn in my Mathbox, which I believe is exactly what you need: a chain in the sense of order theory.
>
>
> If there was to be a rule, I'd say parentheses are used for classes, and left away for wffs.
> For example: `( A + B )` (df-ov) is a class and has parentheses, while `A < B` is a (df-br) is a wff and does not.
> Same for example for df-fv, df-dif, df-un, df-in (classes, parentheses), and df-clel, df-ne, df-ss, df-po, (wff, no parentheses), etc.

The "quick version" is that an infix binary relation (which compares 2 classes and produces a wff) is not surrounded by parentheses per df-br; otherwise it is.

I've tried to get the set.mm/iset.mm conventions documented in "conventions" and friends, e.g.:
https://us.metamath.org/mpeuni/conventions.html

Here's what that says:

> Infix and parentheses. When a function that takes two classes and produces a class is applied as part of an infix expression, the expression is always surrounded by parentheses (see df-ov 7352). For example, the + in (2 + 2); see 2p2e4 12258. Function application is itself an example of this. Similarly, predicate expressions in infix form that take two or three wffs and produce a wff are also always surrounded by parentheses, such as (𝜑 → 𝜓), (𝜑 ∨ 𝜓), (𝜑 ∧ 𝜓), and (𝜑 ↔ 𝜓) (see wi 4, df-or 848, df-an 396, and df-bi 207 respectively). In contrast, a binary relation (which compares two _classes_ and produces a _wff_) applied in an infix expression is _not_ surrounded by parentheses. This includes set membership 𝐴 ∈ 𝐵 (see wel 2110), equality 𝐴 = 𝐵 (see df-cleq 2721), subset 𝐴 ⊆ 𝐵 (see df-ss 3920), and less-than 𝐴 < 𝐵 (see df-lt 11022). For the general definition of a binary relation in the form 𝐴𝑅𝐵, see df-br 5093. For example, 0 < 1 (see 0lt1 11642) does not use parentheses.

Of course, if there's an error or important clarification needed, please propose it!

--- David A. Wheeler

[Ender Ting]

To Thierry: it [~df-chn] is what I need, indeed! Amazing coincidence.

I'd then

• move your chain definition to main, somewhere between "5.7 Words over a set" and "17.3.1 Walks" (in "GRAPH THEORY" part)
  so probably to a new section "9.7 Chains" (in "BASIC ORDER THEORY" part)
  Note: there is something in your htmldef that makes it render "( < Chain𝐴)" with a missing space ;
• move your chain theorems to main too;
• remove ~cupword, ~df-upword which are my definitions for the same;
• port those of my 'UpWord' (chain) theorems which are not obsolete, to main;
• add a few equality and subset theorems to that same section in main.

Is that a valid way to move forward?

Additionally, when proving subsequent theorems, would I place them in my mathbox or in that section?

To Matthew and to David: sounds reasonable! I'll probably stick to surrounding newly defined classes with parens if they need any arguments.

Best wishes,

Ender

четверг, 15 января 2026 г. в 20:15:36 UTC+3, Thierry Arnoux: