Revise df-cleq and df-clel

[benjub]

As discussed in #3199 (and several years ago in https://groups.google.com/g/metamath/c/xdHB0oW0aZ4/).

[benjub]

@digama0 and @tirix : can you see where the mmj2 error comes from ? It looks like it is about grammar conflicts. Did I introduce some with df-bj-mpt2 ?

On my local install (mmj2 v2.5.3 as of 23-Sep-2019.) there is no error, and I cannot install later versions (see digama0/mmj2#68 and digama0/mmj2#69).

[tirix]

Yes, the problem is likely with your new syntax:

$( Syntax for maps-to notation for functions with two arguments. $)
  cmpt2-bj $a class ( <. x , y >. e. A |-> B ) $.

There is a $j statement saying unambiguous 'klr 5';.
This means the grammar is unambiguous at depth 5. You probably made the grammar ambiguous, and maybe increasing that number would work - but I'm unsure which other consequences it might have.

A statement starting with ( <. x , y >. e. A might not distinguish between for example ( <. x , y >. e. A /\ x < B ) and the new ( <. x , y >. e. A |-> B ) except with a larger depth.

[benjub]

There is a $j statement saying unambiguous 'klr 5';. This means the grammar is unambiguous at depth 5. You probably made the grammar ambiguous, and maybe increasing that number would work - but I'm unsure which other consequences it might have.

Thanks for the explanation. Is this an LR(5) parser or an LALR(5) parser ? In any case, I think that increasing the look-ahead does not degrade complexity by a lot ? It has an effect only when looking ahead by 6 is actually needed, and during the initial phase before the parsing itself, IIRC. I'm inclined to change it to unambiguous 'klr 6';.

[benjub]

I removed that definition and will investigate in a future MR. This is totally unrelated to the main object of this MR anyway.

[tirix]

At least it was worth trying increasing that number.

For reference, here are a few links:

• a post describing the mechanism,
• the source code of the MMJ2 LR Parser
• documentation about grammar ambiguity

Maybe this $j unambiguous 'klr 5';. KLR(5) information is actually not used by the parser, and changing that value has no effect? I could not find the corresponding information in the MMJ2 source (neither a constant set to 5, nor reading the klr 5 $j command)

[avekens]

For me everything looks fine, but I am not so deeply involved in the main topic of this PR, i.e., the change of the very basic definitions df-cleq and df-clel. As long as everything else still works, I trust in this changes. But maybe at least another one should approve these very basic changes.

[icecream17]

I wonder if df-clel should have bj-cleljustab (shorter proof cleljust2) as a hypothesis too

[benjub]

I wonder if df-clel should have bj-cleljustab (shorter proof cleljust2) as a hypothesis too

Ideally, one should do that, but note that there is a formula variable in bj-cleljustab and we can only require a specific instance in an $e-hypothesis, so we can't really require the full scheme bj-cleljustab. (For instance, to prove that $e-hypothesis, you have the liberty of deciding to prove only the instance where ph is T..)

Actually, the case of df-clel looks strictly harder than the case of df-cleq, and I do not see how to prove the same conservativity result as for df-clab and df-cleq... Maybe one has to think of a weaker conservativity statement ?

[icecream17]

Consider an alternate axiom system where an instance of bj-cleljustab is provable without e.g. ax-12, but the scheme bj-cleljustab proves ax-12 (and the hypotheses are provable without ax-12)

Therefore this is non-conservative in an alternate axiom system.

(However, bj-cleljustab uses less axioms than the hypotheses in this axiom system, so it is conservative in that way. (Note that all finite expressions with classes expand to setvars and df-clab))

[GinoGiotto]

Happy to see that this issue is going to be resolved, making axiom minimization clear and easier to do. Hopefully, this PR will settle the debate about these definitions.

[jkingdon]

As discussed in #3199 (and several years ago in https://groups.google.com/g/metamath/c/xdHB0oW0aZ4/).

Thanks for linking to that 2021 mailing list thread.

Although many topics are brought up there, I guess the crux of it is the following comment from Norm:

Once we get to interesting results in set theory, all of the FOL= axioms will pretty much be used anyway. Effort spent to eliminate the use of this or that FOL= axiom in the set theory development doesn't seem productive to me, and it may even be confusing to the reader to see longer proofs that may result just to avoid using a certain FOL= axiom in a set theory theorem.

My reaction to that is that if this is our position, we need to get a lot more specific in terms of how we talk about axiom usage. Somewhat in documentation, but in tools too.

I'm kind of inclined to think the current pull request is a step forward even if I'm not sure it solves everything. But I'm not sure I see any of this clearly enough to have a super clear idea of what is best (which is as rigorous as we justifiably want, but also maintains the approachability of metamath by people who don't know this math already).

[benjub]

To answer a part of @jkingdon's post: this MR does not solve everything, far from it ! The more "urgent" and pratical need that emerged in #3199 was to make sure that every theorem depending on df-cleq (resp. df-clel) depends also on ax-9 (res. ax-8).

In the latest (and last in this MR, hopefully), I added two theorems proved from df-clab only. Actually, I moved one from my mathbox. The recent change in the definition df-sb enabled to use sbequ (which before used auxiliary axioms) to shorten the proof sizably, as noticed by @icecream17 . @icecream17 : is the way I credited the theorems fine with you ?

I'm working on doing that too for df-cleq and df-clel but I'd like to to it in a future MR and merge this one now.

Although many topics are brought up there, I guess the crux of it is the following comment from Norm:

Once we get to interesting results in set theory, all of the FOL= axioms will pretty much be used anyway. Effort spent to eliminate the use of this or that FOL= axiom in the set theory development doesn't seem productive to me, and it may even be confusing to the reader to see longer proofs that may result just to avoid using a certain FOL= axiom in a set theory theorem.

quotes the guy who routinely removes ax-3 from the most advanced theorems ;-) More seriously, the goal of this MR is not to remove axiom dependencies from some proofs but to make more transparent the relative dependencies among them. I agree with the rest of your comment.

