On Fri, Aug 29, 2025 at 10:26 AM 'Bulhwi Cha' via Metamath <
[email protected]> wrote:
> Consider the following MM0 example:
>
> strict provable sort wff;
> pure sort nat;
>
> term foo {x: nat} (a b: nat x): wff;
>
> In the term declaration foo, are these statements true?
>
> (a) The variable x is a first order variable.
> (b) The variables a and b are second order variables.
>
Yes.
> Since there's the pure modifier in the sort declaration of nat,
> shouldn't nat contain only names, that is, first order variables?
>
On page 33 (Section 1.5.1 Sort modifiers) of the Metamath Zero paper[0]:
> > The pure modifier asserts that the sort has no expression construc-
> > tors (terms or defs). This is useful for name-only sorts like var.
>
Yes in the modeling sense; there are no terms of a pure sort other than
direct references to a variable. But the distinction between first- and
second-order variables remains syntactically. This is used mainly for
tracking binding structure.
--
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 visit
https://groups.google.com/d/msgid/metamath/CAFXXJSuw9NLK60dt5eEcvtXUM9x_%2BQXhOAmuke49ZKCLPu%3D7Zw%40mail.gmail.com.
