Jim Kingdon wrote on GitHub https://github.com/metamath/set.mm/issues/281 :
"The distinct variable constraints in http://us2.metamath.org:88/mpeuni/pm11.07.html make the theorem a trivial one, which has little application.
The distinct variable constraints between 𝜑
and 𝑥
, and between 𝜑
and 𝑧
, mean that both sides of the theorem ([𝑤 / 𝑥][𝑦 / 𝑧]𝜑
and [𝑦 / 𝑥][𝑤 / 𝑧]𝜑
immediately simplify to 𝜑
(via nfv
and sbf
and the usual machinery around sbbii
and biconditional transitivity).
In case the above is unclear, here's the trivial proof above as a metamath compressed proof of pm11.07
(this is for the 20-Jan-2018 version of set.mm but applies with slight changes to iset.mm too):
$= ( wsb nfv sbf sbbii bitri bitr4i ) ADCFZBEFZAADEFZBCFZMABEFALABEADCADGZHI
ABEABGZHJOABCFANABCADEPHIABCQHJK $.
As for what *11.07
in Principia really is, here is the text from page 152 of https://ia600602.us.archive.org/35/items/PrincipiaMathematicaVolumeI/WhiteheadRussell-PrincipiaMathematicaVolumeI_text.pdf :
*11·07. "Whatever possible argument x may be, 𝜑(x,y) is true whatever possible argument y may be" implies the corresponding statement with x and y interchanged except in "𝜑(x, y)". Pp.
I don't think I can confidently turn that into metamath notation. The translation given in pm11.07
might be roughly correct with different distinct variable constraints,
or it might just map to the fact that metamath theorems are all
(implicitly) theorem schemas, or perhaps something else.
As for what to do about it, perhaps just delete pm11.07
?
The history seems to say this came from a mathbox originally, don't
know if that user is still active or if anyone else wants to pick up the
baton."
(end Jim Kingdon quote)
My comment:
In PM, *11.07 is a very confusing statement, and unfortunately they don't offer a version expressed in symbols. It is also an axiom, which is what "Pp." (primitive proposition) means, so we can't deduce what it is from its proof. At first I thought maybe it meant "A. x A. y phi(x,y)" and "A. y A. x phi(x,y)" could be interchanged i.e. our alcom. But now I see that *11.2 is our alcom. The *11.2 proof claims to use *11.07, but I don't understand how *11.07 is applied (since I don't understand *11.07 in the first place) or why dummy variables are needed in its proof. In theorem alcomiw we do use a dummy variable to derive a weak alcom from Tarski's axioms, but those axioms have nothing comparable to *11.07.
I found this:
http://math.boisestate.edu/~holmes/holmes/pmsemantics.pdf
where Randall Holmes says about *11.07: "Incomprehensible, used to interchange universal
quantifiers."
It is somewhat disturbing that PM rests on the foundation of an axiom that no one seems to understand. I do agree that whatever *11.07 is, it is not pm11.07. I will delete it from set.mm if no one has a better idea of how to correct it.
Norm
Very interesting. I concur with the interpretation of *11.07.
However, why not use this simpler formula for swapping x and y in
ph?
[x/v][y/x][v/y]ph
This is actually the standard way to swap variables when programming, with the help of a third temporary one, so I can relate to it :)
_
Thierry
--
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.
Very interesting. I concur with the interpretation of *11.07.
However, why not use this simpler formula for swapping x and y in ph?
[x/v][y/x][v/y]ph
This is actually the standard way to swap variables when programming, with the help of a third temporary one, so I can relate to it :)
I dimly recall that two variables can be swapped without any temporary variables by using 3 bit-wise XOR operations. :)
Back to the drawing board.