Eliminating $d conditions

[Giovanni Mascellani]

Hi,

suppose that I have a .mm file with a theorem (let it be $p or $a, I
guess it does not matter) involving the variables x and y. Suppose that
said theorem has a condition $d x y $. (also suppose, for simplicity,
that it does not have any other $d condition). Let us call this theorem
thm1. Suppose that the same .mm file has another theorem whose thesis
and hypotheses are just equal to thm1, except that all instances of y
were replaced by x and the $d condition has been removed. Let us call
this second theorem thm2.

Now, what these two theorems are saying, is that the thm1 is true both
if x and y are the same variable (case thm2) and if they are not (case
thm1). So I would be tempted to think that a third theorem thm3 should
be provable from the same axioms, a theorem which has the same thesis
and hypotheses as thm1, but without the $d condition. Baiscally, this
would mean that I could remove a $d condition by proving a variant of a
theorem in which the distinct variables have been set to the same thing.
However, I believe this is not actually possible in general in Metamath.

Is this just an artifact of the Metamath language, or is there any deep
reason why this should not happen? Or am I mistaken in saying that thm1
and thm2 should be in some sense equivalent to thm3? Or am I mistaken in
saying that thm3 is not actually derivable in general?

Thanks for helping me understand.

Giovanni.
--
Giovanni Mascellani <g.masc...@gmail.com>
Postdoc researcher - Université Libre de Bruxelles

[Mario Carneiro]

> Is this just an artifact of the Metamath language, or is there any deep
reason why this should not happen? Or am I mistaken in saying that thm1
and thm2 should be in some sense equivalent to thm3? Or am I mistaken in
saying that thm3 is not actually derivable in general?

The situation is a bit subtle. In general, for an arbitrary Metamath database, this property, that we call "bundling", need not hold. There are models of metamath databases where $d means more than just two variables are unequal, and in these models bundling is not true. If you are familiar with intuitionistic logic or topological models, you can think of $d x y as saying that x and y are "well separated", and x and x are, well, equal, but quantifying over arbitrary x,y considers even those "almost equal" in-between things, and asserting that any two variables are either well separated or equal is an equivalent to decidability of variable equality in the metalogic.

However, for set.mm, this is not a problem - bundling is a theorem. If you want to prove a theorem about x,y, you use excluded middle on the proposition "A. x x = y". When this is true, you can use dral1 and similar theorems to replace y by x everywhere and use thm2, and when it is false "-. A. x x = y" is a distinctor, so you can deduce "F/_ x y" and from there you can change y for a fresh variable z using cbval and similar theorems, and then apply thm1 (with z in place of y).

Incidentally, in iset.mm ax-12 is called the bundling axiom, and enables this reasoning even in the intuitionistic logic database. This is justified because usually even when doing intuitionistic logic the variables themselves are drawn from a countable sequence like the natural numbers, so equality of variables (that is, determining whether two variables denote the same variable, not whether they have the same value) is decidable.

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 metamath+u...@googlegroups.com.
To post to this group, send email to meta...@googlegroups.com.
Visit this group at https://groups.google.com/group/metamath.
For more options, visit https://groups.google.com/d/optout.

[Norman Megill]

On Wednesday, August 15, 2018 at 6:00:20 PM UTC-4, Giovanni Mascellani wrote:

Hi,

suppose that I have a .mm file with a theorem (let it be $p or $a, I
guess it does not matter) involving the variables x and y. Suppose that
said theorem has a condition $d x y $. (also suppose, for simplicity,
that it does not have any other $d condition). Let us call this theorem
thm1. Suppose that the same .mm file has another theorem whose thesis
and hypotheses are just equal to thm1, except that all instances of y
were replaced by x and the $d condition has been removed. Let us call
this second theorem thm2.

Now, what these two theorems are saying, is that the thm1 is true both
if x and y are the same variable (case thm2) and if they are not (case
thm1). So I would be tempted to think that a third theorem thm3 should
be provable from the same axioms, a theorem which has the same thesis
and hypotheses as thm1, but without the $d condition. Baiscally, this
would mean that I could remove a $d condition by proving a variant of a
theorem in which the distinct variables have been set to the same thing.
However, I believe this is not actually possible in general in Metamath.

It is possible in general.

Let thm1(x,z) be the same wff as thm1 with all y's replaced by z's.  Note that "replace" means both free and bound occurrences of y are changed to z.  thm1(x,z) will be accompanied by $d x z.

First, we want to convert the $d to a "distinctor" antecedent of the form -. A. x x=y.  Using dvelimv (or one of its variants dvelim*) to help introduce quantifiers, transform thm1(x,z) to (-. A. x x=y -> thm3).  The $d x z will disappear since z does not appear in (-. A. x x=y -> thm3).  How dvelimv is used for this can be a little tricky, but you can look at examples of its use, or if you have an actual example we can walk through it.  The proof of eujustALT seems to have a relatively straightforward use of dvelim to convert $d y w to (-. A. y y=z ->...).

Next, with the help of dral1, dral2, drex1, drex2 to introduce quantifiers, prove (A. x x=y -> (thm2 <-> thm3)) and thus (A. x x=y -> thm3), also with no $d's.  The proof of eujustALT makes use of drex1.

Using pm2.61i, conclude the unconditional thm3 with no $d's.

Norm
 

Is this just an artifact of the Metamath language, or is there any deep
reason why this should not happen? Or am I mistaken in saying that thm1
and thm2 should be in some sense equivalent to thm3? Or am I mistaken in
saying that thm3 is not actually derivable in general?

Thanks for helping me understand.

Giovanni.
--
Giovanni Mascellani

[Giovanni Mascellani]

