On Sat, Mar 20, 2021 at 1:15 PM Mario Carneiro <[email protected]> wrote:
> 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.) > Oh, and just to call it out explicitly: I'm exploiting the triviality of ph # ps in this proof to assume that v is a setvar, because if v is not a setvar then v # pi_f(x,y) is automatically true (because all term constructors target sorts other than "setvar"). If we use the model with "ph # ps if and only if Free(ph) \cap Free(ps) = \varnothing" then one has to do the same verification where v is not a single variable but rather a set of variables, but other than that nothing really changes about the proof, and the property still holds (so it's still a model). 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/CAFXXJSs%2Bc22CHGZBCu%2BX1TfPjwggRVDFFPA%3D%2BgtsOhCahcuqzg%40mail.gmail.com.
