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.