>
> (Actually df-v is an exception; it should probably read { x | T. } and I
> guess the use of x = x is a historical accident?)
>
This has been proposed in
https://groups.google.com/d/msg/metamath/V3jmbWUd_mM/RAk2DEA3FQAJ, with
explanations that I still stand by. With the new definition df-tru, I
think there is even less of a reason to keep "x = x" (which by the way
evaluates to false in one of the two semantics on the empty domain --
granted, in this case, the universal class is the empty class anyway!).
To answer one of Norm's questions: I don't think the conditional operator
on definitions would benefit many theorems in the current version of
set.mm, I haven't really checked. My main motivation is actually to
improve consistency, to be able to say, for instance: "if_" is to "if" what
"F/_" is to "F/" and what "[_ / ]_" is to "[. / ].", and to emphasize that
classes are defined as extensions of predicates, which has concrete
consequences on proof structures.
As for the definitions, there are indeed two groups: dfif1--4 and dfif5--7
(dfif1 being the current ~df-bj-if), and the easiest to understand are the
first of each group (dfif1 and dfif5). I did put dfif1 as the main
definition because the "if... then" is akin to the implication used in
dfif1. Norm and Mario prefer dfif5, because in intuitionistic logic, it
has the advantage of implying decidability of phi (obvious).
Benoît
--
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/7a006ac0-7c29-43e4-8054-81dd623fa3e8%40googlegroups.com.
