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
On Saturday, April 18, 2020 at 1:37:38 AM UTC-4, savask wrote:
>
> 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/3721120e-4c6e-4644-9791-b3fba9a6cb59%40googlegroups.com.
