Prove tz7.48lem without ax-8

[GinoGiotto]

This proof revision removes dependency of theorem tz7.48lem from ax-8. Also it automatically removes ax-8 from tz7.48-2 as well.

[icecream17]

The way ax-8 is avoided is basically bj-ax8 so idk if this is an actual improvement

[GinoGiotto]

Can you tell where bj-ax8 is used? Metamath.exe doesn't show me:

Metamath - Version 0.198 7-Aug-2021           Type HELP for help, EXIT to exit.
MM> READ set.mm
Reading source file "set.mm"... 43199123 bytes
43199123 bytes were read into the source buffer.
The source has 205354 statements; 2738 are $a and 40892 are $p.
No errors were found.  However, proofs were not checked.  Type VERIFY PROOF *
if you want to check them.
MM> SHOW TRACE_BACK tz7.48lem /MATCH bj-ax8
The proof of statement "tz7.48lem" uses the following earlier statements:
  (None)
MM>

If true that would be odd since bj-ax8 is in a mathbox, and I didn't have /INCLUDE_MATHBOXES activated, so it would be a bug of the minimizer.

Also is it even possible to depend from a statement that appears after the main one? I'm new here, so there might be something that I'm missing.

[icecream17]

I mean that eleq1w is more general than elequ1 but doesn't use ax-8, due to df-clel being "too powerful" in its current state
So the way ax-8 is "saved" here is equivalent to the way it is saved in bj-ax8.

[GinoGiotto]

That's interesting. If df-clel is too powerful, it seems dangerous to leave it like that, shouldn't it have a New usage is discouraged label on it?

However in this case df-clel was already used in fvres and ordtri3, so technically it wasn't introduced as a new dependency for tz7.48lem. The final outcome is still a clear loss.

[tirix]

I originally approved but I did not have @icecream17's sharp eye about axiom dependency!
I think this is pending @icecream17's answer and so I will continue to hold merging for now.

For reference, there were mailing list exchanges between Norm and @benjub about ax-8. I think ultimately, Norm preferred to keep the actual axioms as near to the literature as possible, and so Benoît's suggestions were kept in his mathbox.

@avekens @jkingdon @digama0 don't hesitate to step in if you have an opinion!

[tirix]

It would be nice if we could have a bit more settled situation with respect to https://us.metamath.org/mpeuni/df-clel.html and https://us.metamath.org/mpeuni/df-cleq.html.

I was under the impression that the mailing group discussion settled the point: Norm said he preferred to keep the current axioms, and have the alternative solution in a mathbox, @benjub agreed to do so, and that's the situation we have until now.

Did I understand that correctly? I'm also not diving much into these discussions.

We could reopen that discussion, though.

[icecream17]

A problem with changing the definition now is that currently cleljust2 would add ax-10 ax-12 ax-13 which obscures their actual usages. These axioms would be removed by the new definition of substitution df-ssb.

So if wanting to introduce ax-8 to df-clel, then the choices are either wait until df-ssb is merged or add ax-8 to df-clel in some arbitrary fashion (like with dfcleq and ax-9)

[GinoGiotto]

In case someone isn't following the recent additions in the metamath-knife repo, a discussion about df-clel df-clab df-cleq was brought up in this PR which adds a definition checker.

[icecream17]

Perhaps one could introduce dfclel which arbitrarily introduces ax-8. This would be a quick solution. I say this now because based on #3250 + #3262 it seems this would unintuitively affect $j statements.

Edit: Wait, elequ2 doesn't use ax-8. nvm

[jkingdon]

The ideal of "arbitrarily" introducing ax-8 is, I guess, similar to what we did with ax-9 in https://us.metamath.org/mpeuni/dfcleq.html . But I suppose that sort of thing sidesteps the question of what
the real status (axiom or definition) of df-clel df-clab and df-cleq is.

[jkingdon]

What is the current status of this pull request? I do notice that the definition of df-sb has been changed since it was opened but other than that I'm not too up on our thinking about whether this should be merged or closed or what.

