In a definition in set.mm, what is the difference between the equals sign and the bidirectional?

[Humanities Clinic]

In a definition in set.mm, what is the difference between the equals sign and the bidirectional?

(Apologies, if this is a basic question..)

[Discher, Samiro]

'=' stands for class equality: https://us.metamath.org/mpeuni/wceq.html (e.g. equality of numbers)

'↔' stands for the logical biconditional: https://us.metamath.org/mpeuni/wb.html (i.e. equality of truth values)

---

Von: meta...@googlegroups.com <meta...@googlegroups.com> im Auftrag von Humanities Clinic <humaniti...@gmail.com>
Gesendet: Sonntag, 4. Juni 2023 18:38:45
An: Metamath
Betreff: [Metamath] In a definition in set.mm, what is the difference between the equals sign and the bidirectional?

 

In a definition in set.mm, what is the difference between the equals sign and the bidirectional?

(Apologies, if this is a basic question..)

--
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 on the web visit https://groups.google.com/d/msgid/metamath/0ad5b342-5254-49d7-9fca-65b71a0101b4n%40googlegroups.com.

[Humanities Clinic]

Erm yes I know that.. But it's a little confusing when one sign should/can be used instead of the other.. Can someone clarify?

[David A. Wheeler]

> On Monday, June 5, 2023 at 9:18:51 AM UTC+8 samiro.d...@rwth-aachen.de wrote:
> '=' stands for class equality: https://us.metamath.org/mpeuni/wceq.html (e.g. equality of numbers)
> '↔' stands for the logical biconditional: https://us.metamath.org/mpeuni/wb.html (i.e. equality of truth values)

> On Jun 5, 2023, at 1:26 AM, Humanities Clinic <humaniti...@gmail.com> wrote:
>
> Erm yes I know that.. But it's a little confusing when one sign should/can be used instead of the other.. Can someone clarify?

Sure! If the left & right sides are classes (including sets), use "=".
If the left & right sides are wffs (that is, values that are true or false), use "<->".

So you'd say A = B and ( ph <-> ps ), not the other way around.
The constant true is represented as "T." and the constant false is "F.",
so you'd compare to them using "<->". Here's a true statement:
( T. <-> A. x x = x )

While we're mentioning it, set.mm is picky about parentheses. Here are the conventions:

* 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. For example, the use of "+" in <tt>( 2 + 2 )</tt>.
* Predicate expressions in infix form that take two or three wffs
(a true or false value) and produce a wff are also always
surrounded by parentheses, such as <tt>( ph -> ps )</tt>.
* 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, for example, "1 e. RR" (1 is a member
of the set of real numbers) has no parentheses. This also includes "=".

You can find other set.mm conventions in:
* set.mm general conventions - https://us.metamath.org/mpeuni/conventions.html
* set.mm label naming conventions - https://us.metamath.org/mpeuni/conventions-labels.html

--- David A. Wheeler

[Humanities Clinic]

Thank you Dr Wheeler..

[Jim Kingdon]

Oh cool. I was aware that equals and subset and df-br don't take parentheses but I hadn't quite thought of them as all examples of a "class thing class" (and produce a formula) pattern. I see we have this nicely documented in the "Infix and parentheses" section of conventions.html

[Thierry Arnoux]

As you know, there are 3 typecodes in set.mm.

• Classes represent generalized sets. In the definition of constant classes, like for example Grp, the equal symbol is used: Grp = { w e. _V | ... }
• Wff are formulas, which represent statements. In the definition of constant statements, like for example the "true" constant, the equivalence bidirectional symbol is used: T. <-> ( A. x ... ) 
  
• Setvar do not appear in definitions, but share many properties with classes, so an equal symbol would be used for them.
  

The fact that only classes can be expressed as equal (and not, say, wffs) is expressed in `~wceq`:

cA.wceq $f class A $.

cB.wceq $f class B $.

$( Extend wff definition to include class equality. $)

wceq $a wff A = B $.

Here A and B are defined as classes, only classes can be used.

Same for the equivalence bidirectional, only wff are allowed:

wph $f wff ph $.

wps $f wff ps $. $( Extend wff definition to include the biconditional connective. $)

wb $a wff ( ph <-> ps ) $.

To view this discussion on the web visit https://groups.google.com/d/msgid/metamath/bf8cce0f-3b90-40c7-ae72-c35a61424c0an%40googlegroups.com.