173 views

Skip to first unread message

Jan 22, 2018, 8:41:36 AM1/22/18

to Metamath

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

Jan 22, 2018, 10:58:58 AM1/22/18

to metamath, Metamath

On Mon, 22 Jan 2018 05:41:36 -0800 (PST), Norman Megill <n...@alum.mit.edu> wrote:

> It is somewhat disturbing that PM rests on the foundation of an axiom that

> no one seems to understand.

Agreed.
> 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

Jan 24, 2018, 12:16:18 PM1/24/18

to Metamath

Without weighing in on whether pm11.07 should be deleted, I agree it is not *11.07 which I think is a principle from the text of page 151 approximately (I have no facility with PM notation) written as

(x):(y).Φ(x,y).⊃:(y):(x).Φ(x,y) OR (x,y).Φ(x,y).⊃:(y,x).Φ(x,y) ??

from which *11.2 at the top of page 152 follows given the definition *11.01.

In the same way alcom (*11.2) follows from ax-7 (*11.07)

The proof of *11.2 at the bottom of page 153 appears to use a swap of z,w to w,z from *11.11, thus hiding the use of *11.07. But this is also unclear since I think *11.11 is also not written symbolically so there is ambiguity.

Feb 22, 2018, 11:15:12 PM2/22/18

to meta...@googlegroups.com

Late to the party, but I think this would be:

$d z ph $. $d x y z $.

|- ( A. x A. y ph -> [ x / z ] [ y / x ] [ z / y ] ph )

Sep 16, 2018, 2:13:47 PM9/16/18

to Metamath

My understanding is that PM*11.07 is, in the metamath framework, tautological. It is akin to the structural rule of "exchange" or "permutation":

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

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

Sep 24, 2018, 1:54:43 PM9/24/18

to Metamath

I tried to work out what PM means by their axiom (primitive proposition) called *11.07. Here is my interpretation. The end result is that I think *11.07 really means:

*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

*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

Sep 24, 2018, 9:05:19 PM9/24/18

to meta...@googlegroups.com, 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

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.

Sep 24, 2018, 10:14:19 PM9/24/18

to Metamath

On Monday, September 24, 2018 at 9:05:19 PM UTC-4, Thierry Arnoux wrote:

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

Sep 24, 2018, 10:21:32 PM9/24/18

to meta...@googlegroups.com

On Mon, Sep 24, 2018 at 11:14 PM, Norman Megill <n...@alum.mit.edu> wrote:

I dimly recall that two variables can be swapped without any temporary variables by using 3 bit-wise XOR operations. :)

There is a entire Wikipedia article about that...

André

Sep 24, 2018, 11:28:31 PM9/24/18

to Metamath

Unfortunately, it turns out I was studying the 1st edition, and the 2nd edition is different.

1st edition, p. 156:

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.

2nd edition, p. 152

*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

*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

Sep 25, 2018, 6:05:08 AM9/25/18

to Metamath

Back to the drawing board.

Or back to my post in this thread from Sep 16. I'm not sure what wasn't clear in it.

Benoit

Sep 25, 2018, 11:38:44 AM9/25/18

to Metamath

I read your post again and now fully agree with you that *11.07 represents our idi. I need to destroy my 1st edition copy. :)

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

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

Sep 25, 2018, 6:25:00 PM9/25/18

to meta...@googlegroups.com

On 09/25/2018 03:14 AM, Norman Megill wrote:

> 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

I've done the above at https://github.com/metamath/set.mm/pull/541 with
> 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.

Reply all

Reply to author

Forward

0 new messages

Search

Clear search

Close search

Google apps

Main menu