ex-natded5.3i used on minimize

[Alexander van der Vekens]

After minimizing a proof (min */ver) of a theorem within my Mathbox I observed that the theorem ex-natded5.3i  was used to shorten my proof. I wonder if this should happen or actually be allowed, because this theorem is only an example in section  "Natural deduction examples". In my opinion this should not be allowed, because if my theorem is moved to the main part, its proof will become invalid! How can this be avoided? Maybe by treating part 17 (and also parts 18-20) in the same way as part 21 (Mathboxes) - then the applications must be modified accordingly. Or by adding "(New usage is discouraged.)" to all the theorems in parts 17-20.

Furthermore, there should be an "official" version of theorem ex-natded5.3i in the main part (Section "Logical disjunction and conjunction") which could be used instead:

    ex-natded5.3i.1 $e |- ( ps -> ch ) $.
    ex-natded5.3i.2 $e |- ( ch -> th ) $.
    ex-natded5.3i $p |- ( ps -> ( ch /\ th ) ) $=

Until this problem is "solved", I'll use

min */ver/forbid ex-natded5.3i

[Norman Megill]

On Wednesday, August 7, 2019 at 10:07:46 AM UTC-4, Alexander van der Vekens wrote:

After minimizing a proof (min */ver) of a theorem within my Mathbox I observed that the theorem ex-natded5.3i  was used to shorten my proof. I wonder if this should happen or actually be allowed, because this theorem is only an example in section  "Natural deduction examples". In my opinion this should not be allowed, because if my theorem is moved to the main part, its proof will become invalid! How can this be avoided? Maybe by treating part 17 (and also parts 18-20) in the same way as part 21 (Mathboxes) - then the applications must be modified accordingly.

The label "mathbox" is hard-coded in metamath.exe as a simple way to identify the start of the mathbox section.  In principle it could become a variable label specified by a $t directive that would set it to the first theorem in part 17 to accomplish what you are suggesting.  But it means another complication for users to learn, and the "minimize_with" qualifier "/include_mathboxes" would become misleading.  It doesn't feel right to me.
 

Or by adding "(New usage is discouraged.)" to all the theorems in parts 17-20.

I think that is the right approach.  Actually, I think all theorems in parts 18-20 already have the discouraged tag, as well as many or most theorems in part 17.  Putting the tag on the rest of the part 17 theorems shouldn't be a big effort, and it should be done.

Another question, though, is whether ex-natded5.3i is actually generally useful or whether your "minimize" hit was something rare.  This could be determined by temporarily moving ex-natded5.3i up as early as possible and running "minimize" on the theorems below to see what usage results.  If it turns out to be used enough times to "pay for itself" (i.e. results in a net reduction of set.mm size), then a copy can be placed early in set.mm with a more meaningful name.

Since David organized the natural deduction section, he may want to weigh in.
 

Furthermore, there should be an "official" version of theorem ex-natded5.3i in the main part (Section "Logical disjunction and conjunction") which could be used instead:

    ex-natded5.3i.1 $e |- ( ps -> ch ) $.
    ex-natded5.3i.2 $e |- ( ch -> th ) $.
    ex-natded5.3i $p |- ( ps -> ( ch /\ th ) ) $=

Until this problem is "solved", I'll use

min */ver/forbid ex-natded5.3i

---------------------------

Since we're on the topic of "minimize",  I will be making a change to "minimize" in a new version of metamath.exe to be released in a few days, based on some discussions with Benoit.

Currently, by default, the minimized proof may end up depending on more axioms ($a statements).  This is dangerous since often we want a proof to depend on as few axioms as possible.  To prevent this, we need to specify explicitly which axioms we don't want to depend on using e.g. "/no_new_axioms_from ax-*", but people sometimes forget to do this.

In the new program, by default "minimize" will never introduce dependence on new axioms unless we tell it to with a new qualifier, "/allow_new_axioms <label match>".  The most common usage would probably be "/allow_new_axioms df-*"since dependence on new definitions is usually acceptable.

In order to make it easier to fine-tune, I am keeping the qualifier "/no_new_axioms_from <label-match>".  It will override (suppress) the matches of "/allow_new_axioms".  For example, if all we care about avoiding are ax-ac* and ax-reg, then we could use "minimize * /allow_new_axioms * /no_new_axioms_from ax-ac*,ax-reg".  This will do the same thing as "minimize * /no_new_axioms_from ax-ac*,ax-reg" in the current program version.

Note that in the new version, the "/no_new_axioms_from" qualifier in "minimize * /no_new_axioms_from ax-ac*,ax-reg" (i.e. without "/allow_new_axioms *") will have no effect, because by default new axioms are avoided anyway.

I am also leaving in "/forbid <label-match>", although it will be deprecated.  I may eliminate it eventually because I don't think it offers any practical advantage over "/no_new_axioms_from".  ("/forbid" is an older qualifier than "/no_new_axioms_from".)

The qualifier "/allow_growth" will be changed to "/may_grow" (just a name change to reduce the number of characters you need to type to avoid ambiguity with "/allow_new_axioms").

----------------------

There may be some confusion about the differences among "/except", "/no_new_axioms_from", and "/forbid".

"/except a1i" means that statement a1i will be avoided when attempting to shorten the proof.  However, statements depending on a1i, such as syl, may be used to shorten the proof.

"/no_new_axioms_from a1i" (when accompanied by "/allow_new_axioms *" in the new program) means that statement a1i, and all statements depending on a1i such as syl, will be avoided whenever the original proof is not dependent on a1i.  But if the original proof does depend on a1i, then a1i and any of its dependencies may be used to reduce the proof size.  (Normally, the argument "a1i" would be an axiom or axioms rather than a theorem.)
 
