pm11.07 in set.mm is not what it appears to be
Norman Megill
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
David A. Wheeler
> 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.
In the long term I'd love to see all PM claims proved or mapped to existing
proof/axioms. It'd be fine if they were in their own section and/or marked
that further usage is discouraged (if don't want them further used).
PM, like all human works, has its flaws, but it truly was the first of its kind.
That said, having a "proof" that doesn't actually prove the original
statement doesn't help. It's better to make it clear that set.mm does *not*
have that proof.
--- David A. Wheeler
Richard Penner
Thomas Brendan Leahy
Benoit
if A,B |- C then B,A |- C.
Indeed, in PM*10.11, which is our ~ ax-gen, the premise reads "if $\phi y$ is true whatever possible argument $y$ may be" (see also PM*9.13 and the paragraph preceding it). In this light, one sees that PM*11.07 would be any instance of our (trivial) scheme ~ idi where \phi is any expression with two free variables. It is necessary in the framework of PM because of their treatment of "propositional functions" (see pp.14 and 38) and their distinction between real and apparent variables.
I did put in my mathbox two proofs of ~ ax-7 similar to the proof of PM*11.2 (which is ~ alcom). The proof of ~ ax7-pm is in the spirit of PM*11.2 but adapted to metamath's framework, whereas the proof of ~ ax7-pm2 mimics PM*11.2 at the cost of lengthening the proof (this is similar to the contrast ~ sp / ~ stdpc4 ).
Benoit
Norman Megill
*11.07 |- phi(x,y) => |- phi(y,x)
which can be expressed in set.mm as
$d u v ph $. $d u v x $. $d u v y $.
pm11.07.1 $e |- ph
pm11.07 $p |- [y/u][x/v][u/x][v/y]ph
(There are other possibilities, depending on how we choose to represent phi(x,y) and ph(y,x).)
Here is my reasoning. To get some background on PM's language usage, let us first look at a simpler situation, their version of the generalization rule:
(p. 144) *10.11 If phi(y) is true whatever possible argument y may be, then A. x phi(x) is true. In other words, whenever the propositional function phi(y) can be asserted, so can the proposition A. x phi(x).
Compare this to their equivalent to specialization (our stdpc4), which is a closed theorem that they show symbolically:
(p. 138) *9.2 |- A. x phi(x) -> phi(y) (also = *10.1 p. 145)
which they express in English as, "what holds in all cases, holds in any one case."
In other words, *10.11 is an inference rule (like our ax-gen) and 9.2 is a closed theorem (like our stdpc4). A key feature is that 10.11 is not expressed as a formula whereas *9.2 is. Also, *10.11 uses the word "true" whereas *9.2 uses the word "holds". Therefore I think we can interpret "true" or "asserted" to mean "is provable", and *10.11 would be express symbolically as:
*10.11 |- phi(y) => |- A. x phi(x)
With this background on their language usage, let's look at *11.07 (p. 156):
*11.07. "Whatever possible argument x may be, phi(x,y) is true whatever possible argument y may be" implies the corresponding statement with x and y interchanged. Pp.
Note the use of the word "true" and the lack of a symbolic representation, just as in *10.11. That suggests this is an inference. So this can be expressed symbolically as
*11.07 |- phi(x,y) => |- phi(y,x)
One thing that is slightly puzzling is why they have x and y in different clauses instead of just saying,
*11.07 "Whatever possible arguments x and y may be, phi(x,y) is true" implies the corresponding statement with x and y interchanged. Pp.
I think they are separating the substitutions and effectively parenthesizing (with a comma) "phi(x,y) is true whatever possible argument y may be" (one substitution) so as to break down the double substitution into two successive single substitutions, "Whatever possible argument x may be, [ phi(x,y) is true whatever possible argument y may be ]". It seems they want to have the phrase "whatever (variable) may be" to be applied to only one variable at a time. I don't see anything more subtle, such as the order of the "whatever"s being important.
Anyway, let's get back to translating *11.07 for set.mm. There are different ways of expressing phi(x,y), but I'll assume the simplest for the hypothesis |- phi(x,y) then apply substitutions to obtain the conclusion. The substitutions leading to the conclusion |- phi(y,x) are (letting u and v be dummy variables not in phi):
phi(x,y) ph
phi(x,v) [v/y]ph
phi(u,v) [u/x][v/y]ph
phi(u,x) [x/v][u/x][v/y]ph
phi(y,x) [y/u][x/v][u/x][v/y]ph
so a possible Metamath equivalent for *11.07 is
$d u v ph $. $d u v x $. $d u v y $.
pm11.07.1 $e |- ph
pm11.07 $p |- [y/u][x/v][u/x][v/y]ph
This can be proved trivially in set.mm with 4 applications of sbt. The $d's are actually unnecessary in set.mm, but I put them in to emphasize that u and v are dummy variables not occurring in ph, otherwise we obtain a slightly stronger statement than PM's *11.07. It is unclear whether *11.07 applies when x and y are the same variable, but I assumed they could be; if not, we should make the last two $d's become $d u v x y $. to be as conservative as possible.
I still have some questions about the details of PM's proof of *11.2 (p. 160), which uses *11.07. Step 2 of the proof, where they omit details, is confusing. Here is one possibility: If we apply *11.07 to step (1) we get A. x A. y phi(x,y) -> phi(w,z) i.e. swap z and w. Then applying *11.11, we assign w to z and z to w simultaneously, then prefix A. w A. z to obtain step (2), A. w A. z (A. x A. y phi(x,y) -> phi(z,w))). My uncertainty is that this requires assuming the x,y in *11.11 are not necessarily distinct from z,w in *11.11, but maybe that's allowed, not sure. If it isn't allowed, we would have to go through another set of dummy variables that aren't shown, in order to obtain step (2).
Norm
Thierry Arnoux
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.
Norman Megill
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
Sure, that could be used. Actually, if you (or anyone) feel like proving
sbco4 $p ([y/u][x/v][u/x][v/y]ph <-> [x/w][y/x][w/y]ph),
that would be a nice theorem for the main set.mm. I chose w on the RHS to keep the dummy variables independent, which might be helpful for seeing the $d's required on each side. And if we can prove it with neither $d u w nor $d v w, then w can be replaced with either u or v in an application. I think the required $d's are: u v ph, u v x, u v y, w ph, w x, w y
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. :)
Norm
André L F S Bacci
I dimly recall that two variables can be swapped without any temporary variables by using 3 bit-wise XOR operations. :)
Norman Megill
1st edition, p. 156:
*11.07. "Whatever possible argument x may be, phi(x,y) is true whatever possible argument y may be" implies the corresponding statement with x and y interchanged. Pp.
*11.07. "Whatever possible argument x may be, phi(x,y) is true whatever possible argument y may be" implies the corresponding statement with x and y interchanged except in "phi(x,y)". Pp.
The 2nd edition version is the one discussed earlier in this thread, but I had forgotten about it in the 8 months that elapsed. Of course the extra condition 'except in "phi(x,y)"' completely destroys what I say below, and I'm more confused than ever.
Back to the drawing board.
Norm
Benoit
Back to the drawing board.
Norman Megill
The 1909 1st edition is public domain (published before 1923) whereas the 1927 2nd edition is still under copyright in the US. When I downloaded it a decade ago, the 1st edition was available on a university archive of public domain works, but the 2nd was very hard to locate even as a hard copy. The MIT library relocated it to rare books so you couldn't check it out or even copy it due to its brittleness, and people were selling it for thousands of dollars on amazon. I'm glad archive.org now provides it.
I noticed archive.org also has Takeuti and Zaring (the primary set theory reference in set.mm), which can be "borrowed" for 14 days like a library. I read they were granted status as a public library in the US.
Norm
Jim Kingdon
> Sure, that could be used. Actually, if you (or anyone) feel like proving
>
> sbco4 $p ([y/u][x/v][u/x][v/y]ph <-> [x/w][y/x][w/y]ph),
>
> that would be a nice theorem for the main set.mm. I chose w on the
> RHS to keep the dummy variables independent, which might be helpful
> for seeing the $d's required on each side. And if we can prove it with
> neither $d u w nor $d v w, then w can be replaced with either u or v
> in an application. I think the required $d's are: u v ph, u v x, u v
> y, w ph, w x, w y
the distinct variable constraints above plus one - $d v w . I suspect it
could be removed but I thought it better to send what I have so far
without delay.
> I dimly recall that two variables can be swapped without any temporary
> variables by using 3 bit-wise XOR operations. :)
modify the value of a variable in place (such as metamath, or even some
programming languages) would end up with something which amounts to a
temporary variable anyway.