TODO: Give theorems from [Margaris] and [WhiteheadRussell] actual names

Mario Carneiro

unread,

Sep 24, 2016, 5:13:09 PM9/24/16

to metamath

Currently, the propositional logic theorems from [Margaris] and Principia Mathematica have terrible names, which are basically just the theorem numbers. For example 19.3, or pm2.61. These all need to be renamed to something which better matches set.mm naming conventions; I always get these numbers mixed up.

Any suggestions?

Norman Megill

unread,

Sep 24, 2016, 8:55:56 PM9/24/16

to meta...@googlegroups.com

I don't remember all the 19* names either. It hasn't been too much of a
problem because 'show statement *19.*' shows them all, and I pick the
one I need. A long time ago, I used to keep a printed copy of Margaris'
19.* table handy.

Below is a starting suggestion for the 19.* theorems. Most show a kind
of "distributive" law; for example, in 19.26 the A. distributes over the
/\, leading to "alandi". There are 3 forms of the "di" abbreviation:

"di" - distributive law holds both ways
"ldi" - distributive law holds left to right
"rdi" - distributive law holds right to left

For 19.3 and similar, "sp" means specialization (or simplification) i.e.
discard quantifier; as with "di", we have "lsp" and "rsp".

Suffix "l" means version w/ quantifier (or A. quantifier if there are A.
and E.) on the left e.g. 19.29, 19.17
Suffix "r" means version w/ quantifier on the right e.g. 19.16
Suffix "e" means an E. version when a A. also exists e.g. 19.19

Suffixes "i", "d", "t" mean inference, deduction, and closed theorem
versions as usual. Sometimes the "i" will repeat because of the "di" as
in 19.35ri eximrdii; that is ok.

"2al", "2ex" means double quantification

I've only shown the principle versions with no distinct variables. For
distinct variable version, we add suffix "v" as usual. For restricted
quantifier versions, we use "ral", "rex" as usual.

Below are the main 19.* theorems before the *v and ral* versions. Only
the first line of the conclusion is shown to provide a hint, and $e's
are omitted for brevity.

