Document unbound variables are basically universal

[david-a-wheeler]

Document an issue discussed in the Metamath mailing list, subject "Re: [Metamath] Question about a specific problem probably unrelated with metamath".

[david-a-wheeler]

This attempts to document a point from the mailing list. Improvements / corrections welcome.

[sctfn]

Could you please add something about how this does not apply to class variables? Ie, 0 < K is usually safe to postulate.

[metakunt]

But won't you get a problem discharging the hypothesis if you aren't prefixing it with ph?
As far as I have understood and checked it with all my experience I have collected so far, not prefixing theorems with ph usually causes so much pain. All statements except definitions are (at the very least for me) in deduction form.

#3908

Actually it might even be the first thing I have learned.

[wlammen]

Ie, 0 < K is usually safe to postulate.

Its impossible to quantify classes, and bind them that way. So far it is clear. But when you introduce a class with A e. X, which renders it automatically a set, what is the difference between a e. X and A e. X then?

[sctfn]

The difference is that there is no inference rule analogous to vtoclg for classes. That is, you can't go from |- A e. X => |- B e. X in the general case.

[avekens]

In principle, I think it is a good idea to document this interesting and important observation at a central place.
But is Conventions, section "Distinctness or freeness" the right place?

Furthermore, this description must be worked out a lot, because in this way, and without additional context, it confuses more than it is helpful.

[jkingdon]

I'm undecided about this. If we do say something, I'd probably refer to ax-gen . What to say about classes is, as usual, one of the hardest parts.

I might ultimately come down on the side of "don't try to teach predicate logic in metamath documentation" but of course some of the metamath specific parts warrant a mention so I'm a bit unsure.

[sctfn]

IMO, it's a subtle point of logic that should probably be called out. I agree that ax-gen is the right place for this. I think it's okay to mention class variables there - we aren't trying to keep them secret.

[benjub]

Is there a problem this MR is trying to solve? Yes, the axiom ax-gen is indeed part of set.mm, and I'm not sure we want to repeat it with multiple variations and at various places, including in our "conventions". There are also explanations at https://us.metamath.org/mpeuni/mmdeduction.html#standard and https://us.metamath.org/mpeuni/dtrucor.html

Yes, it is also true that classes cannot be quantified over in set.mm, but do we want to also write that in our "conventions"?

As @jkingdon writes, I also prefer that we "don't try to teach predicate logic in metamath documentation".

[metakunt]

Also a point regarding teaching metamath. I don't particularly have a pro or con regarding where things are to be taught, but from my experience few months ago when I've started it wasn't a good teaching experience.

Generally you want some guidance somewhere accessible for new users to start. The fact that I couldn't even get the tooling to run was just plain abyssmal.

[langgerard]

I think that a comment in ax-gen is a good place for this explanation. This explanation should emphasize that, in the case of the ZFC set theory, the syntax only allows the (universal or existential) quantification over setvar variables, but not over class variables, but that, in the case of NBG or MK set theory, such quantification over class variables is allowed.

[sctfn]

That's still not true in the way we develop our "virtual" classes, though. In NBG, we'd still have the distinction between (now) classvars and the compound expression classes. We'd quantify over classvars and instantiate them with virtual classes. The big difference would be that |- E. y x e. y would no longer be a theorem, so we would need to say A e. U. _V instead of A e. _V (unless we redefined _V)

[digama0]

Right, the key difference is not "set" vs "class" but rather the "var" part of "setvar" (also the reason why we renamed this sort to begin with). The lowercase variables are stand-ins for variables, they are something that can legally appear in the first position of A. x ph. This has nothing to do with whether they are sets or not - 0 is a set but A. 0 ph is nonsense.

If we had a "classvar" sort then they too would be subject to ax-gen and substitution in hypotheses.