Hm, I would prefer to see DV(ph,ps) as a syntax error, and plausibly some current or future verifier applied to set.mm will error on such things. I know that mmj2 has some hardcoded assumptions in it about the nonexistence of such DV constraints.
It's true that metamath does give meaning to this predicate, although in "models for metamath" I used a trivial model for this relation, namely DV(ph,ps) is always true (therefore any scheme including it is equivalent to one without it). In that model, your example theorem scheme is false, but if you instead model DV(ph,ps) as "for all variables x, either [[ph]](x) or [[ps]](x) is a constant function" (note that in the model, wffs are functions from M^vars to truth values, where vars is the set of all variables, so we can ask whether they are constant wrt any particular variable), then your scheme becomes true and it's still a model (there are some coherence rules like "ph # ps -> ph # x, if x is a subterm of ps" that you have to check, but I believe they hold). On Sat, Mar 20, 2021 at 7:52 AM Benoit <[email protected]> wrote: > > 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 > of the form DV(ph,ps). If such a scheme is provable from that axiom > system, then the same scheme without that DV condition is also provable. > Indeed, such a DV condition cannot be produced from DV conditions of the > form DV(x,y) or DV(x,ph). Therefore, the question is equivalent to the > existence of true schemes with DV(ph,ps) which are false without it. An > example is > > ( ( E. x ph -> A. x ph ) \/ ( E. x ps -> A. x ps ) ) , DV(ph,ps) > > It is true because the DV condition implies that x does not occur in at > least one of ph and ps. Therefore, at least one of the two disjuncts is > true. Without the DV condition, it is false: for instance, substitute x=y > for both ph and ps. > > I added it to my mathbox (locally) and reproved ax-5 from it. I do not > know whether the java tool will complain. Maybe I'll do a git pull request > and see. > > Benoit > > -- > 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/188db4a5-23d4-45be-a8bb-5296c87d6856n%40googlegroups.com > <https://groups.google.com/d/msgid/metamath/188db4a5-23d4-45be-a8bb-5296c87d6856n%40googlegroups.com?utm_medium=email&utm_source=footer> > . > -- 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/CAFXXJSu%2BhFTT58-TAsRHuGbLNBkCujmt_KzEcutEyG4zLh8kMQ%40mail.gmail.com.
