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.
--
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/DCI0CS6I3CV0.1INIBJ4CRAHRX%40semmalgil.com.
signature.asc
Description: PGP signature