Dear Mario and Norman,

thank you very much for your help. I sort of grasp what your are saying,
but I could not make it work.

Il 16/08/18 00:32, Mario Carneiro ha scritto:

> When this is true, you can use dral1 and similar theorems to replace y
> by x everywhere and use thm2, and when it is false "-. A. x x = y" is a
> distinctor, so you can deduce "F/_ x y" and from there you can change y
> for a fresh variable z using cbval and similar theorems, and then apply
> thm1 (with z in place of y).

No problem on the "A. x x = y" branch, but I could not prove the "-. A.
x x = y" branch, with neither Mario's nor Norman's approach. Let say
that, for example, I add the following snippet at the end of set.mm:

$c TEST $.

cTEST $a class TEST $.

testxx $a |- x TEST x $.

${
$d x y $.
testxyd $a |- x TEST y $.
$}

I would like to prove:

testxy $p |- x TEST y $= ? $.

The class TEST could be defined as _V times _V, but I want to introduce
new axioms so that I can be sure that the proof of testxy only depends
on testxx and testxyd.

I can easily prove:

testxy1 $p |- ( A. x x = y -> x TEST y ) $=
( cv wceq wal cTEST wbr testxx wb equcomi breq2d sps mpbiri )
ACZBCZDZAENOFGZNNFGZAHPQRIAPONNFABJKLM
$.

However, how would you prove:

testxy2 $p |- ( -. A. x x = y -> x TEST y ) $= ? $.

, from which testxy would follow?

Thanks again, Giovanni.

[Mario Carneiro]

This is actually a bit too easy of an example, in the sense that it doesn't exercise any of the hard cases of the bundling theorem to do with quantification. In this case, you can just reason as follows:

testxyd |- x TEST z

breq2 |- ( z = y -> ( x TEST z <-> x TEST y ) )

chvarv |- x TEST y

You don't even need testxx for this.

It gets more interesting when x and y are involved in quantifiers, like "E.y x TEST y" or "A. x E.y x TEST y". In these cases you have to use cbval and similar theorems to change out any y quantifiers for z quantifiers, and then apply the $d version of the theorem.

[Giovanni Mascellani]

Hi,

Il 16/08/18 16:38, Mario Carneiro ha scritto:

> It gets more interesting when x and y are involved in quantifiers, like
> "E.y x TEST y" or "A. x E.y x TEST y". In these cases you have to use
> cbval and similar theorems to change out any y quantifiers for z
> quantifiers, and then apply the $d version of the theorem.

After understanding the trivial example of "x TEST y", I managed to do
also "E. x x TEST y" and "E. y x TEST y", so I think that now I
understand enough. I would require some more thinking to write a program
to do this automatically, but for the moment I am happy enough of being
able to do bundling by hand. For some reason, I find more difficult the
cases when there are no quantifiers or quantifiers on variables not
involved in the bundling. I guess it's just that my knowledge of the
Metamath library is still lacking.

Thank you, Giovanni.

[Norman Megill]

An open problem in set.mm that I've been playing with off and on for the last few months is exactly the kind of bundling problem you are asking about in this thread.  It is more complicated, though, because we don't have all axioms available.

Specifically, let us discard ax-7, A. x A. y ph -> A. y A. x ph (which has no distinct variable conditions).  Replace it with two new axioms: the weaker ax-7v where x and y are distinct, and the trivial A. x A. x ph -> A. x A. x ph (which is an instance of id, so we don't actually need a new axiom for it).  Is it possible to derive ax-7 with no distinct variable conditions?

I first mentioned this problem here:
https://groups.google.com/d/msg/metamath/iAeDyuyCgRQ/BYTj4OHqAQAJ
(The link inside that post no longer works.)

For current progress and a description, see the link "*19.26.1  Experiments to study ax-7 unbundling" on the Theorem List Contents page.  In set.mm, there are 238 predicate calculus theorems requiring ax-7; of these, I proved 138 from ax-7v, with 90 that I haven't been able to prove yet (if they are possible to prove).

A negative result showing that ax-7 can't be derived from ax-7v would also be nice because it would show the "metalogical" independence of ax-7.


Some of the special cases of ax-7 that I've proved from ax-7v are the following.  I think it is interesting that these are possible at all, but we're still some distance from ax-7 in its most general form.

ax7w12AUX7 provides a tool to prove all cases where the ph in ax-7 consists of any logical combination of atomic formulas with no quantifiers, containing only x and y and no wff metavariables.  ax7w13AUX7 (with no $d) illustrates an application of ax7w12AUX7.

$d v u x $.  $d y u v $.  $d ph x $.  $d ph y $.
ax7w12AUX7 $p |- ( A. x A. y [ x / u ] [ y / v ] ph -> A. y A. x [ x / u ] [ y / v ] ph )

ax7w13AUX7 $p |- ( A. x A. y x e. y -> A. y A. x x e. y ) $= ... $.


ax7w10AUX7 and axw11AUX7 are curious special cases allowing an arbitrary ph, with no distinct variable conditions.

ax7w10AUX7 $p |- ( A. x A. y ( x = y /\ ph ) -> A. y A. x ( x = y /\ ph ) )

ax7w11AUX7 $p |- ( A. x A. y ( -. x = y /\ ph ) -> A. y A. x ( -. x = y /\ ph ) )


By the way, a few years ago I was able to show that ax-9, -. A. x -. x = y with no distinct variable condition, can be derived from the weaker version with x and y distinct (theorem ax9v).  The result is shown as theorem ax9.  The full proof of ax9 from ax9v is longer and more complicated than a typical bundling proof with all axioms available, because we don't have the full strength of ax-9 available to use.

Norm