How does the new df-sb work?

[Eric Schmidt]

I am trying to understand why the new df-sb solves the alpha-renaming problem. It may be true that we cannot use it to prove rename-sb with too few axioms. But we can do a similar  trick with the new definiens:

${
    $d x y z $.  $d t y z $.  $d ph y z $.
    $d x w u $.  $d t w u $.  $d ph w u $.

    new-sbjust $p |- (
        ( A. y ( y = t -> A. x ( x = y -> ph ) )
                               /\ A. z ( z = t -> A. x ( x = z -> ph ) ) ) <->
        ( A. w ( w = t -> A. x ( x = w -> ph ) )
                               /\ A. u ( u = t -> A. x ( x = u -> ph ) ) ) ) $=
      ( weq wi wal wa wsb df-sb bitr3i ) CGHBCHAIBJICJDGHBDHAIBJIDJKABGLEGHBEHA
      IBJIEJFGHBFHAIBJIFJKABCDGMABEFGMN $.
$}

MM> show proof new-sbjust
64   bitr3i.1=df-sb    $a |- ( [ t / x ] ph <-> ( A. y ( y = t -> A. x ( x = y
                        -> ph ) ) /\ A. z ( z = t -> A. x ( x = z -> ph ) ) ) )
70   bitr3i.2=df-sb    $a |- ( [ t / x ] ph <-> ( A. w ( w = t -> A. x ( x = w
                        -> ph ) ) /\ A. u ( u = t -> A. x ( x = u -> ph ) ) ) )
71 new-sbjust=bitr3i $p |- ( ( A. y ( y = t -> A. x ( x = y -> ph ) ) /\ A. z (
 z = t -> A. x ( x = z -> ph ) ) ) <-> ( A. w ( w = t -> A. x ( x = w -> ph ) )
                                  /\ A. u ( u = t -> A. x ( x = u -> ph ) ) ) )
MM> verify proof new-sbjust
new-sbjust
MM> show trace_back new-sbjust /axioms
Statement "new-sbjust" assumes the following axioms ($a statements):
  wn wi ax-mp ax-1 ax-2 ax-3 wb df-bi wa wal cv wceq wsb df-sb

This theorem is proved using only propositional calculus and df-sb. It is certainly not provable with just propositional calculus.

[Steven Nguyen]

If we add the constraint "we are not going to do that" then it "solves" the problem. A rule like "we are not going to do that" would be questionable, but it is less so when most theorems use dfsb instead.

There seems to be no good way to avoid the alpha-renaming axioms in some theorems but not others, without introducing this kind of gap, however much saving the axioms is justified for such theorems. 

--
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 visit https://groups.google.com/d/msgid/metamath/25954fbd-2db8-4bac-9e67-0119216f4806n%40googlegroups.com.

[Matthew House]

