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.
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.
[0] https://digama0.github.io/mm0/thesis.pdf
--
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/DCEROGJJFCS0.268EFL3ONS4SP%40semmalgil.com.
signature.asc
Description: PGP signature
