Thank you Dr Wheeler.. On Monday, June 5, 2023 at 11:05:28 PM UTC+8 David A. Wheeler wrote:
> > 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/b3b1c5ce-de4f-4cf6-90d3-133b73cd78fan%40googlegroups.com.
