Can a floating hypothesis become essential?
78 views
Skip to first unread message
savask
Apr 18, 2020, 1:37:38 AM4/18/20
to Metamath
I have a somewhat silly question regarding the Metamath spec. Consider the following database:
$c A |- wff $.
$v x $.
wx $f wff x $.
${
hyp $e wff x $.
ax $a |- A $.
$}
th $p |- A $= wx wx ax $.
The axiom "ax" has two mandatory hypotheses: an essential hypothesis "hyp" and a floating hypothesis "wx", which turns out to be identical to "hyp". Now, the proof for theorem "th" pushes the expression "wff x" two times on the proof stack by calling floating hypothesis "wx", and then tries to apply axiom "ax". As far as Metamath spec goes, the proof stack doesn't seem to "know" whether its content came from a floating or an essential hypothesis, so the proof should be verified as correct. I checked this database in the MM Tool and checkmm.cpp verifiers, and they do indeed accept it, but what's interesting is that metamath.exe doesn't:
?Error on line 11 of file "weird.mm" at statement 8, label "th", type "$p":
th $p |- A $= wx wx ax $.
^^
Statement "ax" (proof step 3) has its "$e" hypothesis "hyp" assigned the "$f"
hypothesis "wx" at step 2. The assignment of "$e" with "$f" is not allowed.
Why is that? As far as I can tell from the Metamath book, this proof should be OK.
This question arose when dealing with the following programming issue. I've been playing with writing my own Metamath tool, and at one point I decided that I need a data structure representing the linear proof format. For me, a linear proof is just a list of proof steps where each step contains the step label, theorem label, expression and a list of hypotheses step labels. Usually one wants to hide floating hypotheses from the latter list, so the question is, how do I tag floating hypotheses? I decided to split the step hypotheses list in two, one part for floating and another part for essential hypotheses, but it looks like the metamath.exe program instead tags _steps_ as floating/essential/etc (at least, that's how it appears in the /lemmon style proof).
So does it matter whether the step expression was obtained from a floating/essential/axiomatic/etc statement? Or as far as the proof stack doesn't care about expressions' "heritage", one can omit that information from the linear proof?
$c A |- wff $.
$v x $.
wx $f wff x $.
${
hyp $e wff x $.
ax $a |- A $.
$}
th $p |- A $= wx wx ax $.
The axiom "ax" has two mandatory hypotheses: an essential hypothesis "hyp" and a floating hypothesis "wx", which turns out to be identical to "hyp". Now, the proof for theorem "th" pushes the expression "wff x" two times on the proof stack by calling floating hypothesis "wx", and then tries to apply axiom "ax". As far as Metamath spec goes, the proof stack doesn't seem to "know" whether its content came from a floating or an essential hypothesis, so the proof should be verified as correct. I checked this database in the MM Tool and checkmm.cpp verifiers, and they do indeed accept it, but what's interesting is that metamath.exe doesn't:
?Error on line 11 of file "weird.mm" at statement 8, label "th", type "$p":
th $p |- A $= wx wx ax $.
^^
Statement "ax" (proof step 3) has its "$e" hypothesis "hyp" assigned the "$f"
hypothesis "wx" at step 2. The assignment of "$e" with "$f" is not allowed.
Why is that? As far as I can tell from the Metamath book, this proof should be OK.
This question arose when dealing with the following programming issue. I've been playing with writing my own Metamath tool, and at one point I decided that I need a data structure representing the linear proof format. For me, a linear proof is just a list of proof steps where each step contains the step label, theorem label, expression and a list of hypotheses step labels. Usually one wants to hide floating hypotheses from the latter list, so the question is, how do I tag floating hypotheses? I decided to split the step hypotheses list in two, one part for floating and another part for essential hypotheses, but it looks like the metamath.exe program instead tags _steps_ as floating/essential/etc (at least, that's how it appears in the /lemmon style proof).
So does it matter whether the step expression was obtained from a floating/essential/axiomatic/etc statement? Or as far as the proof stack doesn't care about expressions' "heritage", one can omit that information from the linear proof?
Norman Megill
Apr 18, 2020, 9:28:42 AM4/18/20
to Metamath
It looks like this check has been done in metamath.exe all the way back to 1997 (the oldest I have, barring some miracle that allows me to read the ancient TK50 backup tapes in my closet). Right now I can't remember the reasoning behind it, if there was one (other than it is not something one would ordinarily do). The spec was written after the program, and a number of minor things in the program didn't match the spec at first. I tried to synchronize the program and the spec over time, but maybe this one was overlooked. Perhaps I should remove this error message.
Norm
Norm
savask
Apr 18, 2020, 10:47:30 AM4/18/20
to Metamath
I see, thank you for the answer. For a moment I thought that it's some sort of arcane requirement I missed while reading the Metamath book :-)
Perhaps I should remove this error message.
It will be interesting to see comments from other people (and to see if there are any malicious ways to use this peculiarity), but in case it all works out well, may I suggest to modify the metamath program in a way such that these kinds of proofs would check, but the program would still show a warning message? That way we may eventually find out if there's any use to this behavior.
Norman Megill
Apr 18, 2020, 6:02:29 PM4/18/20
to Metamath
OK, I'll turn it into a warning. If in the future we determine that it has a legitimate use, we can easily turn off the warning. But the warning will at least notify the user that something very unusual is being done.
Norm
Norm
Reply all
Reply to author
Forward
0 new messages