> On Monday, June 5, 2023 at 9:18:51 AM UTC+8 [email protected] 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 <[email protected]> > 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 -- 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 on the web visit https://groups.google.com/d/msgid/metamath/F49861B9-4EFE-47B5-9DFB-89F4D2D26A48%40dwheeler.com.
