On Megill's completeness theorem

[Benoit]

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

[Mario Carneiro]

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).

--
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 metamath+u...@googlegroups.com.
To view this discussion on the web visit https://groups.google.com/d/msgid/metamath/188db4a5-23d4-45be-a8bb-5296c87d6856n%40googlegroups.com.

[Benoit]

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

[Mario Carneiro]

On Sat, Mar 20, 2021 at 11:15 AM Benoit <benoit...@gmail.com> 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

[Mario Carneiro]

On Sat, Mar 20, 2021 at 1:15 PM Mario Carneiro <di....@gmail.com> 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

[Norman Megill]

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 check done by "read") flag these as errors, since a purpose of metamath.exe is to make sure the spec is met, and $d ph ps $. is allowed by the spec.  AFAIK this doesn't lead to any inconsistency, but it could be confusing for a human to follow and maybe create difficulties translating to another proof language.

Tarski uses only the concepts of two variables being distinct and of a variable not occurring in a wff, and we follow that convention in set.mm.  The spec allows any combination of variables to be part of a $d for simplicity.  Its "disjoint variable" concept unifies Tarski's two concepts and I believe simplifies proof verification by not requiring special cases for different variable types.

Benoit's example (PR https://github.com/metamath/set.mm/pull/1957) is intriguing.  I don't think we want to add it to the official set.mm (and in the future it will trigger the "verify markup" warning I mentioned), but I would suggest it remain in set.mm in commented-out form for people who want to explore the idea further in their local databases.

Norm

[Benoit]

Interestingly, it passed all the gitlab tests (metamath.c, rust, python, c++, java, and the additional checks of mmj2 --- thanks DAW for having put them in the continuous integration process).  I then commented out this example in my mathbox.  (To answer Norm's question: it does not lead to any inconsistency; I proved the system sound and the axioms are true in my semantics... I'll write up my notes and share them.)

I think it could be banned (trigger an error) by a verifier of set.mm-like databases (like mmj2), but not by a general-purpose verifier (like metamath.c).  But actually, metamath.c also has a part for set-mm-like databases.  So you option-based proposal sounds good.

Indeed, for general databases, one can define any type of variables so there is no notion of "setvar variable".  Maybe, in Mario's Metamath Zero, the restriction would be to have no DV conditions among non-pure sorts. (?)

Benoit

[Mario Carneiro]

On Sat, Mar 20, 2021 at 9:58 PM Benoit <benoit...@gmail.com> wrote:

Indeed, for general databases, one can define any type of variables so there is no notion of "setvar variable".  Maybe, in Mario's Metamath Zero, the restriction would be to have no DV conditions among non-pure sorts. (?)

Indeed, in MM0 there is no analogue of $d ph ps $. at all, the syntax itself makes such a supposition impossible to write. Variables come in two flavors, bound variables (aka names or first order variables) and regular variables (aka metavariables or second order variables). Bound variables are like "setvar" in set.mm, and they are always disjoint (so $d x y $. is implied for every pair of distinct variables), and regular variables declare which bound variables they can depend on, and by omission which bound variables they must be disjoint from (which defines the $d x ph $. conditions). Regular variables cannot depend on other regular variables. (The sort modifiers actually don't matter here; this has to do with the binders like {x: set} vs (ph: wff x).)

 

Mario