As you know, there are 3 typecodes in set.mm. *
*
* *C**lasses *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 ) $.
On 05/06/2023 07:26, Humanities Clinic 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?
On Monday, June 5, 2023 at 9:18:51 AM UTC+8 [email protected]
wrote:
'=' stands forclass 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:* [email protected] <[email protected]> im
Auftrag von Humanities Clinic <[email protected]>
*Gesendet:* Sonntag, 4. Juni 2023 18:38:45
*An:* Metamath
*Betreff:* [Metamath] In a definition in set.mm <http://set.mm>,
what is the difference between the equals sign and the bidirectional?
In a definition in set.mm <http://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 [email protected].
To view this discussion on the web visit
https://groups.google.com/d/msgid/metamath/0ad5b342-5254-49d7-9fca-65b71a0101b4n%40googlegroups.com
<https://groups.google.com/d/msgid/metamath/0ad5b342-5254-49d7-9fca-65b71a0101b4n%40googlegroups.com?utm_medium=email&utm_source=footer>.
--
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/bf8cce0f-3b90-40c7-ae72-c35a61424c0an%40googlegroups.com
<https://groups.google.com/d/msgid/metamath/bf8cce0f-3b90-40c7-ae72-c35a61424c0an%40googlegroups.com?utm_medium=email&utm_source=footer>.
--
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/d0805415-64a6-fa05-470f-d8d40ed037de%40gmx.net.
