In the help section of the minimizer there is this statement:
2. The use of / FORBID without / ALLOW_NEW_AXIOMS has no effect.
Which is not true, so I removed it.
Example that shows why it's not true:
$c |- A B $.
ax-1 $a |- A $.
ax-2 $a |- A $.
${
hyp.1 $e |- A $.
hyp.2 $e |- A $.
inf $a |- B $.
$}
th $p |- B $= ax-1 ax-2 inf $.
Metamath - Version 0.199.pre 29-Jan-2022 Type HELP for help, EXIT to exit.
MM> READ test.mm
Reading source file "test.mm"... 161 bytes
161 bytes were read into the source buffer.
The source has 9 statements; 3 are $a and 1 are $p.
No errors were found. However, proofs were not checked. Type VERIFY PROOF *
if you want to check them.
MM> PROVE th
Entering the Proof Assistant. HELP PROOF_ASSISTANT for help, EXIT to exit.
You will be working on statement (from "SHOW STATEMENT th"):
9 th $p |- B $= ... $.
Note: The proof you are starting with is already complete.
MM-PA> MINIMIZE_WITH * /MAY_GROW
Bytes refer to compressed proof size, steps to uncompressed length.
Scanning forward through statements...
Proof of "th" remained at 3 steps using "ax-1".
Proof of "th" remained at 3 steps using "ax-2".
MM-PA> SHOW NEW_PROOF /NORMAL
Proof of "th":
---------Clip out the proof below this line to put it in the source file:
ax-2 ax-2 inf $.
---------The proof of "th" (13 bytes) ends above this line.
MM-PA> EXIT
Warning: You have not saved changes to the proof of "th".
Do you want to EXIT anyway (Y, N) ? Y
Exiting the Proof Assistant. Type EXIT again to exit Metamath.
MM> PROVE th
Entering the Proof Assistant. HELP PROOF_ASSISTANT for help, EXIT to exit.
You will be working on statement (from "SHOW STATEMENT th"):
9 th $p |- B $= ... $.
Note: The proof you are starting with is already complete.
MM-PA> MINIMIZE_WITH * /MAY_GROW /FORBID ax-2
Bytes refer to compressed proof size, steps to uncompressed length.
Scanning forward through statements...
Proof of "th" remained at 3 steps using "ax-1".
MM-PA> SHOW NEW_PROOF /NORMAL
Proof of "th":
---------Clip out the proof below this line to put it in the source file:
ax-1 ax-1 inf $.
---------The proof of "th" (13 bytes) ends above this line.
MM-PA> EXIT
Warning: You have not saved changes to the proof of "th".
Do you want to EXIT anyway (Y, N) ? Y
Exiting the Proof Assistant. Type EXIT again to exit Metamath.
MM>
In the example above I executed the minimizer with and without the /FORBID option, returning two different results. This shows that /FORBID can have some effects even without the /ALLOW_NEW_AXIOMS option.
In the help section of the minimizer there is this statement:
Which is not true, so I removed it.
Example that shows why it's not true:
In the example above I executed the minimizer with and without the
/FORBID
option, returning two different results. This shows that/FORBID
can have some effects even without the/ALLOW_NEW_AXIOMS
option.