Would be nice to get some kind of resolution so that the list of open pull requests mostly contains ones which need some kind of review/action.

[GinoGiotto]

@jkingdon @wlammen The verifiers are failing after the merge of #3357 which happened a few hours ago. I see other PRs have been merged soon after it, but I think these fails should be addressed first before merging other PRs.

[benjub]

I didn't have time to look at the whole conversation, but indeed there was a discussion on the google group and there are explanations in the comments in my mathbox (if I remember, there is a whole section for df-clel/cleq and ax-8/ax-9.

Here, tz7.48lem depends on df-clel, so it depends on ax-8 anyway, so there is no point in formally removing ax-8 dependency.

[jkingdon]

@jkingdon @wlammen The verifiers are failing after the merge of #3357 which happened a few hours ago. I see other PRs have been merged soon after it, but I think these fails should be addressed first before merging other PRs.

Ah, I'll make a pull request to fix that.

Should have seen that one coming.

[jkingdon]

@jkingdon @wlammen The verifiers are failing after the merge of #3357 which happened a few hours ago. I see other PRs have been merged soon after it, but I think these fails should be addressed first before merging other PRs.

Ah, I'll make a pull request to fix that.

Should have seen that one coming.

Should be fixed by #3362

[GinoGiotto]

Regarding the PR: This was an interesting event because I didn't know that a definition could have some kind axiom-like properties. In general I think this sort of ambiguity might create confusion (it actually confused me at the beginning), so if there is a way to fix that I would be in favour of it.

Currently tz7.48lem depends on both the direct reference of ax-8 and its indirect reference from df-clel. With this change the theorem would only depend on the indirect reference from df-clel. In the past I've found other theorems that could replace ax-8 the same way, and I've been wondering for a while what to do with them, so I decided to wait until a decision would be taken for this PR. With my recent scans, I even decided to skip ax-8 and ax-9, since they would probably return the same outcome, even tho this means to lose some potential axiom reductions.

In case of closing I would write explicitly the exeptions of ax-8 and ax-9 in the Metamath conventions (section "Minimizing axioms and the axiom of choice"), so that this event won't happen again.

[jkingdon]

I didn't know that a definition could have some kind axiom-like properties. In general I think this sort of ambiguity might create confusion (it actually confused me at the beginning), so if there is a way to fix that I would be in favour of it.

As far as I know the "definitions" (or "axioms", we've debated this over the years) with this property are df-bi df-clab df-cleq and df-clel as noted in the "Definitions or axioms?" section of https://us.metamath.org/mpeuni/mmset.html#class

Those are the four which are not checked by the definition checker in mmj2 which runs on every pull request.

[icecream17]

My above comment about (bj-cleljustab/cleljust2) using too many axioms is now outdated since sbequ uses fewer axioms now.

#3199 (comment)

Norm said he preferred to keep the current axioms, and have the alternative solution in a mathbox

(post by Norm in link in above comment)

I would be happy to see this idea explored in a mathbox. Even if we don't import it and change our "official" FOL= axiom system on the MPE home page (which is the result of a lot of fine tuning over many years and admittedly somewhat biased by my personal preferences), it can still exist as an important stand-alone study that can be referenced in the main set.mm and the MPE home page. We do keep some permanent important things in mathboxes, such as the old FOL= axiomatization in my mathbox that is referenced in many places.

I think the "even if we don't import it" suggests that changing the definitions would be allowed. Actually I'm not sure about how chang[ing] our "official" FOL= axiom system relates to adding hypotheses, because BJ's reply seems to talk about a completely different system with ax-7cl ax-8cl and such.

However, the previous post by Norm (relative to above post) does specifically mention adding hypotheses:

They could be restored by adding the corresponding $e hypotheses to these axioms (the $e hypotheses would have exactly the same form as the $a conclusions, with class metavariables replaced by variable metavariables).

I am more open to this, as long as it will put this to rest once and for all. Do we know that other substitutions into A and B of df-cleq and df-clel can't generate FOL= statements that are stronger than these hypotheses?

(my answer to that last part would be yes)

shorter (less detailed) justification of df-clab, df-cleq, df-clel

• df-clab: all usages of wcel so far were wel.
  So wcel simply has a piecewise "definition" of wel and df-clab, which are not ambiguous with each other.
• df-cleq is similar to df-clab but with wceq~weq. However, df-cleq is ambiguous with weq. Therefore a hypothesis "containing" weq is necessary. The hypothesis would look like bj-df-cleq (but without A. u A. v at the beginning).
• df-clel fails the dv check because ∃𝑥(𝑥 = 𝐴 ∧ 𝑥 ∈ 𝐵)) ↔ ∃𝑦(𝑦 = 𝐴 ∧ 𝑦 ∈ 𝐵)) hasn't been proven. (see vjust) But assume it has.
  df-clel is ambiguous with both wel and df-clab, and so would need to contain both. The hypotheses would be a la cleljust and bj-cleljustab (cleljust2 is shorter).

