Proving ax7v and ax7 in Metamath Zero

[CreateSource]

Hello! I'm Jack, and I've recently picked up Metamath Zero. I've been testing my ability to use it by converting theorems from the original Metamath website to Metamath One. I've recently hit some trouble with doing that because of the differing ideas between "bound" variables and "distinct" variables. I feel like I understand the concepts separately but I don't necessarily know how to translate between them. This has been slowly becoming more of a problem and has caused me to question what I'm doing now at ax-7 proving itself.

Here's a link to the repo, but I'll post examples below: https://github.com/abnormalhare/mm-to-mm1

By trying to specify distinctness, I ended up writing ax7v as such:

`theorem ax7v{x: setvar} (y: setvar) (z: setvar x): $ x =s y -> x =s z -> y =s z $ = 'ax_7;`

It feels weird to write it like this. And it also leads to ax7 being written as:
`theorem ax7{x y z .t: setvar}: $ x =s y -> x =s z -> y =s z $`

This looks wrong because ax-7 did not need any bound variables, but now ax7 needs all of them to be bound?

I did try to read documentation of MM0, including the thesis put here and the markdown MM0 and MM1 files, but it was a little confusing. There's even a part where it references a deleted "Variable Inference" section that I found using git log, but that didn't help. I tried to find other repos that have also converted some theorems of Metamath, but I didn't find any that did ax7.

Is this the answer or am I missing something? 

[Steven Nguyen]

From my vague understanding, I think that none of the variables in

`theorem ax7{x y z .t: setvar}: $ x =s y -> x =s z -> y =s z $`

are bound to each other. They are all of type "setvar", and this type does not depend on any variable. So no actual binding is happening, despite all the variables being a "bound variable".

Contrast with

`theorem ax7v{x: setvar} (y: setvar) (z: setvar x): $ x =s y -> x =s z -> y =s z $ = 'ax_7;`

where z's type depends on x, so x is ..."actively" bound or something


Relevant part of the documentation https://github.com/digama0/mm0/blob/master/mm0.md:  A binder enclosed in curly braces as in `{x: set}` denotes a bound variable, which may appear in dependencies of other types (see "Variable Inference").

[CreateSource]

I agree that ax7v does have some form of "binding" for z from x and that ax7 does not. However, because ax7 depends on ax7v, it requires x to be bound regardless of what the outcome is.

I've also read that part of the documentation, like I stated originally, but "Variable Inference" is not a section in the current version of the documentation, and the old documentation has outdated syntax.

[Gino Giotto]

Mario would be the best person to answer this, but I've noticed myself that DV conditions in MM1 don't quite behave in the same way as in Metamath. In Metamath, you can prove the statement of the full ax-8 by exploiting alpha-renaming of certain definitions (see in-ax8 and ss-ax8). However, in MM1, it seems that deriving the full ax-8 is not possible, and the best we can do is to derive a weaker version of ax-8 with bound variables (see this discussion if you want to enter this rabbit hole):

theorem ax8vvv {a b: set} (c: set): $ a =s b -> a es. c -> b es. c $).

Anyway, this is an example that some unbundling proofs that work in Metamath do not work in MM1, and this is probably by design. After all, it would be strange if the "hidden axiom schema" that Mario mentions in his post, meant to govern bound variables, allowed the user to derive theorems that contain no bound variables at all.

Regarding your specific question, the purpose of the proof of ax7 is to "unbundle" ax-7 (see this post), which means deriving the full version of ax-7 (the one with no DV conditions) from weaker ones (with DV conditions). So, I think what you are trying to do here is to replicate the unbundling process in MM1.

Here is a version that works:

theorem ax7v1 {x: set} (y z: set): $ x =s y -> x =s z -> y =s z $ = 'ax_7;

theorem ax7v2 {y: set} (x z: set): $ x =s y -> x =s z -> y =s z $ = 'ax_7;

theorem ax7 (x y z: set): $ x =s y -> x =s z -> y =s z $

    = '(exlimiiv (equcoms (syld ax7v2 (com23 (syld ax7v2 (a1i (com12 ax7v1)))))) (!! ax6ev w));

I took the names of the used theorems from set.mm, so you should be able to replicate the proof. The generated ax7 has no bound variables at all, and it's identical to the original ax-7. This is problably the closest you can get to the Metamath version of unbundling ax-7. It makes intuitive sense since the Metamath version ax7v1 has the DVs $ x y $ and $ x z $, which seems to coincide to how this MM1 version ax7v1 behaves:

theorem ax7v1_dgen1 {x: set} (z: set): $ x =s x -> x =s z -> x =s z $ = 'ax7v1; --> gives an error: disjoint variable violation at ax7v1 (x, y) -> (x, x)

theorem ax7v1_dgen2 {x: set} (y: set): $ x =s y -> x =s x -> y =s x $ = 'ax7v1; --> gives an error: disjoint variable violation at ax7v1 (x, z) -> (x, x)

theorem ax7v1_dgen3 {x: set} (y: set): $ x =s y -> x =s y -> y =s y $ = 'ax7v1; --> does not give an error (y and z are not disjoint)

You can do an analogous check for ax7v2, which has the DVs $ x y $ and $ y z $. You might encounter similar issues when unbundling ax-8 and ax-9 as well.