On Sat, Mar 20, 2021 at 9:58 PM Benoit <[email protected]> wrote:
> Indeed, for general databases, one can define any type of variables so
> there is no notion of "setvar variable". Maybe, in Mario's Metamath Zero,
> the restriction would be to have no DV conditions among non-pure sorts. (?)
>
Indeed, in MM0 there is no analogue of $d ph ps $. at all, the syntax
itself makes such a supposition impossible to write. Variables come in two
flavors, bound variables (aka names or first order variables) and regular
variables (aka metavariables or second order variables). Bound variables
are like "setvar" in set.mm, and they are always disjoint (so $d x y $. is
implied for every pair of distinct variables), and regular variables
declare which bound variables they can depend on, and by omission which
bound variables they must be disjoint from (which defines the $d x ph $.
conditions). Regular variables cannot depend on other regular variables.
(The sort modifiers actually don't matter here; this has to do with the
binders like {x: set} vs (ph: wff x).)
Mario
--
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/CAFXXJSvfZd2wvhXJt6h%3DM-b%2B0DR-0ehyeAFJPu5ZZaJU%2BDS_tA%40mail.gmail.com.
