Re: [Metamath] Use of parentheses for new definitions

['David A. Wheeler' via Metamath]

> On Jan 15, 2026, at 12:15 PM, 'Thierry Arnoux' via Metamath 
> <metamath@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

-- 
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+unsubscr...@googlegroups.com.
To view this discussion visit 
https://groups.google.com/d/msgid/metamath/2B920EBD-7087-477C-A626-DD49880B750B%40dwheeler.com.