What are first/second order variables in Metamath Zero?

[Bulhwi Cha]

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

[Mario Carneiro]

On Fri, Aug 29, 2025 at 10:26 AM 'Bulhwi Cha' via Metamath <meta...@googlegroups.com> 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.

[Bulhwi Cha]

There are still a few things that confuse me.

strict provable sort wff;
pure sort nat;

term qt1 {x: nat} (a b: nat x): wff;
axiom ax1 {x: nat} (a b: nat x): $ qt1 x a b $;

theorem thm1 {x: nat}: $ qt1 x x x $ = '(ax1);

term qt2 {x: nat} (a b: nat): wff;
axiom ax2 {x: nat} (a b: nat): $ qt2 x a b $;

theorem thm2 {x: nat}: $ qt2 x x x $ = '(ax2);
-- error: disjoint variable violation at ax2
-- (x, a) -> (x, x)
-- (x, b) -> (x, x)

Are the following statements about the declarations of qt2 and ax2 true?

(a) The variables a and b are second-order variables.
(b) The variables a and b need not be distinct.
(c) The variables x and a are distinct.
(d) The variables x and b are distinct.

[Mario Carneiro]

Yes. There is no actual notion of distinctness between two second order variables. The substitution for a cannot reference the variable substituted for x (which in thm2 is also x).