[icecream17]

(approve when this is done, or may happen in a later pr)

[avekens]

The command is "show trace_back", but "show trace" works as abbreviation.

[benjub]

Indeed. I would prefer to keep the full command, but on the webpage it appears as in index like TRACE_BACK which is why I made that modification.

[avekens]

You are right, and there are several MINIMIZE_WITH in set.mm which are displayed in the same ugly way. In 2019, I proposed that two consecutive underscores __ should always be treated as literal _ (see google group https://groups.google.com/g/metamath/c/r3pwUvhI3NQ/m/fcEmU5OkAwAJ ). I do not know, however, if this was ever implemented. Currently, there aren't any two consecutive underscores __ in comments of set.mm.

[mazsa]

@digama0 wouldn't you like to weigh in on Benoit's request?

[benjub]

@digama0 wouldn't you like to weigh in on Benoit's request?

I think I will merge this MR since I fear conflicts. We can discuss further in later MRs on the topic. I'll probably try to write up Mario's proof of conservativity in https://us.metamath.org/mpeuni/mmnotes.txt soon. This is basically Levy's proof of conservativity, with Mario's additions to adapt it to the case of set.mm. The precise statement will probably be weaker (i.e. "object level" and not "scheme level").

[mazsa]

Once we get to interesting results in set theory, all of the FOL= axioms will pretty much be used anyway. Effort spent to eliminate the use of this or that FOL= axiom in the set theory development doesn't seem productive to me, and it may even be confusing to the reader to see longer proofs that may result just to avoid using a certain FOL= axiom in a set theory theorem.

My reaction to that is that if this is our position, we need to get a lot more specific in terms of how we talk about axiom usage. Somewhat in documentation, but in tools too.

I'm kind of inclined to think the current pull request is a step forward even if I'm not sure it solves everything. But I'm not sure I see any of this clearly enough to have a super clear idea of what is best (which is as rigorous as we justifiably want, but also maintains the approachability of metamath by people who don't know this math already).

It seems to me that what we may need are the actually valid usage equivalence classes of axioms and explicit preferences among them, see also https://us.metamath.org/mpeuni/mmset.html#subsys . + a description of how to check them like in case of proof lenght minimize_with * /include_mathboxes

[mazsa]

• a description of how to check them like in case of proof lenght minimize_with * /include_mathboxes

#3399 (comment)