It's probably a good thing that these DV conditions be forbidden in set.mm-like databases (but not in general databases). More precisely, any $d statement containing at least two non-setvar metavariables should raise an error, and not be silently ignored (as would be the case if implementing your model). In particular, $d x A ph $. should not be silently translated to $d x A $. $d x ph $.
Indeed, your model "ignores" these DV conditions (page 12, line 2 of "Models for Metamath" v4 arXiv). And indeed, the meaning I gave to these DV conditions is the one corresponding, in your notation, to ph # ps if and only if Free(ph) \cap Free(ps) = \varnothing which I think is closer to the intended meaning of any Metamath system, reflecting the phrase "disjoint variables". By the way: the coherence rule "ph # ps -> ph # x, if x is a subterm of ps" is no different from the coherence rule "x # ph -> x # y, if y is a subterm of ph" needed to prove your Theorem 4. Where in the paper do you prove it ? And does it correspond to the "freshness substitution" property of Definition 3 ? Benoit On Saturday, March 20, 2021 at 1:18:57 PM UTC+1 [email protected] wrote: > 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/9ae5d465-f989-4958-8947-40f277f1bcd2n%40googlegroups.com.
