On Tue, Sep 2, 2025 at 5:52 AM 'Bulhwi Cha' via Metamath <
[email protected]> wrote:
> 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.
>
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).
--
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/CAFXXJSuB%3DQHoiOh5zEuVWFgFJqb312mAEtA87JGm2gtBFbQAAg%40mail.gmail.com.
