Explain why $d is used on its first use

[david-a-wheeler]

Explain why $d is used when $d is first used.
This text is tweaked from an email by Mario Carneiro on 2024-01-01 titled "Re: [Metamath] Results about ax-13 usage".

I thought it was a great point and that the information belonged somewhere in set.mm itself.

[david-a-wheeler]

@digama0 - I tweaked some nice text you wrote for inclusion into set.mm. This okay?

[avekens]

I think the comment for the definition is not a good place for such a description. Maybe it can be moved to the section header (as section comment).

Furthermore, the text is very difficult to understand (without more context/background information), especially:

   would lead to situations where even after the variable is done being
   used you still can't discharge the distinctor.  This would mean its
   logical equivalent would permanently stick around.  

What does " variable is done being used", "discharge the distinctor" and "logical equivalent" mean?

[benjub]

I think the comment for the definition is not a good place for such a description. Maybe it can be moved to the section header (as section comment).

Furthermore, the text is very difficult to understand (without more context/background information), especially:

   would lead to situations where even after the variable is done being
   used you still can't discharge the distinctor.  This would mean its
   logical equivalent would permanently stick around.  

What does " variable is done being used", "discharge the distinctor" and "logical equivalent" mean?

Actually, I would have a bit more than one comment per sentence in this PR. The proposed text is either superfluous (if you already understand DV conditions), or confusing (if you don't know DV conditions yet, then you'll be even more at a loss after reading that).

DV conditions are already explained in https://us.metamath.org/mpeuni/mmset.html#distinct or Appendix C.2 of the Metamath book, or Subsection 2.1 of Mario's article "Models for Metamath". If need be, a link can be added to that first URL.

[benjub]

Suggested change

	This is our first use of a disjoint variable restriction aka distinct
	variables ($d in the Metamath language). It would be possible to
	express our axioms without $d but there are good reasons we do it this
	way. The "obvious" way of truthfully expressing this axiom (and other
	similar axioms) without distinct variable constraints ($d statements)
	would lead to situations where even after the variable is done being
	used you still can't discharge the distinctor. This would mean its
	logical equivalent would permanently stick around. Effectively all
	proofs would end up saying "provided there are at least N variables in
	the metalogic, the following theorem holds" because you actually can't
	prove anything about whether variables exist in this setting. This
	admits models where e.g. the object logic only has three variables v0 v1
	v2 and so you can't write any expression containing four or more forall
	or exists quantifiers without being degenerate in some way, so the
	undischargeable assumptions that pile up are saying that the object
	logic is at least nondegenerate enough to perform the proof in question.
	The $d provisos provide a simple mechanism to eliminate the problem in
	general.
	For an explanation of disjoint variable conditions, see
	~ https://us.metamath.org/mpeuni/mmset.html#distinct .

[david-a-wheeler]

Linking to the explanation in mmset.html is fine, and Appendix C.2 of the Metamath book obviously does talk about $d. However, while they both explain "what they do", I think they don't adequately explain "why they're used at all". My goal is to more clearly explain why this approach is taken. Putting it in mmset.html's #distinct instead is fine... but I think it should go somewhere. I could tweak this proposal to move that kind of text into mmset.html#distinct and see how that works :-).

[benjub]

Linking to the explanation in mmset.html is fine, and Appendix C.2 of the Metamath book obviously does talk about $d. However, while they both explain "what they do", I think they don't adequately explain "why they're used at all". My goal is to more clearly explain why this approach is taken. Putting it in mmset.html's #distinct instead is fine... but I think it should go somewhere. I could tweak this proposal to move that kind of text into mmset.html#distinct and see how that works :-).

I think you made a good move in opening this PR, and in wanting to give more info to the reader at the place in set.mm where DVs are first used. My criticism was only about the content of that piece of text, and nothing/no-one else. So: yes, let's put the link to mmset.html#distinct now. Then, we can add something there about why set.mm resorts to that device. Can I propose something this weekend ?

[savask]

The proposed text is either superfluous (if you already understand DV conditions), or confusing (if you don't know DV conditions yet, then you'll be even more at a loss after reading that).

I'm not as well-versed in $d conditions as others here, so I can be considered an outsider in that regard. I tried reading David's comment, and it indeed completely went over my head, so I tend to agree with benjub's remark :-)

[david-a-wheeler]

@benjub : Can I propose something this weekend ?

Of course! I tried to clarify things, but it's not clear I succeeded, so I'd love to see your take. I'll mark this PR as "draft". Please create your own PR, I suspect it'll be better!

[tirix]

This explanation might be clearer if we provided some examples of what a theorem would become if the $d distinct variable conditions were replaced with additional hypotheses for provided there are at least N variables in the metalogic.

This translates into a bunch of -. A. x x = y as antecedents, and @wlammen has some examples in his mathbox: Compare for example 2sb6 and wl-2sb6d.

So my idea would be to move such an example theorem to main and cite it as an example.

Maybe @benjub had something similar in mind when reworking comments in #3761.

[benjub]

So, I reread https://us.metamath.org/mpeuni/mmset.html#distinct and I think it is a good explanation, with no need to add anything to it. Therefore, I think that the proposal I made above to simply link to it is sufficient.

I made a proposal in #3786.

[jkingdon]

This translates into a bunch of -. A. x x = y as antecedents, and @wlammen has some examples in his mathbox: Compare for example 2sb6 and wl-2sb6d.

Now this is something which attracts my attention - making the point via proved theorems. The ideal example wouldn't use ax-5 at all (and thus, perhaps, would be something simpler than 2sb6). Of course this would be in a separate section ("life without ax-5") and most of the sections could remain on the "life without ax-13" course we have been talking about.

[tirix]

This translates into a bunch of -. A. x x = y as antecedents, and @wlammen has some examples in his mathbox: Compare for example 2sb6 and wl-2sb6d.

The ideal example wouldn't use ax-5 at all (and thus, perhaps, would be something simpler than 2sb6).

2sb6 and wl-2sb6d seemed to be a good example because of the numerous hypotheses added, which correspond exactly to each pair of distinct variable, and the fact that it is already proven. But any other example would work.

[benjub]

Can we close this PR as superseded by #3786 ?

[jkingdon]

Can we close this PR as superseded by #3786 ?

That would be my preferred course of action. Adding more text is something to be a bit wary of, and as far as I could tell #3786 covers it.

[benjub]

Given that @jkingdon, @tirix, and @avekens (see #3786 (review)) agree, I'm going to close this PR as superseded by #3786) barring some oppositions in the next few days.

[jkingdon]

Given that @jkingdon, @tirix, and @avekens (see #3786 (review)) agree, I'm going to close this PR as superseded by #3786) barring some oppositions in the next few days.

We can always reopen it or make a new issue or pull request if someone wants to revisit later.

[jkingdon]

Superceded by #3786