Just to make sure...

oh wait df-tru makes things more complicated.

[GinoGiotto]

I removed my credit since Avoid ~ ax-8 . is not an accurate description and I don't think this change deserves a "revised by" comment anyway.

[benjub]

I removed my credit since Avoid ~ ax-8 . is not an accurate description and I don't think this change deserves a "revised by" comment anyway.

Independently of the credit tag: the proof modification makes the proof longer, it seems, so what is gained ? (that's a genuine question, not a rhetorical one)

[benjub]

Answering @icecream17's latest comment: indeed, the discussion in https://groups.google.com/g/metamath/c/xdHB0oW0aZ4/ was diverted to a second (even if related) topic, and most arguments against changes were actually about the more disruptive changes of not overloading class and setvar equalities. The changes in df-cleq and df-clel, however (summarized and explained in the message https://groups.google.com/g/metamath/c/xdHB0oW0aZ4/m/EYUEt3DDBgAJ, and actually the topic of the initial message of that thread by @wlammen) are much less disruptive.

In that message, I mentioned "concrete implications" of having the current versions of df-cleq and df-clel, which are non-conservative definitions, and this MR is just an illustration of that.

[GinoGiotto]

Independently of the credit tag: the proof modification makes the proof longer, it seems, so what is gained ? (that's a genuine question, not a rhetorical one)

I've been following the discussion that has been ongoing for the past few months, and although I haven't come across a definitive consensus, it seems to me that this change is indeed unnecessary. I think the most sensible thing to do at this point is to reference this case in the Metamath conventions under the section "Minimizing axioms and the axiom of choice" to clarify that replacing ax-8 with df-clel does not generally justify a proof lengthening, effectively making this case an exception. Moreover the conventions indicate a preference for weaker axioms, and since ax-8 is provable from df-clel it doesn't look like this PR would provide added value in this regard either (I still have some uncertainty regarding the nature of df-clel, and whether it even makes sense to assign a "strength" to a definition). Also beginner question: Is it possible to prove df-clel from ax-8? (I guess not, otherwise it could be disclosed as a theorem instead).

[digama0]

(I still have some uncertainty regarding the nature of df-clel, and whether it even makes sense to assign a "strength" to a definition)

You shouldn't be able to assign a strength to definitions, because they don't increase the strength of the system, that's what it means to be a definition. Unfortunately, as I have mentioned on the list in the past df-clel isn't actually a definition, it's an axiom, and I strongly dislike the misuse of the df-* prefix in this case.

[GinoGiotto]

Unfortunately, as I have mentioned on the list in the past df-clel isn't actually a definition, it's an axiom, and I strongly dislike the misuse of the df-* prefix in this case.

Well then I would dare to make a proposal, why not change the name of df-clel into ax-something and convert ax-8 into a proper theorem? I offer myself to make the change if there is consensus for it.

[jkingdon]

Well then I would dare to make a proposal, why not change the name of df-clel into ax-something and convert ax-8 into a proper theorem? I offer myself to make the change if there is consensus for it.

I think I'm probably in favor of it. Background reading includes https://us.metamath.org/mpeuni/mmset.html#class especially the part where it says "Levy presents our three definitions above as axioms rather than definitions." and that whole section. There's something fishy about the status quo in the sense that section calls df-clel conservative when https://us.metamath.org/mpeuni/bj-ax8.html seems to show it is not (well maybe it is conservative if we assume ax-8, but not if we consider the axioms minus ax-8?).

If we do this there is a lot of text to update and we somehow have to say that ax-8 is one of Tarski's axioms even if we are tempted to call it a theorem. Perhaps what to do about ax-8 is a somewhat separate question from what to do about df-clel.

If we want a more incremental change, I also made #3375 which is sort of similar in the sense that it says that whether or not we rename df-clel to ax-* treat it as an axiom for the purposes of whether to rewrite proofs to avoid ax-8.

[benjub]

Well then I would dare to make a proposal, why not change the name of df-clel into ax-something

No, I think df-clel is fine since it is conservative (see precise statement below), like df-cleq and df-clab. There is no unanimous definition of what a definition is (I'm not talking about me, but among recognized authors), so it could be considered one or not depending on your conventions. Not a big deal in my opinion; what is important is conservativity and eliminability, and these notions are clearly defined.

and convert ax-8 into a proper theorem?

Certainly not. It's better to keep modularity. With the current situation, {ax-mp, ax-gen, ax-1--ax-13} is an axiomatization of classical FOL= with one binary predicate and no terms, and that is a nice feature we should keep.

There's something fishy about the status quo in the sense that section calls df-clel conservative when https://us.metamath.org/mpeuni/bj-ax8.html seems to show it is not (well maybe it is conservative if we assume ax-8, but not if we consider the axioms minus ax-8?).

@jkingdon is correct: the current situation is that

{df-clab, df-cleq, df-clel} is conservative over {ax-mp, ax-gen, ax-1--ax-9, ax-ext}

whereas with my proposal, we would have the strictly stronger statement

{df-clab, df-cleq, df-clel} is conservative over {ax-mp, ax-gen, ax-1--ax-7, ax-ext}

As I wrote above and in the google group a few years ago, there are concrete, practical implications of this improvement for our development of set.mm, which are detailed there and which we are seeing in this very thread.

If there is no objection, I'm going to push an MR replacing df-clel and df-cleq by https://us.metamath.org/mpeuni/bj-df-clel.html and https://us.metamath.org/mpeuni/bj-df-cleq.html (I'm going to wait a few days).

edit: I'll remove the extra universal quantifiers A. u A. v from the $e-hypotheses.

[wlammen]

If conservativity is the idea behind the hypothesis of bj-df-cleq, shouldn't the dv condition on u and v be dropped then?

[benjub]

If conservativity is the idea behind the hypothesis of bj-df-cleq, shouldn't the dv condition on u and v be dropped then?

There is a funny fact that actually, DV conditions involving a variable in an $e-hypothesis have practically no effect: on the one hand, adding a DV condition to a scheme always yields a weaker scheme, but on the other hand, anytime the scheme without that DV condition is used in a proof (of a theorem which does not have that $e-hypothesis), then one can replace it with the corresponding scheme with that DV condition, and this is still a valid proof. So the scheme with that DV condition permits to prove exactly the same theorems (without that $e-hypothesis). edit: What is barred is false: the scheme with DV conditions is actually strictly weaker, since you could prove its $e-hypothesis using a degenerate instance.

[not relevant anymore: [Well, "without that $e-hypothesis" is a bit too weak: there could be another scheme i.e.,
${ $d u v $. $e |- F(u, v) $. $p |- G(u, v) ) $}
used to prove the $e-hypothesis of
${ $d u v x y $. $e |- G(u, v) $. $p |- H(x, y) $}
but you get the idea. One could state the result above using "without $e-hypothesis with a set of effective DV conditions including the set of effective DV conditions of that $e-hypothesis". "Effective DV condition" means "DV condition among variables occurring in the scheme.]]

[jkingdon]

Closing per #3375 (comment) and the general sentiment that replacing ax-8 with df-clel doens't accomplish much. Thanks to everyone who helped clarify these matters.