I will probably add a check to metamath.exe in "verify markup" to issue a
warning if a $d statement has multiple wff and/or class variables (along
with a qualifier to skip that check if it isn't desired for some reason).
We probably don't want to have "verify proof" (or the initial syntax
Hi all,
I wanted to share a simple remark, which is probably known to some.
Megill's completeness theorem [Megill, Thm. 9.7] proves that all true
schemes with DV conditions of the form DV(x,y) and DV(x,ph) are provable
from ax-mp, ax-gen, ax-1--13. One can ask about schemes with DV conditions