"/forbid a1i" means that statement a1i and any statement depending on a1i will be unconditionally avoided when attempting to shorten the proof.  So syl would also be avoided.  This will be the case whether or not the original proof depends on a1i.  (Normally, the argument "a1i" would be an axiom or axioms rather than a theorem.)

Norm

[David A. Wheeler]

I didn't expect ex-natded5.3i to be widely reused, so I am fine with adding "(New usage is discouraged.)". I probably should have done so in the first place.

But as Norm suggests, we should test and see if it is useful to reuse it for minimization. If it turns out to make many other proofs simpler, then fantastic. It is certainly general. We might want to separate the general-purpose theorem and its proof from the example, because the example is trying to a show specific proof approach. That only matters if indeed it appears useful for minimization.

--- David A.Wheeler

[Jim Kingdon]

On 8/7/19 3:43 PM, Norman Megill wrote:
> In the new program, by default "minimize" will never introduce
> dependence on new axioms unless we tell it to with a new qualifier,
> "/allow_new_axioms <label match>".  The most common usage would
> probably be "/allow_new_axioms df-*"since dependence on new
> definitions is usually acceptable.

Thanks for making and describing these changes. I had assumed it already
worked that way, so I think the new behavior will be less suprising and
error-prone.

[Alexander van der Vekens]

It's the second time now I got ex-natded5.3i  into my proof on minimize!

Since it seems that this is a very useful theorem, I want to propose to put it into the first part of set.mm (maybe after ~ jctir), in the following form:

  ${
    jccir.1 $e |- ( ph -> ps ) $.
    jccir.2 $e |- ( ps -> ch ) $.
    $( Inference conjoining a consequent of a consequent to right of the
       consequent in an implication.  (Contributed by Mario Carneiro,
       9-Feb-2017.) $)
    jccir $p |- ( ph -> ( ps /\ ch ) ) $=
      ( syl jca ) ABCDABCDEFG $.
  $}

In my special case, the following segment of a proof (7 lines)

 65 rnggrp       $p |- ( R e. Ring -> R e. Grp )
 66 rnggrp       $p |- ( R e. Ring -> R e. Grp )
 67 eqid         $p |- ( Base ` R ) = ( Base ` R )
 68 d1matid.0    $e |- .0. = ( 0g ` R )
 69 67,68 grpidcl  $p |- ( R e. Grp -> .0. e. ( Base ` R ) )
 70 66,69 syl    $p |- ( R e. Ring -> .0. e. ( Base ` R ) )
 71 65,70 jca    $p |- ( R e. Ring -> ( R e. Grp /\ .0. e. ( Base ` R ) ) )

was replaced by the following segment (5 lines):

5326 rnggrp      $p |- ( R e. Ring -> R e. Grp )
5335 eqid        $p |- ( Base ` R ) = ( Base ` R )
5336 d1matid.0   $e |- .0. = ( 0g ` R )
5337 5335,5336 grpidcl  $p |- ( R e. Grp -> .0. e. ( Base ` R ) )
5338 5326,5337 ex-natded5.3i  $p |- ( R e. Ring -> ( R e. Grp /\ .0. e. ( Base` R ) ) )

[Norman Megill]

On Tuesday, August 20, 2019 at 12:36:53 PM UTC-4, Alexander van der Vekens wrote:

It's the second time now I got ex-natded5.3i  into my proof on minimize!

Since it seems that this is a very useful theorem, I want to propose to put it into the first part of set.mm (maybe after ~ jctir), in the following form:

  ${
    jccir.1 $e |- ( ph -> ps ) $.
    jccir.2 $e |- ( ps -> ch ) $.
    $( Inference conjoining a consequent of a consequent to right of the
       consequent in an implication.  (Contributed by Mario Carneiro,
       9-Feb-2017.) $)
    jccir $p |- ( ph -> ( ps /\ ch ) ) $=
      ( syl jca ) ABCDABCDEFG $.
  $}

Please go ahead and add this as you have suggested.

Also, could you add "(New usage is discouraged.)" to ex-natded5.3i and perhaps the other ex-natded* as well?

Thanks,
Norm

[Benoit]

Alexander, can you check, using the script "scripts/min.cmd", whether the theorem "jccil" (where the conclusion is "( ph -> ( ch /\ ps ) )" ) is also worth adding?
Thanks,
Benoit

[Alexander van der Vekens]

with PR #1059, jccir and jccil (for symmetry reasons) will be available in the main part of set.mm. Furthermore, I added "(New usage is discouraged.)" to the ex-natded* theorems.

By the way, there are two proofs in Mathboxes using ex-natded* theorems:

"ex-natded9.20" is used by "nobnddown".

"ex-natded5.3i" is used by "stoweidlem34".

[Benoit]

On Thursday, August 22, 2019 at 1:11:42 PM UTC+2, Alexander van der Vekens wrote:

with PR #1059, jccir and jccil (for symmetry reasons) will be available in the main part of set.mm. Furthermore, I added "(New usage is discouraged.)" to the ex-natded* theorems.

By the way, there are two proofs in Mathboxes using ex-natded* theorems:

"ex-natded9.20" is used by "nobnddown".

"ex-natded5.3i" is used by "stoweidlem34".

Using min.cmd, I minimized all theorems using jca with jccil and jccir (PR #1068).  In PR #1072, I added a comment to ex-natded5.3i to recommend use of jccir instead.  I also removed the two remaining uses of ex-natded* theorems mentioned by Alexander.

Benoit