Yeah, I agree that the new df-sb seems to be solving the wrong problem. The only full solutions are to add justification hypotheses or justified restatements. I personally prefer the latter (https://github.com/metamath/set.mm/pull/5207) since it doesn't depend so much on the metatheoretic properties of set.mm w.r.t. DV conditions; but either of them would be better than the presently new df-sb.

[ookami]

My main observation was that many proofs using df-sb and in close neighborhood to it, do not need alpha-renaming at all. They substitute just one instance of the definition, and its dummy variable stays fixed during the proof.  Such proofs don't need any external justification, so incorporating one adds unnecessary axiom dependencies to the theorem.

A rewrite of the definition df-sb would look like this

 ( [ t / x ] ph <-> ( A. y ( y = t -> A. x ( x = y -> ph ) ) /\ ( A. y ( y = t -> A. x ( x = y -> ph ) ) <-> A. z ( z = t -> A. x ( x = z -> ph ) ) ) 

The second conjunct is the alpha-renaming capability, so in prose the definition reads roughly like this: Substitution is defined as A. y ( y = t -> A. x ( x = y -> ph ) ), provided alpha-renaming is possible.

Such constructs are common. For example df-eu: ( E! x ph <-> ( E* ph /\ E. x ph )  which one may interpret as: Existential Uniqueness is equivalent to Uniqueness, provided an x exists fulfilling ph.

So if you can somehow provide a ph for which alpha-renaming fails, well, then [ t / x ] ph is simply false, even if A. y ( y = t -> A. x ( x = y -> ph ) ) holds. But dfsb shows you cannot come up with such a ph unless some common axioms around equality and universal quantifiers are not generally valid.  So don't look for them unless you are considering really weird universes.

To the first poster here, erics... Your observation is no surprise for me.  Using just2-df you can derive the old justification

( A. y ( y = t -> A. x ( x = y -> ph ) ) <-> A. z ( z = t -> A. x ( x = z -> ph ) ) ) 

directly from the new definition restricted to propositional logic only.  The definition itself has this expression, so to say, built in.  Your example is a complex extension of the old justification, but with no structural elements that demands something extra.

To icecream...  Please use the alpha-renaming support of the definition at freedom, it was deliberately built into it. 

To mattllo... I don't know whether my post here answers your questions.

[ookami]

To better reveal who I am: An abbreviated form of my email address is wolfl...@gmail.com

[Eric Schmidt]

Well, the proof of new-sbjust above shows that the proposed new method of introducing definitions cannot be relied upon to produce accurate lists of required axioms. Unless there is some restriction that we can mechanically enforce to prevent a proof like that.

I have given this matter some more thought. We want definitions to be conservative, but whether this is the case depends on the underlying logic. Definitions with dummy variables are conservative over FOL. However, over a weaker logic that cannot prove the equivalence of the definiens with its alpha-renaming, the definition is not conservative and is therefore invalid. When you are trying to avoid using axioms needed to prove alpha-renaming results, you are using such a weaker logic.

To look at this from a different angle, consider the requirement in ordinary mathematical exposition that concepts are well-defined. The group operation in a quotient group, for instance, is defined by multiplying arbitrarily chosen members of the cosets. It is required to prove that the result does not depend on the choices in order for the definition to be allowed. Any argument using the quotient group logically depends on the well-definedness result. If you try to argue using a "quotient group" defined using a non-normal subgroup, that will not be considered correct, even if it turns out that expanding the definition results in a valid proof. Similarly, definitions with dummy variables require picking a particular setvar metavariable. The definiendum has been well-defined only if we can can prove that the choice of variable doesn't affect the result. This is exactly what is proved in the typical justification theorem. Further, just as with the quotient groups, any argument using the definiendum logically depends on this justification theorem.

In short, if you are working in a logic that does not support alpha-renaming, then definitions involving dummy variables are not conservative and therefore are disallowed. So, if you want to prove something in such a logic, you simply cannot use such definitions. And any putative theorem whose statement contains the definiendum is not meaningful, because the definiendum has not been given a valid definition. This applies to all of the more complicated versions of df-sb, because they still have dummy variables in them.

[ookami]

Why is the list of axioms in new-sbjust not faithful?  The left side of its equivalence can be transformed by propositional logic to

( A. y ( y = t -> A. x ( x = y -> ph ) ) /\ ( A. y ( y = t -> A. x ( x = y -> ph ) ) <-> A. z ( z = t -> A. x ( x = z -> ph ) )

that, if true, roughly states "Hey, I've got a particular ph and y for which the basic term A. y ... holds, and if this basic term holds, it holds for every alpha-renamed one".  Why do you need more than propositional logic to arrive at "The basic term alpha-renamed to w holds, and if this basic term holds, it holds for every alpha-renamed one"? On the other side, if false, the left side states: "I came up with a variable for which the basic term with ph does not hold", and the logic is even simpler then.

Whether you need more axioms to establish the truth of one side is irrelevant to the equivalence of new-sbjust.  In the end is ( ph -> ph ) also provable in propositional logic for ph that is in need of the Axiom of Choice to hold.

Maybe specialize ph to T. to see that all expressions can be established without knowing anything about equality in some cases, so I think one need not demand that all of FOL must be there for a definition of substitution.

I strongly agree with you that df-sb, new or old form, makes generally only sense if all of FOL is there.  That's why it is located where it is, after ax-7.

[ookami]

Ok, you must believe that generally all substitution instances of axioms, definitions and theorems hold likewise.  That's where we live in Metamath a bit beyond pure propositional logic.  A design principle, so to say. 

[Eric Schmidt]

I have read your argument. If I am understanding you correctly, you are claiming that new-sbjust can be proved with just propositional calculus. I remain unconvinced of this. Further, I believe it is provable that it is not. In this post I wish to explain (1) the proof of this and (2) what goes wrong with the informal argument for new-sbjust you presented. These might be done in either order. I will show the proof first.

(1) The proof is based, first, on the observation that propositional calculus does not know what the universal quantifier is, and so as far as it is concerned, A. x ph is just a wff that depends on x and ph somehow. So, it would be possible to interpret A. x ph as any formula we like that depends on x and ph. In particular we can interpret it as just ph. To make this more precise, suppose we have a proof of new-sbjust just from ax-mp, ax-1, ax-2, ax-3, df-bi, and df-an. If we replace every instance of A. X PH -- where X is an arbitrary setvar expression and PH is an arbitrary wff expression -- with just PH, we will still have a valid proof. Or, to specify this in even more detail, every usage of the syntactic axiom wal will have a $f hypothesis proving wff PH. In the list of labels constituting the proof of new-sbjust, we replace the proof of wff A. X PH with the proof of wff PH. The end result of this will be a proof of

        |- (
        ( ( y = t -> ( x = y -> ph ) )
                               /\ ( z = t -> ( x = z -> ph ) ) ) <->
        ( ( w = t -> ( x = w -> ph ) )
                               /\ ( u = t -> ( x = u -> ph ) ) ) )

This is not a theorem of FOL and is false in general. But we can go even further than this. There are eight equality expressions in this formula:

y = t
x = y
z = t
x = z
 
w = t
x = w
u = t
x = u

A similar procedure allows us to replace y = t with, say, ps. (Replace the proof of wff y = t with the single label wps, which asserts wff ps.) Nothing is stopping us from replacing all eight expressions with different wff variables, but it will suffice to replace the first four with ps and the last four with ch. This will give us a proof of

        |- (
        ( ( ps -> ( ps -> ph ) )
                               /\ ( ps -> ( ps -> ph ) ) ) <->
        ( ( ch -> ( ch -> ph ) )
                               /\ ( ch -> ( ch -> ph ) ) ) )

This is not a tautology (it simplifies to |- ( ( ps -> ph ) <-> ( ch -> ph ) ) ). But the theorems of propositional calculus are exactly the tautologies, so we have reached a contradiction.

(2) Now let us see what is the issue with the informal argument for new-sbjust. Which is to say, what prevents us from turning it into a formal proof? My understanding of the situation is this: If have a theorem that says

|- ( A. y ( y = t -> A. x ( x = y -> ph ) ) <-> A. z ( z = t -> A. x ( x = z -> ph ) )

we can freely substitute y and z with any setvars when we use it. However, this is not true when the formula is a hypothesis or an antecedent. In these cases, it can only be used exactly as written. So the gloss of

( A. y ( y = t -> A. x ( x = y -> ph ) ) /\ ( A. y ( y = t -> A. x ( x = y -> ph ) ) <-> A. z ( z = t -> A. x ( x = z -> ph ) )

as, "Hey, I've got a particular ph and y for which the basic term A. y ... holds, and if this basic term holds, it holds for every alpha-renamed one" is not correct. It only says that you can rename y to z, not that you can rename y to any variable. (If ph and y are "particular", so is z!) In particular you will not be able to rename y to w.

[ookami]

(1) Nice observation.  df-sb depends on equality and the universal operator.  Both are not defined, but restricted by axioms.  The question is how much of these are needed by a given usage of df-sb.  You are right when you state propositional logic alone is not sufficient.

(2) Ok, the instantiation of the definition lets you choose z freely, and hopefully you will pick it according to your needs.  The limit is reached when you need many more, as in new-sbjust. Of course, you can add more and more conjuncts to the current definition until the alphabet of set variables is exhausted.  That is no solution, of course.  The justification theorem allowing alpha-renaming still exists in parallel to the definition, so theorems using completely different set variables can be established, but only with the full set of axioms of FOL then.

---

The recent changes to df-sb were only motivated by the observation, that the axiom dependency lists were not correct in many cases.  You observe now a similar problem with new-sbjust.  The axiom dependencies are an important feature of Metamath, allowing to track where the Axiom of Choice is used.  Unfortunately, the way you are allowed to instantiate definitions can omit axioms from the list, that were there, if the proof does not rely on definitions.  It would be critical if the Axiom of Choice is one of those omitted.

Do you have a suggestion how to improve the lists without fail? 

[Matthew House]

For a while now, my proposal for how to improve the lists without fail has been post-hoc justification theorems with a1ii, enforced via a new definition check that verifies the form of the justification theorems. I've tried to explain the idea in https://github.com/metamath/set.mm/issues/4955#issuecomment-3473559397, https://github.com/metamath/set.mm/issues/4955#issuecomment-3478001916, and https://github.com/metamath/set.mm/pull/5207. More recently, I've been working to actually implement a checker for it, which still requires hashing out a few more details before it's ready.

The basic idea is, any usage of an axiom must be wrapped in a special a1ii step, |- ph & |- ps => |- ph. The "ph" is the literal statement of the axiom, while the "ps" is enforced to be exactly the same statement, but with the defined symbol expanded imto its definition, where crucially every bound variable is replaced with a fresh dummy variable.

Fresh dummy variables are precisely the mechanism in Metamath that let us say "this proof follows regardless of what you substitute in for the variable", and cannot possibly be cheated. This way, the justification theorem for the "ps" branch always requires the full set of axioms needed to justify the axiom (be it an alpha-renaming or a simple biid/eqid).

This basic idea can be expanded in a few different ways, e.g., allowing simpler justification theorems with fewer axioms for subcases of a definition; this was one of the points of objection earlier. I'm working to make my new checker fully support the general case.

In the case of the old df-sb, this method would require it to be wrapped in a restatement dfsb whose second "ps" branch is precisely sbjust: so you couldn't use the definition without carrying along the proof that the rename is valid. (In the case of the new df-sb, it would require an alpha-renaming proof for the whole conjunction.)

To view this discussion visit https://groups.google.com/d/msgid/metamath/fd7f2308-6642-4225-93fe-3afc591686b1n%40googlegroups.com.

[Matthew House]

(Sorry, by "any usage of an axiom" I meant "any usage of a definition axiom". Non-definition axioms can still be used freely in this setup, it's only definitions that have special rules and must be wrapped.)

[ookami]

One reason for the broken axiom dependencies is the use of setvar as dummies in a definition.  Being able to choose them freely causes one problem.

The grammar of Metamath can be changed to introduce a new sort of constant dummy variables that cannot be substituted, only promoted to setvar similar to how a setvar can be promoted as a class variable.  This promotion feature allows a dummy variable behave, apart from substitution, like a setvar, and in particular expressions can provably be alpha-renamed to ones with a setvar instead of the dummyvar.  Any such renaming in a proof will introduce axiom dependencies now sometimes missing, while proofs not being dependent on alpha-renaming use the dummyvar as given in the definition.

[Matthew House]

Hmm, there really seems to be two different things you're talking about here:

1. Presently, there's nothing to enforce that users of a definition also use all the axioms needed to justify alpha-renaming.
2. Used correctly, a definition with dummy variables requires that we add the alpha-renaming axioms, even when a given proof might not rely on that alpha-renaming.

My proposal is to fix #1: every use of a definition goes through the wrapper, which we enforce to be a correct proof of alpha-renaming. By "fresh dummy variables", I mean variables that are introduced in the middle of the proof, but don't appear anywhere in its hypotheses or assertion. This is precisely Metamath's way to express that "this proof [of the alpha-renaming] works for any value of the fresh variable satisfying the DV conditions".

The way I see it, #2 is a redundancy problem but not really a correctness problem in the same way #1 is. It's also harder to fix: we can't simply add "special constant setvars", since constants are invisible to DV conditions, so it would break stuff like ax-5. If we really wanted to fix it, we would have to modify the whole primitive syntax of our set.mm language, and I don't think it's worth the cost. (Especially since many classical notions of definition rely on this alpha-renaming to make sense, e.g. df-tru classically wants to be defined as an arbitrary ( ph -> ph ).)

If we want to explore definitions that expose their bound variables to avoid justifying renaming, I think we can simply write new niche definitions for that, without messing with the existing idiomatic definitions. (E.g., I'd be a bit curious what we can prove about the alternative dfsb1-substitution compared to the current doubled-substitution.)

To view this discussion visit https://groups.google.com/d/msgid/metamath/09117f79-5839-43a6-941a-7b5d9a33756dn%40googlegroups.com.

[ookami]

Regarding #1: Yes, that is exactly the issue that the proof of in-ax8 suffers from.  However, this has already been addressed, for example in the current version of df-mo, where the alpha-renaming capability is added as a hypothesis. As a result,  any user of this definition must provide a justification for that capability.

Using a hypothesis resolves two issues:

  (a) It incorporates the justification into any proof that uses the definition, making the dependency immediately immediately visible in the proof itself.

  (b) It provides some flexibility.  This was (wih the former df-sb) exploited in sbt, where the T. as a substitute for ph allows for a simpler justification.

Regarding #2: There seem to be levels of correctness.

The highest level concerns only logical correctness. Once a justification theorem has been established - even if stated separately - the logical correctness of the definition is ensured.  There is still a small enforcement issue: the justification theorem must be proved and appear before the definition.  If these conditions are satisfied, then the definition is fully consistent with both the underlying logic and its implementation in Metamath.

Unfortunately, the list of axiom dependencies displayed for a theorem's proof using such a definition may differ from one avoiding that definition.  In this case the proof itself remains correct, but the displayed dependency information is not.

The next level of correctness concerns the reliability of the information shown on a theorem's web page.  Here again, I see two degrees of correctness.

  (a) The first degree ensures that the displayed list contains every axiom required for a proof, even if it also includes axioms that the theorem does not depend on.  This can be achieved by effectively merging the definition with its            justification, where a general justification theorem is sufficient.

  (b) The second degree aims to display only those axioms that the particular proof actually requires.  This greater precision is likely what a reader expects if they are unaware of Metamath's implementation details.  Ultimately, this            approach seeks to produce a minimal dependency list, which is consistent with the existing practice of contributors revising proofs to reduce axiom dependencies and receiving credit by having their names attached to the                improved proofs.

My proposal of introducing a separate dummy-variable type is intended to eliminate these issues altogether: enforcement, proof correctness, and the correctness  of the displayed dependency list.

The variables for substitution occurring in the definiendum and definiens are then exactly the same, reinforcing the idea that a definition is simply an abbreviation.  Consequently, a definition can always be introduced or expanded in a proof affecting without axiom dependencies or restricting its use through helper theorems.

There is, however, a trade-off. A separate variable type for dummy variables is introduced for dummy variables, and this type is used only in definitions whose definiens contains bound variables.  Each dummy-variable type contains exactly one variable, so renaming is not possible in Metamath.  A dummy variable is otherwise a setvar, and it can be promoted within proofs whenever a setvar is required, so it behaves exactly like an ordinary setvar, except with respect to substitution.  Since it cannot be substituted - it is the sole member of its variable type - it behaves as if it is fixed.  Nevertheless, it is not a constant token in the sense of other syntactic constants that appear in Metamath formulas.