redefine df-ral and friends

[wlammen]

The current definition df-ral (∀𝑥 ∈ 𝐴 𝜑 ↔ ∀𝑥(𝑥 ∈ 𝐴 → 𝜑)), sloppily phrased as For all x in class A holds 𝜑, is perceived as problematic, when x and A are not disjoint. In this case the filtering is done by querying whether x belongs to A(x), itself an element of a collection of classes A varying with x. This is rarely needed, if at all, and the comments to theorems using df-ral show, that their authors often are unaware of this exception.

I propose to change the definition to (∀𝑥 ∈ 𝐴 𝜑 ↔ (Ⅎ𝑥𝐴 ∧ ∀𝑥(𝑥 ∈ 𝐴 → 𝜑))). From this definition a theorem (∀𝑥 ∈ 𝐴 𝜑 ↔ ∀𝑥(𝑥 ∈ 𝐴 → 𝜑)) with disjoint x, A follows using only axioms up to ax-5.

The change is too massive to be carried out in a single pull request. So for some time we need both definitions (that extends to other quantifiers like df-rex, df-rmo, df-reu) in parallel. Any comments, suggestions, objections? See also #3192, where this proposal was discussed.

[digama0]

I have an alternative proposal:

( A. x e. A ph <-> A. y ( y e. A -> [ y / x ] ph ) )

(You are also welcome to rephrase this to something provably equivalent; I don't keep up with subsystems of the MM axioms.)

I think that your definition will have more side effects than mine, because yours has an extra conjunct and isn't just a forall anymore. You can't easily generalize that to other binders like df-rex (would it also be a conjunction, or would it be a disjunction now?) or df-rab (it's not even a proposition in this case) or df-sum (at this point there really is no place to put a side condition).

[wlammen]

Nice trick! Now x may appear in A without any effect. One should still assume x y, ph y, A y disjoint.

I'd replace [ y / x ] ph with A x ( x = y -> ph ) to be independent of the flavour of df-sb.

[wlammen]

From https://us.metamath.org/mpeuni/df-wl-ral.html on you will find a possible alternative definition of restricted quantifiers, as discussed above. One has to say, though, that it is inconsistent with definitions like this here https://encyclopediaofmath.org/wiki/Restricted_quantifier , which is more supportive of the old way. Again, your opinions, please.

[digama0]

Note that in the linked definition, R is a predicate (a wff) and not a class. I agree with using R(x) in the predicate case, and it is recoverable in our setting by using A. x e. { x | R(x) } P(x) if desired.

[tirix]

I think it would be interesting to do the change, but we should clearly state in the comments what the textbook definition is, where to find it, and redirect first reader there.
Then we can explain the technicalities and why the set.mm definition differs.

[wlammen]

If your restricting predicate is strictly limited to 𝑥 ∈ 𝐴, then the new definition is perhaps a bit more to the point, since it semantically sees 𝑥 ∈ 𝐴 as an idiom restricting elements to those of a given class. If you later want to extend 𝑥 ∈ 𝐴 to general predicates, as is outlined in encyclopedia of math, then you are perhaps better off sticking to the current interpretation.

Nothing limits us to later introduce another restricted quantifier on top with a general predicate as the filtering expression, should this turn out to be useful. In the past years there was little to no pressure in this direction, though. If you don't object, I will start soon introducing the new definitions to main, and then bit by bit rewrite applications of df-ral and friends to the new definition, in the end replacing the old ones. This will sometimes make modifications in mathboxes, usually adding distinct variable provisos, necessary.

[tirix]

I will start soon introducing the new definitions to main, and then bit by bit rewrite applications of df-ral and friends to the new definition, in the end replacing the old ones. This will sometimes make modifications in mathboxes, usually adding distinct variable provisos, necessary.

Could we discuss this thoroughly first? Maybe pass it through the mailing list and gather more opinions?
Also, for example, does this mean that two versions of wral will coexist for a while?
If so what will be our policy during that period?

[wlammen]

My hope was this github issue would be the right place to introduce new ideas. But of course, there is no haste, I can explain it somewhere else. Is the mailing list this Google group https://groups.google.com/g/metamath? And to answer one of your questions - if it is up to me there will be a transition period.

[david-a-wheeler]

Usually github issues are the right place for new ideas, but in the case of significant/far-reaching changes, I think it's wise to create a github issue (to track it) and then post on the mailing list. Far more people will see mailing list posts, and thus you'll get more feedback, as well as giving people a heads-up (and a warning).

[david-a-wheeler]

Normally when we use a definition "different from usual" we use the new definition, and then prove that the "old" definition is equivalent (or is at least equivalent in certain cases).

[wlammen]

Normally when we use a definition "different from usual" we use the new definition, and then prove that the "old" definition is equivalent (or is at least equivalent in certain cases).

This is already done in https://us.metamath.org/mpeuni/df-wl-ral.html and later theorems. The gist is, that whenever 𝑥 is not free in 𝐴 in the expression 𝑥 ∈ 𝐴, old and new definitions coincide, not taking axiom usage into account. The conversion between the two definitions often needs ax-10, ax-12, and ax-11, so imitating the old results may see an increase in the usage of these axioms.

[wlammen]

I am not really supporting this issue any more. It seems the suggested new definition drags in ax-11 at a very early stage, and this is something I don't like. So leave the definition of https://us.metamath.org/mpeuni/df-ral.html as it is. For a reason I don't understand, dv restrictions are not welcome in definitions. To get more into the desired direction, I suggest to mark this definition as not to be used any more, except by two theorems (1) dfralv adding a dv condition on x and A (2) and dfralf adding Ⅎ𝑥𝐴 to the definition as the only users of this definition. This would limit applications of df-ral to the clear case with the meaning "for all elements x from a set A holds ... .