19.26 alandi $p |- ( A. x ( ph /\ ps ) <-> ( A. x ph /\ A. x ps ) ) $=
19.26-2 2alandi $p |- ( A. x A. y ( ph /\ ps ) <-> ( A. x A. y ph /\ A.
x A. y ps
19.26-3an al3andi $p |- ( A. x ( ph /\ ps /\ ch ) <-> ( A. x ph /\ A. x
ps /\ A. x
19.29 exanrdil $p |- ( ( A. x ph /\ E. x ps ) -> E. x ( ph /\ ps ) ) $=
19.29r exanrdir $p |- ( ( E. x ph /\ A. x ps ) -> E. x ( ph /\ ps ) ) $=
19.29r2 2exanrdi1 $p |- ( ( E. x E. y ph /\ A. x A. y ps ) -> E. x E. y
( ph /\ ps )
19.29x 2exanrdi2 $p |- ( ( E. x A. y ph /\ A. x E. y ps ) -> E. x E. y (
ph /\ ps )
19.35 eximdi $p |- ( E. x ( ph -> ps ) <-> ( A. x ph -> E. x ps ) ) $=
19.35i eximldii $p |- ( A. x ph -> E. x ps ) $=
19.35ri eximrdii $p |- E. x ( ph -> ps ) $=
19.25 aleximldi $p |- ( A. y E. x ( ph -> ps ) -> ( E. y A. x ph -> E. y
E. x ps ) )
19.30 alorldi $p |- ( A. x ( ph \/ ps ) -> ( A. x ph \/ E. x ps ) ) $=
19.43 exordi $p |- ( E. x ( ph \/ ps ) <-> ( E. x ph \/ E. x ps ) ) $=
19.33 alorrdi $p |- ( ( A. x ph \/ A. x ps ) -> A. x ( ph \/ ps ) ) $=
19.33b alordi $p |- ( -. ( E. x ph /\ E. x ps ) -> ( A. x ( ph \/ ps )
<-> ( A. x
19.40 exanldi $p |- ( E. x ( ph /\ ps ) -> ( E. x ph /\ E. x ps ) ) $=
19.40-2 2exanldi $p |- ( E. x E. y ( ph /\ ps ) -> ( E. x E. y ph /\ E.
x E. y ps )
19.8a exrsp $p |- ( ph -> E. x ph ) $=
19.2 alimex $p |- ( A. x ph -> E. y ph ) $=
19.3 alsp $p |- ( A. x ph <-> ph ) $=
19.9t exlspt $p |- ( A. x ( ph -> A. x ph ) -> ( E. x ph -> ph ) ) $=
19.9 exsp $p |- ( E. x ph <-> ph ) $=
19.9d exlspd $p |- ( ps -> ( E. x ph -> ph ) ) $=
19.12 exalim $p |- ( E. x A. y ph -> A. y E. x ph ) $=
19.16 albildir $p |- ( A. x ( ph <-> ps ) -> ( ph <-> A. x ps ) ) $=
19.17 albildil $p |- ( A. x ( ph <-> ps ) -> ( A. x ph <-> ps ) ) $=
19.19 albildie $p |- ( A. x ( ph <-> ps ) -> ( ph <-> E. x ps ) ) $=
19.21 alimdi $p |- ( A. x ( ph -> ps ) <-> ( ph -> A. x ps ) ) $=
19.21-2 2alimdi $p |- ( A. x A. y ( ph -> ps ) <-> ( ph -> A. x A. y ps
) ) $=
19.21bi alrsp $p |- ( ph -> ps ) $=
19.21bbi 2allspd $p |- ( ph -> ps ) $=
19.23 alimdie $p |- ( A. x ( ph -> ps ) <-> ( E. x ph -> ps ) ) $=
19.23bi exlsp $p |- ( ph -> ps ) $=
19.27 alimdil $p |- ( A. x ( ph /\ ps ) <-> ( A. x ph /\ ps ) ) $=
19.28 alimdir $p |- ( A. x ( ph /\ ps ) <-> ( ph /\ A. x ps ) ) $=
19.36 eximdi $p |- ( E. x ( ph -> ps ) <-> ( A. x ph -> ps ) ) $=
19.36i eximdii $p |- ( A. x ph -> ps ) $=
19.37 eximdie $p |- ( E. x ( ph -> ps ) <-> ( ph -> E. x ps ) ) $=
19.38 alimrdi $p |- ( ( E. x ph -> A. x ps ) -> A. x ( ph -> ps ) ) $=
19.39 eximrdie $p |- ( ( E. x ph -> E. x ps ) -> E. x ( ph -> ps ) ) $=
19.24 eximrdi $p |- ( ( A. x ph -> A. x ps ) -> E. x ( ph -> ps ) ) $=
19.32 alordir $p |- ( A. x ( ph \/ ps ) <-> ( ph \/ A. x ps ) ) $=
19.31 alordil $p |- ( A. x ( ph \/ ps ) <-> ( A. x ph \/ ps ) ) $=
19.44 exordil $p |- ( E. x ( ph \/ ps ) <-> ( E. x ph \/ ps ) ) $=
19.45 exordir $p |- ( E. x ( ph \/ ps ) <-> ( ph \/ E. x ps ) ) $=
19.34 exorrdi $p |- ( ( A. x ph \/ E. x ps ) -> E. x ( ph \/ ps ) ) $=
19.41 exandil $p |- ( E. x ( ph /\ ps ) <-> ( E. x ph /\ ps ) ) $=
19.42 exandir $p |- ( E. x ( ph /\ ps ) <-> ( ph /\ E. x ps ) ) $=
19.21t alimdit $p |- ( A. x ( ph -> A. x ph ) -> ( A. x ( ph -> ps ) <->
( ph ->
19.23t alimdiet $p |- ( A. x ( ps -> A. x ps ) -> ( A. x ( ph -> ps )
<-> ( E. x ph

For the pm* ones, I have no suggestions right now but hopefully some
more or less consistent, easy-to-remember naming scheme can be figured
out. Many of the pm* we have already renamed, and a large percentage of
the remaining ones are weird, obscure things that are rarely used. The
ones in most need of renaming can be found with "show label pm*i",
meaning it is used enough that a *i inference version was useful. There
are about a dozen of these, specifically:

pm2.21 pm2.24 pm2.43 pm2.43 pm2.61 pm2.65 pm2.86 pm3.2 pm3.2 pm3.43
pm4.71 pm5.21 pm5.32 pm5.74

Better names for these will go a long way towards addressing the pm*
problem, and maybe most of the others aren't worth doing. Perhaps look
at the actual usage of the others to see which renames would provide the
most benefit.

Norm

On 9/24/16 5:13 PM, Mario Carneiro wrote:
> Currently, the propositional logic theorems from [Margaris] and
> Principia Mathematica have terrible names, which are basically just the
> theorem numbers. For example 19.3, or pm2.61. These all need to be

> renamed to something which better matches set.mm <http://set.mm> naming

> conventions; I always get these numbers mixed up.
>
> Any suggestions?
>

> --
> 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
> <mailto:metamath+u...@googlegroups.com>.
> To post to this group, send email to meta...@googlegroups.com
> <mailto:meta...@googlegroups.com>.
> Visit this group at https://groups.google.com/group/metamath.
> For more options, visit https://groups.google.com/d/optout.

Mario Carneiro

unread,

Sep 25, 2016, 3:51:34 AM9/25/16

to metamath

On Sat, Sep 24, 2016 at 8:55 PM, Norman Megill <n...@alum.mit.edu> wrote:

I don't remember all the 19* names either. It hasn't been too much of a problem because 'show statement *19.*' shows them all, and I pick the one I need. A long time ago, I used to keep a printed copy of Margaris' 19.* table handy.

Below is a starting suggestion for the 19.* theorems. Most show a kind of "distributive" law; for example, in 19.26 the A. distributes over the /\, leading to "alandi". There are 3 forms of the "di" abbreviation:

These are some great suggestions. A few suggested tweaks:

19.29r exanrdir $p |- ( ( E. x ph /\ A. x ps ) -> E. x ( ph /\ ps ) ) $=
19.29r2 2exanrdi1 $p |- ( ( E. x E. y ph /\ A. x A. y ps ) -> E. x E. y ( ph /\ ps )

2exanrdi1 -> 2exanrdir (for consistency with exanrdir)

19.35 eximdi $p |- ( E. x ( ph -> ps ) <-> ( A. x ph -> E. x ps ) ) $=
19.35i eximldii $p |- ( A. x ph -> E. x ps ) $=
19.35ri eximrdii $p |- E. x ( ph -> ps ) $=

For these sorts of things, I would suggest eximldii -> eximdii and eximrdii -> eximdiri; basically I suggest an "i" for inference form and "ri" for reversed inference, similar to ori/orri pairs.

19.25 aleximldi $p |- ( A. y E. x ( ph -> ps ) -> ( E. y A. x ph -> E. y E. x ps ) )
19.30 alorldi $p |- ( A. x ( ph \/ ps ) -> ( A. x ph \/ E. x ps ) ) $=
19.43 exordi $p |- ( E. x ( ph \/ ps ) <-> ( E. x ph \/ E. x ps ) ) $=
19.33 alorrdi $p |- ( ( A. x ph \/ A. x ps ) -> A. x ( ph \/ ps ) ) $=
19.33b alordi $p |- ( -. ( E. x ph /\ E. x ps ) -> ( A. x ( ph \/ ps ) <-> ( A. x
19.40 exanldi $p |- ( E. x ( ph /\ ps ) -> ( E. x ph /\ E. x ps ) ) $=
19.40-2 2exanldi $p |- ( E. x E. y ( ph /\ ps ) -> ( E. x E. y ph /\ E. x E. y ps )

aleximldi -> aleximdi
alorrdi -> alordi
alordi -> alordib
exanldi -> exandi
2exanldi -> 2exandi

The rationale here is that if there is no ldi/rdi/di forms to disambiguate, they should be called just "di". For alorrdi -> alordi, I give that one the primary name because it is the most straightforward distribution theorem, leaving alorldi with the "left" moniker to distinguish from a potential "right" version |- ( A. x ( ph \/ ps ) -> ( E. x ph \/ A. x ps ) ). alordi -> alordib gets the "b" suffix because it is bidirectional "at a cost" (i.e. the focus is on the fact that it is a bidirectional form of alordi).

19.12 exalim $p |- ( E. x A. y ph -> A. y E. x ph ) $=

exalim -> exalcom

19.16 albildir $p |- ( A. x ( ph <-> ps ) -> ( ph <-> A. x ps ) ) $=
19.17 albildil $p |- ( A. x ( ph <-> ps ) -> ( A. x ph <-> ps ) ) $=
19.19 albildie $p |- ( A. x ( ph <-> ps ) -> ( ph <-> E. x ps ) ) $=

albildir -> albidir
albildil -> albidil
albildie -> albidie

19.21bi alrsp $p |- ( ph -> ps ) $=
19.21bbi 2allspd $p |- ( ph -> ps ) $=

Why the different names?
alrsp -> alspd
2allspd -> 2alspd

19.36 eximdi $p |- ( E. x ( ph -> ps ) <-> ( A. x ph -> ps ) ) $=
19.36i eximdii $p |- ( A. x ph -> ps ) $=
19.37 eximdie $p |- ( E. x ( ph -> ps ) <-> ( ph -> E. x ps ) ) $=

eximdi -> eximdia

eximdie -> eximdi

Rationale: eximdie is the more straightforward distribution law, while a forall sneaks into the other one

For the pm* ones, I have no suggestions right now but hopefully some more or less consistent, easy-to-remember naming scheme can be figured out. Many of the pm* we have already renamed, and a large percentage of the remaining ones are weird, obscure things that are rarely used. The ones in most need of renaming can be found with "show label pm*i", meaning it is used enough that a *i inference version was useful. There are about a dozen of these, specifically:

pm2.21 pm2.24 pm2.43 pm2.43 pm2.61 pm2.65 pm2.86 pm3.2 pm3.2 pm3.43 pm4.71 pm5.21 pm5.32 pm5.74

My plan is to give each of these a short name which can be used in all the different variations.

David A. Wheeler

unread,

Sep 25, 2016, 8:19:52 AM9/25/16

to meta...@googlegroups.com, Mario Carneiro

>On Sat, Sep 24, 2016 at 8:55 PM, Norman Megill <n...@alum.mit.edu> wrote:
>> I don't remember all the 19* names either.

Renaming makes sense. One request: please keep a specific citation to the theorem number in each comment just before the individual theorem. That way, it will be easy to see if a particular theorem from Principia Mathematica is already proved.

In the long run I would like to see every theorem from PM proved in set.mm. Now that we can mark "don't use this later", it easy to add something without necessarily automatically reusing it later. I think of set.mm as a modern principia Mathematica... set.mm should have at least as much as the original.

--- David A.Wheeler

Norman Megill

unread,

Sep 25, 2016, 2:39:53 PM9/25/16

to meta...@googlegroups.com

Overall, these changes are probably a good thing for future generations,
but for some current users familiar with the current names it will take
some adjusting. At least for me. :)

I suggest we plan to do these 1 month from now, so there is plenty of
time to field suggestions and objections on this thread, and also time
for users to update set.mm with their latest mathboxes before the change.

On 9/25/16 3:51 AM, Mario Carneiro wrote:
> On Sat, Sep 24, 2016 at 8:55 PM, Norman Megill <n...@alum.mit.edu
> <mailto:n...@alum.mit.edu>> wrote:
>
> I don't remember all the 19* names either. It hasn't been too much
> of a problem because 'show statement *19.*' shows them all, and I
> pick the one I need. A long time ago, I used to keep a printed copy
> of Margaris' 19.* table handy.
>
> Below is a starting suggestion for the 19.* theorems. Most show a
> kind of "distributive" law; for example, in 19.26 the A. distributes
> over the /\, leading to "alandi". There are 3 forms of the "di"
> abbreviation:
>
>
> These are some great suggestions. A few suggested tweaks:

Your changes to my 19.* suggestions seem fine (some of which were fixing
carelessness on my part).

[...]

> For the pm* ones, I have no suggestions right now but hopefully some
> more or less consistent, easy-to-remember naming scheme can be
> figured out. Many of the pm* we have already renamed, and a large
> percentage of the remaining ones are weird, obscure things that are
> rarely used. The ones in most need of renaming can be found with
> "show label pm*i", meaning it is used enough that a *i inference
> version was useful. There are about a dozen of these, specifically:
>
> pm2.21 pm2.24 pm2.43 pm2.43 pm2.61 pm2.65 pm2.86 pm3.2 pm3.2 pm3.43
> pm4.71 pm5.21 pm5.32 pm5.74
>
>
> My plan is to give each of these a short name which can be used in all
> the different variations.
>
> enot, short for "not elimination"

The literature calls pm2.21 the "Duns Scotus law", which is probably too
obscure for most people, It is also called the "principle of
explosion". I don't have a big objection to "enot" though.

pm2.43 is called "contraction" in the literature. The "c" suffix in
syl*c means "syl... combined with contraction". I don't have a big
objection to "imidm" but I'm mentioning it in case someone has a better
idea.

> pm2.43i imidms $e |- ( ph -> ( ph -> ps ) ) $p |- ( ph -> ps )
> pm2.43d imidmsd $e |- ( ph -> ( ps -> ( ps -> ch ) ) ) $p |- ( ph -> (
> ps -> ch ) )
> pm2.43a imidm13d $e |- ( ps -> ( ph -> ( ps -> ch ) ) ) $p |- ( ps -> (
> ph -> ch ) )
> pm2.43b imidm23d $e |- ( ps -> ( ph -> ( ps -> ch ) ) ) $p |- ( ph -> (
> ps -> ch ) )
> pm2.43 imidm $p |- ( ( ph -> ( ph -> ps ) ) -> ( ph -> ps ) )
> pm2.43bgbi imidm13b $p |- ( ( ph -> ( ps -> ( ph -> ch ) ) ) <-> ( ps ->
> ( ph -> ch ) ) )
> pm2.43cbi imidm14b $p |- ( ( ph -> ( ps -> ( ch -> ( ph -> th ) ) ) )
> <-> ( ps -> ( ch -> ( ph -> th ) ) ) )
>

[...]

> a2r: reversed ax-2

ax-2 is a kind of distributive law for implication. For the
bidirectional version, some time ago I changed the name from "pm5.41" to
"imdi". Perhaps use variants of "imdi"?

> pm2.86i a2ri $e |- ( ( ph -> ps ) -> ( ph -> ch ) ) $p |- ( ph -> ( ps
> -> ch ) )
> pm2.86d a2rd $e |- ( ph -> ( ( ps -> ch ) -> ( ps -> th ) ) ) $p |- ( ph
> -> ( ps -> ( ch -> th ) ) )
> pm2.86 a2r $p |- ( ( ( ph -> ps ) -> ( ph -> ch ) ) -> ( ph -> ( ps ->
> ch ) ) )
>
> ian: and introduction

Note that jca (acronym for "join consequents with AND"), jcad, etc. are
deduction versions of pm3.2. In its comment, pm3.2 is called "join
antecedents with conjunction." Should we change jca to iand, jcad to
iandd, and so on?

Also, pm3.43 is in turn a closed theorem form of jca.

> pm3.43i animrdii $p |- ( ( ph -> ps ) -> ( ( ph -> ch ) -> ( ph -> ( ps
> /\ ch ) ) ) )
> pm3.43 animrdi $p |- ( ( ( ph -> ps ) /\ ( ph -> ch ) ) -> ( ph -> ( ps
> /\ ch ) ) )
>

[...]

>
> ebian: eliminate a hypothesis and replace with AND
> pm5.32 ebianb $p |- ( ( ph -> ( ps <-> ch ) ) <-> ( ( ph /\ ps ) <-> (
> ph /\ ch ) ) )
> pm5.32i ebianl $e |- ( ph -> ( ps <-> ch ) ) $p |- ( ( ph /\ ps ) <-> (
> ph /\ ch ) )
> pm5.32ri ebianr $e |- ( ph -> ( ps <-> ch ) ) $p |- ( ( ps /\ ph ) <-> (
> ch /\ ph ) )
> pm5.32d ebianld $e |- ( ph -> ( ps -> ( ch <-> th ) ) ) $p |- ( ph -> (
> ( ps /\ ch ) <-> ( ps /\ th ) ) )
> pm5.32rd ebianrd $e |- ( ph -> ( ps -> ( ch <-> th ) ) ) $p |- ( ph -> (
> ( ch /\ ps ) <-> ( th /\ ps ) ) )
> pm5.32da ebianla $e |- ( ( ph /\ ps ) -> ( ch <-> th ) ) $p |- ( ph -> (
> ( ps /\ ch ) <-> ( ps /\ th ) ) )
>
> ebiim: eliminate a hypothesis and replace with implies

I always think of pm5.74 as a distributive law for implication over
biconditional. Perhaps imbidi? I think of pm5.32 as kind of a
distributive law as well, where we distribute an antecedent over the
consequent using conjunction.

> pm5.74 ebiimb $p |- ( ( ph -> ( ps <-> ch ) ) <-> ( ( ph -> ps ) <-> (
> ph -> ch ) ) )
> pm5.74i ebiim $e |- ( ph -> ( ps <-> ch ) ) $p |- ( ( ph -> ps ) <-> (
> ph -> ch ) )
> pm5.74ri ebiimr $e |- ( ( ph -> ps ) <-> ( ph -> ch ) ) $p |- ( ph -> (
> ps <-> ch ) )
> pm5.74d ebiimd $e |- ( ph -> ( ps -> ( ch <-> th ) ) ) $p |- ( ph -> ( (
> ps -> ch ) <-> ( ps -> th ) ) )
> pm5.74rd ebiimrd $e |- ( ph -> ( ( ps -> ch ) <-> ( ps -> th ) ) ) $p |-
> ( ph -> ( ps -> ( ch <-> th ) ) )
> pm5.74da ebiima $e |- ( ( ph /\ ps ) -> ( ch <-> th ) ) $p |- ( ph -> (
> ( ps -> ch ) <-> ( ps -> th ) ) )

For the record, below are the pm* theorems used 10 or more times that
aren't in the above list, found with 'show usage pm*' then sorted and
edited.

Statement "pm4.56" is directly referenced in the proofs of 10 statements:
Statement "pm2.04" is directly referenced in the proofs of 11 statements:
Statement "pm3.3" is directly referenced in the proofs of 11 statements:
Statement "pm2.53" is directly referenced in the proofs of 12 statements:
Statement "pm3.22" is directly referenced in the proofs of 13 statements:
Statement "pm4.24" is directly referenced in the proofs of 13 statements:
Statement "pm3.24" is directly referenced in the proofs of 17 statements:
Statement "pm3.35" is directly referenced in the proofs of 18 statements:
Statement "pm5.5" is directly referenced in the proofs of 19 statements:
Statement "pm2.18d" is directly referenced in the proofs of 21 statements:
Statement "pm3.21" is directly referenced in the proofs of 23 statements:
Statement "pm2.01d" is directly referenced in the proofs of 31 statements:
Statement "pm2.27" is directly referenced in the proofs of 67 statements:

Note that pm4.56 is the same as ioran reversed. There are a few other
pm* that are reversals, such as oridm and pm4.25. Most of these can be
found by looking for pm* theorems that have short proofs using bicomi.
Maybe we should eliminate the pm* versions. (We would still keep the
[WhiteheadRussell] ref in the comment of the non-pm* versions.) I felt
our non-pm* version was more natural or at least in keeping with some
vague set.mm convention of having the thing you usually start with on
the lhs: for ioran we are "distributing" the -. over the lhs; for oridm
we are "eliminating" the \/ of the lhs.

BTW in case we ever need a complete list of the pm* prop calc theorems
in their original form, the page
http://us.metamath.org/mmsolitaire/pmproofs.txt provides one.

Finally, since we're on the topic, we may also want to discuss the
proposed changes at the top of set.mm:

PROPOSED:
Date Old New Notes
proposed syl imtri (analogous to *bitr*, sstri, etc.)
proposed sylib imbitri etc.
proposed sylbid biimtrd etc.
proposed sylbird biimtrrd etc.
proposed syl5* *trid (syl5bi -> biimtrid; syl5eqel ->
eqeltrid;etc.)
proposed syl6* *trdi
proposed *mpt* *mpf* or *mptf* (maps-to for functions)
proposed *mpt2* *mpo* or *mpto* (maps-to for operations)

Norm

Norman Megill

unread,

Sep 25, 2016, 3:19:38 PM9/25/16

to meta...@googlegroups.com

On 9/25/16 8:19 AM, David A. Wheeler wrote:
>
>> On Sat, Sep 24, 2016 at 8:55 PM, Norman Megill <n...@alum.mit.edu>
>> wrote:
>>> I don't remember all the 19* names either.
>
> Renaming makes sense. One request: please keep a specific citation
> to the theorem number in each comment just before the individual
> theorem. That way, it will be easy to see if a particular theorem
> from Principia Mathematica is already proved.

Don't worry, we will always keep the PM and 19* literature references in
the comment. If any are missing, we should add them. I actually plan
to use this to locate the 19.* and pm* theorems whose names I'm familiar
with, using 'search * 19. /comment', until I've gotten used to the new
names.

>
> In the long run I would like to see every theorem from PM proved in
> set.mm. Now that we can mark "don't use this later", it easy to add
> something without necessarily automatically reusing it later. I think
> of set.mm as a modern principia Mathematica... set.mm should have at
> least as much as the original.

Beyond the relatively clean prop calc theorems, the FOL and set theory
in PM may have no exact translations. Andrew Salmon's mathbox was an
attempt in this direction, but as you can see they tend to be somewhat
weird and useless, and if you compare the PM originals there was some
creativity involved (as I recall).

Set theory is problematic since in order to avoid Russell's paradox, PM
is based on a ramified theory of types and an axiom of reducibility. It
is closer to NF than ZFC. NF was actually the result of trying to
simplify PM's theory of types, so it might make more sense to add them
to the NF database. For example, to represent the number 1, PM uses the
class of all singletons, which is a proper class in ZFC.

Norm

David A. Wheeler

unread,

Sep 25, 2016, 4:18:00 PM9/25/16

to meta...@googlegroups.com, Norman Megill

>Beyond the relatively clean prop calc theorems, the FOL and set theory
>in PM may have no exact translations.

That's a fair point. However, at least the prop calc theorems could be added.

> Andrew Salmon's mathbox was an
>attempt in this direction, but as you can see they tend to be somewhat
>weird and useless, and if you compare the PM originals there was some
>creativity involved (as I recall).

I thought the statements to be proved were fairly straight translations of the originals. If not, maybe they could be updated to be that way.

Why not add a new prop calc subsection called "other PM theorems about propositional calculus" and put theorems there? They can be marked as not to be used, at least to start with, but it may turn out that some are more useful than you are expecting.

>Set theory is problematic since in order to avoid Russell's paradox, PM
>is based on a ramified theory of types and an axiom of reducibility.

I know.

Okay, modified long term goal: get all the PM theorems from propositional calculus included in set.mm.

And as separately noted, I'd also like to see Euclidean geometry and similar handled. Geometry was supposed to be Volume 4 of PM, if I recall correctly.

--- David A.Wheeler

Mario Carneiro

unread,

Sep 25, 2016, 4:29:07 PM9/25/16

to metamath

On Sun, Sep 25, 2016 at 2:39 PM, Norman Megill <n...@alum.mit.edu> wrote:

Overall, these changes are probably a good thing for future generations, but for some current users familiar with the current names it will take some adjusting. At least for me. :)

I suggest we plan to do these 1 month from now, so there is plenty of time to field suggestions and objections on this thread, and also time for users to update set.mm with their latest mathboxes before the change.

These also conflict with the *ENF old versions of theorems, so I think we should wait until the ENF update lands before enacting these.

I thought about some variation on "explosion", but the first four initial segments of that word are taken, and I didn't want to make it more complicated than that. Additionally, most logic books I've seen seem to prefer the simple naming system of "connective-E" and "connective-I" for the indroduction and elimination rules for each connective, which fits well with are general style, although most of these theorems are not named this way in set.mm.

pm2.21d enotd $e |- ( ph -> -. ps ) $p |- ( ph -> ( ps -> ch ) )
pm2.21 enot $p |- ( -. ph -> ( ph -> ps ) )
pm2.21i enoti $e |- -. ph $p |- ( ph -> ps )
pm2.24 enotr $p |- ( ph -> ( -. ph -> ps ) )
pm2.24ii enotii $e |- ph $e |- -. ph $p |- ps
pm2.24d enotrd $e |- ( ph -> ps ) $p |- ( ph -> ( -. ps -> ch ) )
pm2.24i enotri $e |- ph $p |- ( -. ph -> ps )

imidms: idempotence of implication, "s" suffix for hypothesis manipulation

pm2.43 is called "contraction" in the literature. The "c" suffix in syl*c means "syl... combined with contraction". I don't have a big objection to "imidm" but I'm mentioning it in case someone has a better idea.

How about imidm -> imc then?

pm2.43i imcs $e |- ( ph -> ( ph -> ps ) ) $p |- ( ph -> ps )
pm2.43d imc23s $e |- ( ph -> ( ps -> ( ps -> ch ) ) ) $p |- ( ph -> ( ps -> ch ) )
pm2.43a imc13s $e |- ( ps -> ( ph -> ( ps -> ch ) ) ) $p |- ( ps -> ( ph -> ch ) )
pm2.43b imc31s $e |- ( ps -> ( ph -> ( ps -> ch ) ) ) $p |- ( ph -> ( ps -> ch ) )
pm2.43 imc $p |- ( ( ph -> ( ph -> ps ) ) -> ( ph -> ps ) )
pm2.43bgbi imc31b $p |- ( ( ph -> ( ps -> ( ph -> ch ) ) ) <-> ( ps -> ( ph -> ch ) ) )
pm2.43cbi imc41b $p |- ( ( ph -> ( ps -> ( ch -> ( ph -> th ) ) ) ) <-> ( ps -> ( ch -> ( ph -> th ) ) ) )

I also fixed the numbering so that imcMN means that position N was eliminated and merged into position M (imc31d and imc31b express the same kind of contraction even though the variables are different).

a2r: reversed ax-2

ax-2 is a kind of distributive law for implication. For the bidirectional version, some time ago I changed the name from "pm5.41" to "imdi". Perhaps use variants of "imdi"?

Alright, then by the "rdi" convention you mentioned these should be "imrdi":

pm2.86i imrdii $e |- ( ( ph -> ps ) -> ( ph -> ch ) ) $p |- ( ph -> ( ps -> ch ) )
pm2.86d imrdid $e |- ( ph -> ( ( ps -> ch ) -> ( ps -> th ) ) ) $p |- ( ph -> ( ps -> ( ch -> th ) ) )
pm2.86 imrdi $p |- ( ( ( ph -> ps ) -> ( ph -> ch ) ) -> ( ph -> ( ps -> ch ) ) )

ian: and introduction

Note that jca (acronym for "join consequents with AND"), jcad, etc. are deduction versions of pm3.2. In its comment, pm3.2 is called "join antecedents with conjunction." Should we change jca to iand, jcad to iandd, and so on?

Also, pm3.43 is in turn a closed theorem form of jca.

pm3.43i animrdii $p |- ( ( ph -> ps ) -> ( ( ph -> ch ) -> ( ph -> ( ps
/\ ch ) ) ) )
pm3.43 animrdi $p |- ( ( ( ph -> ps ) /\ ( ph -> ch ) ) -> ( ph -> ( ps
/\ ch ) ) )

Actually, I think these should be "imanrdi" since in the three variable side implication is at the root. More schematically:

ABdi $p |- ( ( ph A ( ps B ch ) ) <-> ( ( ph B ps ) A ( ph B ch ) ) )
ABldi $p |- ( ( ph A ( ps B ch ) ) -> ( ( ph B ps ) A ( ph B ch ) ) )
ABrdi $p |- ( ( ( ph B ps ) A ( ph B ch ) ) -> ( ph A ( ps B ch ) ) )

thus:

pm3.43i imanrdii $p |- ( ( ph -> ps ) -> ( ( ph -> ch ) -> ( ph -> ( ps /\ ch ) ) ) )
pm3.43 imanrdi $p |- ( ( ( ph -> ps ) /\ ( ph -> ch ) ) -> ( ph -> ( ps /\ ch ) ) )

ebian: eliminate a hypothesis and replace with AND

[...]

ebiim: eliminate a hypothesis and replace with implies

I always think of pm5.74 as a distributive law for implication over biconditional. Perhaps imbidi? I think of pm5.32 as kind of a distributive law as well, where we distribute an antecedent over the consequent using conjunction.

This is a good point. How about ebianl -> anbidi and ebianr -> anbidir, and ebiim -> imbidi, ebiimr -> imbirdi.

pm5.32 anbidib $p |- ( ( ph -> ( ps <-> ch ) ) <-> ( ( ph /\ ps ) <-> ( ph /\ ch ) ) )
pm5.32i anbidi $e |- ( ph -> ( ps <-> ch ) ) $p |- ( ( ph /\ ps ) <-> ( ph /\ ch ) )
pm5.32ri anbidir $e |- ( ph -> ( ps <-> ch ) ) $p |- ( ( ps /\ ph ) <-> ( ch /\ ph ) )
pm5.32d anbidid $e |- ( ph -> ( ps -> ( ch <-> th ) ) ) $p |- ( ph -> ( ( ps /\ ch ) <-> ( ps /\ th ) ) )
pm5.32rd anbidird $e |- ( ph -> ( ps -> ( ch <-> th ) ) ) $p |- ( ph -> ( ( ch /\ ps ) <-> ( th /\ ps ) ) )
pm5.32da anbidia $e |- ( ( ph /\ ps ) -> ( ch <-> th ) ) $p |- ( ph -> ( ( ps /\ ch ) <-> ( ps /\ th ) ) )

ebiim: eliminate a hypothesis and replace with implies

pm5.74 imbidib $p |- ( ( ph -> ( ps <-> ch ) ) <-> ( ( ph -> ps ) <-> ( ph -> ch ) ) )
pm5.74i imbidi $e |- ( ph -> ( ps <-> ch ) ) $p |- ( ( ph -> ps ) <-> ( ph -> ch ) )
pm5.74ri imbirdi $e |- ( ( ph -> ps ) <-> ( ph -> ch ) ) $p |- ( ph -> ( ps <-> ch ) )
pm5.74d imbidid $e |- ( ph -> ( ps -> ( ch <-> th ) ) ) $p |- ( ph -> ( ( ps -> ch ) <-> ( ps -> th ) ) )
pm5.74rd imbirdid $e |- ( ph -> ( ( ps -> ch ) <-> ( ps -> th ) ) ) $p |- ( ph -> ( ps -> ( ch <-> th ) ) )
pm5.74da imbidia $e |- ( ( ph /\ ps ) -> ( ch <-> th ) ) $p |- ( ph -> ( ( ps -> ch ) <-> ( ps -> th ) ) )

For the record, below are the pm* theorems used 10 or more times that aren't in the above list, found with 'show usage pm*' then sorted and edited.

Taking a shot at these:

pm4.56 iorancom $p |- ( ( -. ph /\ -. ps ) <-> -. ( ph \/ ps ) )

Not seeing a big use for commuted versions of biconditionals, since we have such a large complement of theorems that apply biconditionals in either direction.

pm2.04 com12t $p |- ( ( ph -> ( ps -> ch ) ) -> ( ps -> ( ph -> ch ) ) )

pm3.3 expt $p |- ( ( ( ph /\ ps ) -> ch ) -> ( ph -> ( ps -> ch ) ) )
expt expit $p |- ( ( -. ( ph -> -. ps ) -> ch ) -> ( ph -> ( ps -> ch ) ) )

pm2.53 ort $p |- ( ( ph \/ ps ) -> ( -. ph -> ps ) )

pm3.22 ancom1 $p |- ( ( ph /\ ps ) -> ( ps /\ ph ) )

pm4.24 anidmcom $p |- ( ph <-> ( ph /\ ph ) )

pm3.24 noncon $p |- -. ( ph /\ -. ph )

noncon = Law of noncontradiction.

pm3.35 mpt $p |- ( ( ph /\ ( ph -> ps ) ) -> ps )

Modus ponens, theorem form.

pm5.5 mpb $p |- ( ph -> ( ( ph -> ps ) <-> ps ) )

Modus ponens biconditional. Not super happy with this, we should have a general name for "absorption" laws such as this one and biantrud, ibar, biorf and such.

pm2.18 npeir $p |- ( ( -. ph -> ph ) -> ph )
pm2.18d npeird $e |- ( ph -> ( -. ps -> ps ) ) $p |- ( ph -> ps )

Pierce's law for negation. (FYI this one is not intuitionistic, unlike pm2.01.)

pm3.21 iancom $p |- ( ph -> ( ps -> ( ps /\ ph ) ) )

pm2.01 inot $p |- ( ( ph -> -. ph ) -> -. ph )
pm2.01d inotd $e |- ( ph -> ( ps -> -. ps ) ) $p |- ( ph -> -. ps )

inot = not introduction

pm2.27 mpit $p |- ( ph -> ( ( ph -> ps ) -> ps ) )

mpt with implication

.

Finally, since we're on the topic, we may also want to discuss the proposed changes at the top of set.mm:

PROPOSED:
Date Old New Notes
proposed syl imtri (analogous to *bitr*, sstri, etc.)
proposed sylib imbitri etc.
proposed sylbid biimtrd etc.
proposed sylbird biimtrrd etc.
proposed syl5* *trid (syl5bi -> biimtrid; syl5eqel -> eqeltrid;etc.)
proposed syl6* *trdi

Despite the logical naming scheme, I am still of the view that these theorems are common enough that some "exceptional" naming is allowed. In particular, I would not support any name change that is longer than "syl*" are currently. Perhaps "itr" instead of "syl" is a compromise?

Mario

proposed *mpt* *mpf* or *mptf* (maps-to for functions)
proposed *mpt2* *mpo* or *mpto* (maps-to for operations)

I support this, since the "2" often conflicts with other numbers after an "mpt" theorem.

Mario

Norm

--
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+unsubscribe@googlegroups.com.
To post to this group, send email to meta...@googlegroups.com.

Norman Megill

unread,

Sep 25, 2016, 5:21:36 PM9/25/16

to meta...@googlegroups.com

On 9/25/16 4:17 PM, David A. Wheeler wrote:
>
>> Beyond the relatively clean prop calc theorems, the FOL and set
>> theory in PM may have no exact translations.
>
> That's a fair point. However, at least the prop calc theorems could
> be added.

All of the prop calc theorems are there already. Any gaps in the
numbering are the same as in PM.

I think I read somewhere that Russell had a bunch of index cards that he
used to organize the theorems. For some he added a digit to squeeze it
in like *5.501 between *5.5 and *5.53. And *5.51, *5.52 are missing in
the book, so maybe they were taken out after 5.501 was added because
they weren't needed. He just left the gaps rather than try to renumber
them all when he was finished.

I might mention that to study the pm* theorems or see which ones are
there, using the theorem list is inefficient because they are scattered
about depending on what previous theorems were needed to derive them.
Instead, the bibliographic x-ref has them all collected and placed in
order, regardless of where they exist in set.mm.

http://us.metamath.org/mpegif/mmbiblio.html

Norm

David A. Wheeler

unread,

Sep 25, 2016, 5:37:56 PM9/25/16

to meta...@googlegroups.com, Norman Megill

>All of the prop calc theorems are there already. Any gaps in the
>numbering are the same as in PM.

That's cool! Does it say that anywhere in the visible material (e.g. a section description)?

--- David A.Wheeler

Norman Megill

unread,

Sep 25, 2016, 10:15:55 PM9/25/16

to David A. Wheeler, meta...@googlegroups.com

No. I didn't think anyone was interested.

While not part of set.mm, a permanent complete list of all 193 PM prop
calc theorems, as I mentioned in another post, is held in:

http://us.metamath.org/mmsolitaire/pmproofs.txt

These show the original PM theorems unaltered, whereas the set.mm
versions occasionally have minor variations (such as swapped order of
biconditional) in order to be more practical to work with.

As for FOL, some of the more useful theorems are probably already in
set.mm. For example, *10.21 is essentially the same as 19.21v. It's a
matter of going through them carefully and adding a PM reference to the
theorem's comment, like was already done for *10.22 <-> 19.26. If
someone wants to do this, it is helpful to read "The Notation in
Principia Mathematica":

http://plato.stanford.edu/entries/pm-notation/

The first edition of PM Vol. 1 is public domain and easy to find in PDF
form. AFAIK the 2nd edition did not add or delete any of the main prop
calc and FOL theorems but fixed some typos.

The 2nd edition of Vol. 1, which is still under copyright and thus hard
to find, added Appendix A which proposed to replace the axioms with an
axiomatization using Nicod's axiom for the Sheffer stroke (NAND gate).
Russell was apparently enamored with this because it showed the adequacy
of a single connective and a single axiom, which was unknown at the time
of the first edition. It never caught on, maybe because theorems
expressed with Sheffer stroke notation are hard to read. In set.mm, the
equivalence of Nicod's axiom/rule and our standard ax-1,2,3.mp (via
luk-1,2,3) is shown starting at theorem nic-dfim.

Norm

David A. Wheeler

unread,

Sep 26, 2016, 5:35:38 PM9/26/16

to Norman Megill, metamath

> >> All of the prop calc theorems are there already. Any gaps in the
> >> numbering are the same as in PM.
> >
> > That's cool! Does it say that anywhere in the visible material (e.g. a section description)?

On Sun, 25 Sep 2016 22:15:52 -0400, Norman Megill <n...@alum.mit.edu> wrote:
> No. I didn't think anyone was interested.

I'm interested. I think it'd be important to ensure that set.mm includes all the PM
prop calc and FOL theorems.

There should be a mapping somewhere listing PM theorems and their
set.mm names. I think it should be somewhere in set.mm itself, so that
theorem renames are cleanly handled. E.g., there might be a section on
"PM propositional calculus", where the section text shows the mappings,
and the section contents include the "left over theorems" if they've not
been proved elsewhere.

> While not part of set.mm, a permanent complete list of all 193 PM prop
> calc theorems, as I mentioned in another post, is held in:
>
> http://us.metamath.org/mmsolitaire/pmproofs.txt

Those focus on proofs using "only the axioms". Would it be interesting to
include both "normal" proofs and "proofs that only directly use axioms"?
If so, there might need to a naming convention for "proofs only directly using axioms"
(I think there are already some in set.mm).

> These show the original PM theorems unaltered, whereas the set.mm
> versions occasionally have minor variations (such as swapped order of
> biconditional) in order to be more practical to work with.

I think it's reasonable to accept minor variations as "essentially the same".

...

> The first edition of PM Vol. 1 is public domain and easy to find in PDF
> form. AFAIK the 2nd edition did not add or delete any of the main prop
> calc and FOL theorems but fixed some typos.
>
> The 2nd edition of Vol. 1, which is still under copyright and thus hard
> to find, added Appendix A which proposed to replace the axioms with an
> axiomatization using Nicod's axiom for the Sheffer stroke (NAND gate).
> Russell was apparently enamored with this because it showed the adequacy
> of a single connective and a single axiom, which was unknown at the time
> of the first edition. It never caught on, maybe because theorems
> expressed with Sheffer stroke notation are hard to read. In set.mm, the
> equivalence of Nicod's axiom/rule and our standard ax-1,2,3.mp (via
> luk-1,2,3) is shown starting at theorem nic-dfim.

Those are good reasons for generally preferring the first edition over the
second. That preference should be documented somewhere in set.mm, so that people
will know that.

--- David A. Wheeler

fl

unread,

Sep 27, 2016, 10:34:30 AM9/27/16

to Metamath, n...@alum.mit.edu, dwhe...@dwheeler.com

I also think it is important to keep track of history's most influential formal systems. Even if Whitehead and Russel's system

is no longer in use, it is however this system that gives to Curry the idea of his simply typed lambda calculus. It is also what

Gödel had in mind when he made his incompletness theorem.

I think that PM can be translated into metamath. It is an Hilbert system. The problem as usual is translating

the free variables into distinct ones.

Translating PM would help to understand precisely what have been the improvements made by Curry in the system of type.

(A question. Peano in *Arithmetices Principia* has given a long list of propositional and predicate calculus. (No axioms and

no proofs if I recall correctly. I just wonder if this is the source (at least partial) for Russel's work on propositional and

predicate calculus. The two lists would deserve to be compared.)

(A second observation. Normally to explain the title of *Principia Mathematica*, one refers to Newton.

But it just comes to my mind, that it is a reference to Peano as well.)

--

FL

David A. Wheeler

unread,

Sep 27, 2016, 1:49:50 PM9/27/16

to metamath, Metamath, nm

On Tue, 27 Sep 2016 07:34:29 -0700 (PDT), "'fl' via Metamath" <meta...@googlegroups.com> wrote:
> I also think it is important to keep track of history's most influential

> formal systems....
> I think that PM can be translated into metamath...

I agree, but currently my sights are more set on getting the propositional calculus subset
(and maybe the predicate calculus subset) pulled into set.mm.

--- David A. Wheeler

Cris Perdue

unread,

Sep 27, 2016, 9:45:03 PM9/27/16

to meta...@googlegroups.com

Beyond the relatively clean prop calc theorems, the FOL and set theory in PM may have no exact translations. Andrew Salmon's mathbox was an attempt in this direction, but as you can see they tend to be somewhat weird and useless, and if you compare the PM originals there was some creativity involved (as I recall).

Set theory is problematic since in order to avoid Russell's paradox, PM is based on a ramified theory of types and an axiom of reducibility. It is closer to NF than ZFC. NF was actually the result of trying to simplify PM's theory of types, so it might make more sense to add them to the NF database. For example, to represent the number 1, PM uses the class of all singletons, which is a proper class in ZFC.

Norm

Some thoughts: Grouping theorems from PM with NF would be unorthodox, based on NF having a universal set and omitting specific types; also unusual compared with any accounts I have read.

Simple type theory of the Church variety (e.g. Peter Andrews, 2002) was also the result of trying to simplify PM's theory of types, and successful in avoiding paradoxes. Andrews' type theory in a sense allows a description of all singletons, though through type parameters, which are really metalinguistic. In proof assistants of the HOL family however, type parameters are part of the language, so the collection of all singletons of all types can be described in the language. Perhaps PM set theory could be grouped together with simple type theory.

I was able to find an article by Godel on Russell's logic, which might be of some interest:

https://books.google.com/books?id=lgDGTYNcOY4C&pg=PA119#v=onepage&q&f=false

Godel seems to claim that the axiom of reducibility is violated by the actual development of mathematics in PM.

fl

unread,

Sep 28, 2016, 6:52:16 AM9/28/16

to Metamath, n...@alum.mit.edu, dwhe...@dwheeler.com

I also think it is important to keep track of history's most influential formal systems. Even if Whitehead and Russel's system
is no longer in use, it is however this system that gives to Curry the idea of his simply typed lambda calculus.

... that gave to Church etc.

--

FL

David A. Wheeler

unread,

Sep 30, 2016, 4:51:24 PM9/30/16

to Norman Megill, metamath

On Sun, 25 Sep 2016 22:15:52 -0400, Norman Megill <n...@alum.mit.edu> wrote:

> On 9/25/16 5:37 PM, David A. Wheeler wrote:
> >
> >> All of the prop calc theorems are there already. Any gaps in the
> >> numbering are the same as in PM.
> >
> > That's cool! Does it say that anywhere in the visible material (e.g. a section description)?
>
> No. I didn't think anyone was interested.

I'm interested!

> While not part of set.mm, a permanent complete list of all 193 PM prop
> calc theorems, as I mentioned in another post, is held in:
>
> http://us.metamath.org/mmsolitaire/pmproofs.txt

Very nice. I did a cross-check (see below) between that file & set.mm, just to make sure
there was no accidental omission.
Set.mm also includes *2.33, but that's a definition. It's awesome that
set.mm seems to include all the prop calculus axioms/theorems/definitions from PM
(assuming pmproofs.txt isn't missing anything). Now that just needs to be documented :-).

I'm going to push the following to the propositional calculus section comment (develop branch).
It's an interesting factoid that wasn't documented, and this fixes it:

+ All 193 axioms, definitions, and theorems for propositional calculus in
+ _Principia Mathematica_ (specifically *1.2 through *5.75) are
+ axioms or formally proven. See the Bibliographic Cross-References
+ at ~ mmbiblio.html for a complete cross-reference from sources used
+ to its formalization in the Metamath Proof Explorer.

Obviously please do adjust to taste. It's easier to move information around
once it's written in the first place :-).

It appears that the version that's been consistently referenced (at least here) is
"Principia Mathematica to *56", which is much *newer*. But that may be actually
easier to get, so that makes sense to me.

One oddity: the sort order in the Bibliographic Cross-References shows *1.2
after *1.4. You might want to use "natural sort" (in a natural sort, when comparing digits,
you group them & sort them numerically); see https://en.wikipedia.org/wiki/Natural_sort_order

--- David A. Wheeler

P.S. I verified that the prop calculus information was in set.mm by doing this:

# List all the *names in pmproofs.txt:
grep -Eo ' \*[0-9.]+' pmproofs.txt | sed 's/^ //' | sort -n | uniq > pmproof-numbers.txt
# Same for mmbiblio.html (if it's not in mmbiblio, maybe set.mm wasn't formatted correctly):
grep -Eo ' \*[0-9.]+' mmbiblio.html | sed 's/^ //' | sort -n | uniq > mmbiblio-numbers.txt
diff -u pmproof-numbers.txt mmbiblio-numbers.txt

David A. Wheeler

unread,

Sep 30, 2016, 5:18:25 PM9/30/16

to metamath, Norman Megill, metamath

On Fri, 30 Sep 2016 16:51:21 -0400 (EDT), "David A. Wheeler" <dwhe...@dwheeler.com> wrote:
> + All 193 axioms, definitions, and theorems for propositional calculus in
> + _Principia Mathematica_ (specifically *1.2 through *5.75) are
> + axioms or formally proven. See the Bibliographic Cross-References
> + at ~ mmbiblio.html for a complete cross-reference from sources used
> + to its formalization in the Metamath Proof Explorer.

Pushed, but with a correction: The count is 194 (because set.mm includes definition *2.33).

--- David A. Wheeler

Norman Megill

unread,

Oct 1, 2016, 5:27:15 PM10/1/16

to dwhe...@dwheeler.com, metamath

On 9/30/16 4:51 PM, David A. Wheeler wrote:

> One oddity: the sort order in the Bibliographic Cross-References shows *1.2
> after *1.4. You might want to use "natural sort" (in a natural sort, when comparing digits,
> you group them & sort them numerically); see https://en.wikipedia.org/wiki/Natural_sort_order

Natural sort order is already used. This glitch is caused because *1.2
is called "*1.2 (Taut)", which acts like a very big number (since the
software tolerates non-digits in the numbering). I will take off the
"(Taut)" part from the theorem number and put it elsewhere in the
comment, so that this item will be sorted correctly.

The Bibliographic Cross-References entries are sorted by author, then by
page, then by theorem number on that page. The page and theorem number
sorts use natural order, meaning they are padded with leading spaces so
that they are right-justified before sorting. While this algorithm
isn't perfect, it works 99% of the time. It didn't seem to be worth the
effort to divide the theorem number into numeric/non-numeric subfields
with natural/alphabetic sub-sorts applied respectively. In any case,
the number of theorems on one page is usually small so that all of them
can be seen simultaneously, and any out-of-order glitches like "*1.2
(Taut)" will still be easily noticed.

Actually, PM is peculiar in that it does _not_ use natural sort order
for the number after the decimal point. As an example, Theorem *2.3
comes after Theorem *2.21 in the PM book. Almost all other books would
have *2.3 before *2.21, and that is the sorting order I chose for the
bib xref. I don't think it is worth the extra code complexity to make a
special case for PM, and anyway it is probably better to have them
(incorrectly) sorted in natural order since that is what most people
expect if they aren't familiar with PM.

Norm

David A. Wheeler

unread,

Oct 2, 2016, 7:31:37 AM10/2/16

to Norman Megill, metamath

>Natural sort order is already used. This glitch is caused because *1.2
>is called "*1.2 (Taut)", which acts like a very big number (since the
>software tolerates non-digits in the numbering).

The space should still end the number in a natural sort. I think it's a sort bug.

>The Bibliographic Cross-References entries are sorted by author, then by
>page, then by theorem number on that page.

Very sensible.

> The page and theorem number
>sorts use natural order, meaning they are padded with leading spaces so
>that they are right-justified before sorting.

?

We nay be using the phrase "natural sort" with different definitions. I mean this:
https://en.m.wikipedia.org/wiki/Natural_sort_order
Where digits are compared they are grouped and compared as integers.

So you should see this:
1.2
1.2 taut
1.3
1.21

>Actually, PM is peculiar in that it does _not_ use natural sort order
>for the number after the decimal point. As an example, Theorem *2.3
>comes after Theorem *2.21 in the PM book.

That IS weird.

> I don't think it is worth the extra code complexity to make
>a
>special case for PM, and anyway it is probably better to have them
>(incorrectly) sorted in natural order since that is what most people
>expect if they aren't familiar with PM.

Makes sense. The page# sort should help a lot anyway.

--- David A.Wheeler

Norman Megill

unread,

Oct 2, 2016, 12:07:14 PM10/2/16

to meta...@googlegroups.com

On 10/2/16 7:31 AM, David A. Wheeler wrote:
>
>> Natural sort order is already used. This glitch is caused because *1.2
>> is called "*1.2 (Taut)", which acts like a very big number (since the
>> software tolerates non-digits in the numbering).
>
> The space should still end the number in a natural sort. I think it's a sort bug.

It isn't a bug in the usual sense, because that is the way it was
purposely designed. To simplify the code, it assumes that the theorem
number is a number, which it is almost all of the time.

The "(Taut)" shouldn't be there, because it isn't a number. The code
tolerates things that are not numbers without producing annoying warning
messages, but the sorting on a given page may or may not be what one
expects. I don't think this is a big deal because the number of
theorems on a given page is almost always tiny and easy to see all at
once, and in any case the sort is correct as long as the theorem numbers
are numbers, which they almost always are.

Of course the code can be changed, but moving "(Taut)" outside of the
bib reference will also fix it. This is a minor cosmetic issue that
rarely occurs and is usually easy to fix in the set.mm comment, and I'm
not sure if it is worth the trouble of changing the code. I added a
note to my to-do list to look at this, but it may be a while before I
get to it. Perhaps I'll write a general-purpose function that creates a
true natural sort key, given any character string along with an integer
specifying maximum field width.

>
>> The Bibliographic Cross-References entries are sorted by author, then by
>> page, then by theorem number on that page.
>
>
> Very sensible.
>
>> The page and theorem number
>> sorts use natural order, meaning they are padded with leading spaces so
>> that they are right-justified before sorting.
>
> ?
>
> We nay be using the phrase "natural sort" with different definitions. I mean this:
> https://en.m.wikipedia.org/wiki/Natural_sort_order
> Where digits are compared they are grouped and compared as integers.
>
> So you should see this:
> 1.2
> 1.2 taut
> 1.3
> 1.21

You are correct, when the theorem number is not a number, then the
sorting is not a natural sort. The code was written to assume the
theorem number is number, and when it is, it is a natural sort.

The software does not treat "(Taut)" as a separate field but as part of
the theorem number, including the space. That is how the software is
designed right now, with only one field to hold the theorem number.
Taking out the "(Taut)" will fix the problem.

>
>
>> Actually, PM is peculiar in that it does _not_ use natural sort order
>> for the number after the decimal point. As an example, Theorem *2.3
>> comes after Theorem *2.21 in the PM book.
>
> That IS weird.

Yes and no. It allowed inserting new theorems without having to
renumber everything, which was very laborious in pre-computer days for a
work of that complexity. For example, *2.5, *2.51, *2.52, and *2.521
all resemble each other. I would guess that *2.521 was added later, and
the extra digit allowed it to be inserted before *2.53 (which has a
different general pattern). It would be interesting to see if there is
a correlation between the number of digits and how far into the book the
theorem is first referenced.

So if we treat the theorem numbers as simply decimal numbers rather than
<chapter>.<sequence number>, they sort correctly.

I think it is a good thing that they went to the trouble of organizing
the theorems in logical groups rather than just adding them sequentially
as they were needed. Not having sequential integers after the decimal
point seems like a reasonable compromise given that computers didn't exist.

I can't imagine the difficulty of creating PM without a computer, always
worrying that some tiny mistake would make the whole thing collapse.
Russell himself said, "...my intellect never quite recovered
from the strain of writing Principia Mathematica. I have been ever
since definitely less capable of dealing with difficult abstractions
than I was before" (The Autobiography of Bertrand Russell, the Early
Years, p. 143.). [OTOH the long hours I have spent with Metamath have
definitely improved my math ability. I think the feedback of seeing my
work verified with 100% rigor makes a huge difference. There is also my
optimism, warranted or not, that it will never become obsolete but will
be a permanent contribution to human knowledge, hopefully lasting in one
form or another for generations beyond me. Maybe I'm wrong, but deep
down I "know" that it is the right approach to formalizing math. AFAIK
it is the only proof language that can express FOL and ZFC exactly, with
no compromises, with complete, fine-grained control over the axioms, and
with proofs that humans can in principle easily verify by hand. For me
that is a strong motivation. And it is amazing to me, and very
rewarding, to see what Mario and others have accomplished with it in the
last couple of years.]

Norm

fl

unread,

Oct 3, 2016, 7:22:46 AM10/3/16

to meta...@googlegroups.com

"...my intellect never quite recovered
from the strain of writing Principia Mathematica. I have been ever
since definitely less capable of dealing with difficult abstractions
than I was before" (The Autobiography of Bertrand Russell, the Early
Years, p. 143.).

The quotation is famous but curious. It gives the impression that the

brain is a muscle. It is not exactly that. Some people have suffered from depression

after an intellectual work. It was the case of one of Mizar's developpers

if I recall well. He ended up in a

hospital. But it doesnt appear that Russel was ever depressive.

Or it means that he was fed up with all these tiny details.

Russel's autobiography is a masterpiece. I often regret that mathematicians or

other scholars never keep a diary of their intellectual life: their problems, projects,

difficulties, successes and so on and even of their intellectual social life

(readings, conversations...)

If we had Pnueli's diary for instance...

--

FL

fl

unread,

Oct 4, 2016, 5:35:53 AM10/4/16

to Metamath

And it is amazing to me, and very
rewarding, to see what Mario

and others

have accomplished with it in the
last couple of years.]

By the way, in the definition of derivative given by Mario Carneiro

http://us2.metamath.org:88/mpegif/df-dv.html

Is it possible to make an aknowledgement to my own older work.

http://us2.metamath.org:88/mpegif/df-der.html

Something like:

(Contributed by FL, 29-May-2014.)

(Modified by Mario Carneiro, 7-Aug-2014.)

--

FL

fl

unread,

Oct 5, 2016, 4:55:33 AM10/5/16

to Metamath

Is it possible to make an aknowledgement to my own older work.

I think it would be fairer.

--

FL

fl

unread,

Oct 6, 2016, 7:33:45 AM10/6/16

to Metamath

By the way, in the definition of derivative given by Mario Carneiro

http://us2.metamath.org:88/mpegif/df-dv.html

Is it possible to make an aknowledgement to my own older work.

http://us2.metamath.org:88/mpegif/df-der.html

I know that it hasn't drawn the attention of the grand jury contrary to the work

of my opponent but well it had been designed with love, care and patience

and maybe it deserves a little mention.

(Nothing very important you know. Something unobstrusive.)

--

FL

Reply all

Reply to author

Forward