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?
--
You received this message because you are subscribed to the Google Groups
"Metamath" group.
To unsubscribe from this group and stop receiving emails from it, send an email
to [email protected].
To view this discussion on the web visit
https://groups.google.com/d/msgid/metamath/7664abd1-7a64-4c70-8805-b1f07023347e%40googlegroups.com.
