On Sat, Mar 20, 2021 at 11:15 AM Benoit <[email protected]> wrote:
> 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 $. > At the metamath level, those two are very much not interchangeable. Of course a formal system can have many models, this is the standard relation between syntax and semantics, and all this means is that your example theorem is not derivable from set.mm's axioms, because it has a countermodel. Megill's completeness theorem is about the term model where disjointness means disjointness of variables in the underlying terms, and in that model of course $d ph ps $. is nontrivial. (This is the model defined in Theorem 5.) 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". > That's true. The main reason I "stubbed out" this part of the model is because it's not needed by any axiom. Indeed it's an interesting observation that this is a model, because it shows just how underdetermined the meaning of $d ph ps $. is in set.mm. 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 ? > Actually I mixed up the property; the correct property (which is in the paper) is that v # x, v # y -> v # pi_f(x,y) for every term constructor f. I believe this proof is omitted in the paper, but it's trivial for the usual operations like -> and -. because if ph and ps are constant wrt x then so is (ph -> ps); the interesting cases are the binders. Suppose v # x and v # ph, we want to prove v # (A. x ph). Now v # x means v != x, and v # (A. x ph) means v e/ Free(f |-> forall m in M, ph(f[x->m])), that is, if f and g agree except at v, then forall m in M, ph(f[x->m]) iff forall m in M, ph(g[x->m]), which is true because ph(f[x->m]) iff ph(g[x->m]) because f[x->m] and g[x->m] differ only at v. (In fact, we don't need v != x in this proof at all.) Yes, this is the freshness substitution property, or rather the simplified form of it that appears in the second bullet of Definition 10. Mario -- 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/CAFXXJSuaQejztTUnh4tg9jBeHQ2qp_rh8gNzUqd45P_Jhx2%2BWQ%40mail.gmail.com.
