Hello / Contributing? / Matiyasevich's theorem

[Stefan O'Rear]

Hello all.  A couple months ago I was bitten by the formal math bug, downloaded Metamath and have since been trying to prove the Davis-Putnam-Robinson-Matiyasevich theorem (a set of integers is definable by a Diophantine equation system iff it is recursively enumerable).  I feel now like I've got something to share and solicit public opinions on, but I am not clear on what the procedures are in this community for doing that.  There seem to be a number of active contributors to set.mm but I don't see the channel where contributions are being made, nor for that matter do I know whether what I have is the kind of thing that belongs in set.mm.

Given the lack of any discussions of this sort in the last year, I doubt that this is the correct place to discuss developments like this.  However, I have failed to find any obviously more appropriate place.

I have tentatively published my current work along with a revision history at https://raw.githubusercontent.com/sorear/metamath-stuff/master/dprm.mm.  I have just finished adding descriptions and section headers to everything still in use.  The current frontier of development is ~ jm2.27dioph , showing that the sequence of solutions to a Pell equation is a Diophantine set.  There are a number of lemmas capable of standing alone in that file; the most significant is probably ~ irrapx1 (Lagrange's classical theorem that every irrational number has infinitely many close rational approximations, for a specific sense of "close").

Many of these results contain inadvertent uses of mathboxes, mostly due to IMPROVE ALL; I intend to clean that up at some point.  The use of ~ qredeu is very much deliberate though.  There are also a number of old results with very clumsy proofs due to not understanding how to use things like explicit substitutions.

Thoughts?  Pointers to better fora?

[Mario Carneiro]

Hi Stefan,

Although some of this is best answered by Norm, I can answer a few of these questions.

First of all, the primary avenue of communications among myself and the other active contributors is generally by direct email; this has the unfortunate side effect that the forum often doesn't get too much traffic, although I'm sure there are many eyes on it. If you talk to Norman Megill <n...@alum.mit.edu> he can get a mathbox set up for you, and you can submit your mathbox updates by just emailing it to him.

Uses of mathboxes is totally fine, but it's important to know what uses what so that we can import theorems that are needed by several mathboxes into the global namespace.

I'll need to look over your work in more detail later (and it will be easier to do this once your mathbox is in set.mm), but from what I can tell there is some good stuff in there. The work on Diophantine approximation definitely caught my eye; it's not too far from Liouville's Theorem, which is one of my 100 goals. (If you prove this one yourself you can get a mention at http://www.cs.ru.nl/~freek/100/ .)

Stylistically, it would help if you formatted your theorems the same way as set.mm, in particular regarding the 79-character line limit and theorem commenting. Much of this will be dealt with automatically by metamath's source rewrap command (which is run on the public version of set.mm), but IMO it mangles the formatting of theorem statements when it has to force a line wrap, so I prefer to format it myself so that it doesn't need to. Theorem comments and dates are mandatory; if you don't metamath will put a "PUT DESCRIPTION HERE" comment instead.

Also, if you haven't yet be sure to try out mmj2, the proof assistant for metamath with a GUI and lots of nice step proving and formatting features (for which I am a main developer).

Congratulations on this much successful work! I look forward to your future theorems, and it's always nice to see a new contributor.

Mario Carneiro

--
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 http://groups.google.com/group/metamath.
For more options, visit https://groups.google.com/d/optout.

[n...@alum.mit.edu]

Hi Stefan,

It looks like you've done some impressive work.  When you are ready,
send me an email with a link to the latest version, and I will create a
mathbox for you in the official set.mm.

Mario did a good job of answering most of your questions. Here are some
additional comments.

>     Many of these results contain inadvertent uses of mathboxes, mostly
>     due to IMPROVE ALL; I intend to clean that up at some point.  The
>     use of ~ qredeu is very much deliberate though.  There are also a
>     number of old results with very clumsy proofs due to not
>     understanding how to use things like explicit substitutions.

Yes, other mathbox references should be removed unless you think the
theorem would be generally beneficial for the main part of set.mm.  In
that case, let me know and I can move it up out of the mathbox.

To avoid this problem in the future, you can use a modified set.mm with
mathboxes removed.  You've probably figured that out already.

On my to-do list is to have the 'improve' command avoid other mathboxes
unless explicitly told, like the 'minimize_with' command does now, so
eventually this won't be a problem anymore.

I moved ~ qredeu up to the main part of set.mm, in the 13-Oct-2014
version that you can download from
http://us2.metamath.org:88/mpegif/mmrecent.html .

On proof size:  While there is no hard and fast rule for the maximum
size of a proof, I prefer proofs that compress in under a second using
'save proof xxx /compressed' in the metamath program, in order to make
my routine maintenance of set.mm easier.  If it takes longer than that,
you can break up the proof into two or more smaller lemmas.

(Mario Carneiro wrote:)

> Stylistically, it would help if you formatted your theorems the same way
> as set.mm, in particular regarding the 79-character line
> limit and theorem commenting. Much of this will be dealt with
> automatically by metamath's source rewrap command (which is run on the
> public version of set.mm), but IMO it mangles the
> formatting of theorem statements when it has to force a line wrap,

Yes, it mangles the formatting.  In a too-long line in a $a/$p/$e
statement, 'write source .../rewrap' simply inserts a new-line at the
last space that doesn't exceed the 79-character limit.  (I could take
this out, but I put it in because it started to take too much time
fixing people's submissions, where that's all I'd do anyway if I was in
a hurry.)  So, you should format it by hand as you want it to appear
within that limit.  There isn't any fixed convention for this
formatting, although I like to break at major connectives such as ->,
<->, =, with the connective starting the next line and indented per the
nesting level inside the wff.

BTW the wrapping width of 'write source .../rewrap' is controlled by the
last 'set width' command.  If you 'set width 9999', comments will be
unwrapped, which some people may prefer for editing convenience, then
they can be rewrapped with the default 'set width 79' for the final
release.  Note that only the comment immediately preceding a $p or $a
statement is rewrapped, and only that comment is displayed on the
web pages.

Norm

[David A. Wheeler]

Welcome! I thinnk it is easier to develop proofs using mmj2. You might find my Youtube video helpful:

http://m.youtube.com/watch?v=Rst2hZpWUbU

--- David A.Wheeler

[n...@alum.mit.edu]

On Monday, October 13, 2014 10:34:03 PM UTC-4, n...@alum.mit.edu wrote:

    (Mario Carneiro wrote:)
    > Stylistically, it would help if you formatted your theorems the same way
    > as set.mm, in particular regarding the 79-character line
    > limit and theorem commenting. Much of this will be dealt with
    > automatically by metamath's source rewrap command (which is run on the
    > public version of set.mm), but IMO it mangles the
    > formatting of theorem statements when it has to force a line wrap,

    Yes, it mangles the formatting.  In a too-long line in a $a/$p/$e
    statement, 'write source .../rewrap' simply inserts a new-line at the
    last space that doesn't exceed the 79-character limit.

I'll have the program issue a warning when this happens, so the user will know to review it.

Norm

[Stefan O'Rear]

First I'd like to thank everyone for the quick and warm welcome.  Glad to see my concerns about going public were unfounded.  Now for all of the process questions I didn't want to ask completely cold. :)

I'll definitely be checking out mmj2.  I have indeed been using the built-in proof assistant, and learning as I go.

Mario: Liouville's theorem (presumably you mean ~ aaliou ) indeed looks like a nice one.  I might give that a try later.

Do we have a list of surface syntax conventions to follow, beyond those that are enforced by rewrap?  I found a description of the section break comment syntax hidden in "HELP TEX".  I've been breaking after connectives — I'll switch to before for consistency.

On Monday, October 13, 2014 7:34:03 PM UTC-7, n...@alum.mit.edu wrote:

It looks like you've done some impressive work.  When you are ready,
send me an email with a link to the latest version, and I will create a
mathbox for you in the official set.mm.

What constitutes ready in this case?  I expect that late next week or so I'll be revisiting most of the old proofs to remove mathboxes and apply any "lessons learned".  Would after that be a good point?

(So far, I have basically not touched working proofs.  If it verifies and the statement is correct, I've left it be.  This will be changing soon.)

Looking at the revision log in set.mm, it seems like active contributors feed their changes back every couple weeks.  Is that a good model to follow?

How do you all manage your changes that haven't been fed back?  Do you just have a modified copy of set.mm?  I started a new file with $[ set.mm $] at the top, and I've been keeping that open in a text editor since it's substantially smaller than set.mm.  Relatedly, I have not been using WRITE SOURCE in my process; proofs just get copied and pasted out (and occasionally into the wrong theorems, with hilarious results).  I've been keeping said file in version control locally so I can revert anything I damage, and running a V P * before every commit to catch blatant editing errors.  (The other reason I have a split out file is that git has issues with repeated small edits to multi-megabyte files like a copy of set.mm would be.)

If you use modified set.mms, what's the standard practice for updating them when they change upstream?  

Something else I haven't come to a satisfactory opinion on is naming, especially for definitions.  I feel rather dirty claiming three-letter names like rmX and rmY in a global namespace like we have for constants.  None of my names are very long because typing them would get annoying quickly, but many of them are rather cryptic (would you have any idea what a Pell14QR is?  The set of solutions of a Pell equation coded as reals and restricted to the right half-plane, i.e. quadrants 1 and 4.)  I could probably be using the temporary definition idiom (I mean things like the $e statement ~ vitali.1 ; is there another name for this?) much more than I am, but there are also case where it doesn't seem to apply.  What can be said about community best practices for naming concepts and the responsible use of the global namespace?

 

On proof size:  While there is no hard and fast rule for the maximum
size of a proof, I prefer proofs that compress in under a second using
'save proof xxx /compressed' in the metamath program, in order to make
my routine maintenance of set.mm easier.  If it takes longer than that,
you can break up the proof into two or more smaller lemmas.

I can't tell if this is in response to something specific, so some general thoughts.  My prejudice is that if (after set w 79; sh n/c) the proof is taller than it is wide, it's too long.  I've noticed that the proof assistant becomes quite sluggish around 30k uncompressed steps, which has happened twice so far and resulted in an immediate sidetrack to look for places to split.  I'll apply the compression-time heuristic from now on as well.

I seem to have a particular problem with proofs that rely heavily on algebraic manipulation.  I don't suppose you know any magic bullets for those.  (I do have an idea I've been exploring, but it involves a change to ~ df-op and that's probably overstepping my bounds as a newbie juuuust a tad.)

Hopefully this isn't too many questions for today.  Part of my motivation for asking all this here is so that the answers are openly visible for the next person to come along.  (One last: How do you pronounce Megill?)

Cheers and thanks again. -sorear.

[Mario Carneiro]

Hi Stefan,

On Wed, Oct 15, 2014 at 4:05 AM, Stefan O'Rear <stef...@cox.net> wrote:

Mario: Liouville's theorem (presumably you mean ~ aaliou ) indeed looks like a nice one.  I might give that a try later.

Ah, yes, I forgot that I'd already written out the statement. Of course you can change it if you find it easier to state another way.
 

Do we have a list of surface syntax conventions to follow, beyond those that are enforced by rewrap?  I found a description of the section break comment syntax hidden in "HELP TEX".  I've been breaking after connectives — I'll switch to before for consistency.

This is mostly "play-by-ear", I'd say - the 20000 examples in set.mm should give you a good idea of how all the usual formatting issues are resolved. As for line breaks before/after connectives, I usually break before, but there are some that break after, and they both read well so it's not so important. I wouldn't say that the formatting of formulas is strict enough to write a program for - we just want to avoid long blocks of text with 6 automatic line breaks in them, cause that's impossible to read. (And there are some who make those kind of theorems...)

Actually, I will usually copy a nearby theorem as a template whenever I create a new one - this is a simple way to make sure you have all the components, in the right order (scope bracket, DJ vars, hyps, thm comment, statement, proof block, date comment, end bracket) and with proper line length. (My editor also has a line at 80 chars, which helps.)

 

What constitutes ready in this case?  I expect that late next week or so I'll be revisiting most of the old proofs to remove mathboxes and apply any "lessons learned".  Would after that be a good point?

This is entirely up to your own schedule. I think of it like releasing new versions of an application - maybe it's a big release, and you want to get everything together at once, or maybe it's just a bugfix or incremental addition, and you want to get it out as soon as you have an integer number of theorems in your file. As long as it compiles with no errors and the style is decent (and even if it's not this is fixable), it's acceptable - it's your mathbox, after all. (One possible thing to note is that complete theorems which rely on other incomplete theorems are not acceptable, because you can't compile the incomplete theorem. Doesn't mean you can't commit it anyway, though - just comment it out until you are ready, as with aaliou.)

 

(So far, I have basically not touched working proofs.  If it verifies and the statement is correct, I've left it be.  This will be changing soon.)

I think you will find mmj2 useful for shortening proofs manually (although the MM-PA minimize command is one of the primary features that is not present in mmj2). Of course, this is not an essential operation, but if you think of a shorter way to derive a theorem, go for it - that's a standing goal in set.mm.

 

Looking at the revision log in set.mm, it seems like active contributors feed their changes back every couple weeks.  Is that a good model to follow?

My own preference is to submit once I have a "substantial" amount of work to commit, something that interested people would want to take note of, rather than a more continuous stream (which I think Norm might prefer, but don't quote me). It's also less work for the maintainer, unless the commit gets so large that merges become a problem.

 

How do you all manage your changes that haven't been fed back?  Do you just have a modified copy of set.mm?  I started a new file with $[ set.mm $] at the top, and I've been keeping that open in a text editor since it's substantially smaller than set.mm.  Relatedly, I have not been using WRITE SOURCE in my process; proofs just get copied and pasted out (and occasionally into the wrong theorems, with hilarious results).  I've been keeping said file in version control locally so I can revert anything I damage, and running a V P * before every commit to catch blatant editing errors.  (The other reason I have a split out file is that git has issues with repeated small edits to multi-megabyte files like a copy of set.mm would be.)

Although I may be a special case because I do a lot of work in main set.mm, I work directly out of a modified copy of set.mm. This also doesn't break the metamath program's rewrite ability (which will expand out any includes), although generally I do set.mm modifications directly with a text editor, copying completed proof blocks from mmj2. If my commit is restricted to my mathbox, I will just copy it into a file to send it, even if I am working in place. You could also relocate your mathbox to the beginning if you want to force avoid mathboxes, or at the end if you want to have them all available in case you find something you like and edit it out or mark it for importation later.

 

If you use modified set.mms, what's the standard practice for updating them when they change upstream?

I use git version control to manage merges from the master copy. Git is great even for dealing with a single large file, and the tools all work just as well as for a many-file source code project. You can see my repo here [https://github.com/digama0/set.mm/commits/exp] - if you want you could even contribute on the same repo. I don't think Norm uses Git - he just keeps a history of dated versions of set.mm - so my approach is to prepare a submission by downloading the latest master copy, adding it to my master branch, then switching to the experimental branch and merge/rebase onto master, and send the merged file to Norm. That way he doesn't have to do anything but just update the master copy. The low tech version, which usually works fine for mathbox-localised changes, is to replace your own version of set.mm with the latest immediately before submission to make sure that upstream updates don't break your mathbox (and if they do, fix them), and then send the revised mathbox.

 

Something else I haven't come to a satisfactory opinion on is naming, especially for definitions.  I feel rather dirty claiming three-letter names like rmX and rmY in a global namespace like we have for constants.  None of my names are very long because typing them would get annoying quickly, but many of them are rather cryptic (would you have any idea what a Pell14QR is?  The set of solutions of a Pell equation coded as reals and restricted to the right half-plane, i.e. quadrants 1 and 4.)  I could probably be using the temporary definition idiom (I mean things like the $e statement ~ vitali.1 ; is there another name for this?) much more than I am, but there are also case where it doesn't seem to apply.  What can be said about community best practices for naming concepts and the responsible use of the global namespace?

So this is a bit of an unusual approach by comparison to some other proof languages, but here we prefer not to make definitions unless there is a clear benefit in terms of size or if the definition is very common or has lots of things that derive from it. There's no need to make the definition describe everything about what it means - that's what the definition comment is for. Definition symbols should be short, and so should definition labels - pick a short string to represent your definition and use it in all theorems which contain the definition and are about it in some way. For your example, I would call the constant "Pell" and the label "pell", meaning that you would have theorems like "cpell" (Pell is a class), "df-pell" (the definition of Pell), "ispell" (expand out any quantifiers and make a class-form version of df-pell), "pellre" (a Pell number is a real number), or similar names (I'm making this up without a clear idea of what theorems you have, but it's along those lines). Don't worry about potentially overlapping with some other "pell" concept or something that also happens to be called "pell" - there's nothing like that right now, and if the need arises in the future we can disambiguate them then, with an eye for what is what so that the new names are still intelligent and short.

You mentioned "temporary definitions" or "long-lived hypotheses", and indeed this is another common way to avoid having to make a definition. If your pell concept, in your opinion, is unlikely to have general applicability beyond the lemma you are trying to prove, I would make it a long-lived hypothesis instead. You can see other examples of this pattern in qrng.q and 4sq.1. (4sq also gives an example of a definition df-gz that I chose *not* to make temporary even though it was only invented for 4sq, because I anticipated that it would have general applicability.) Since definitions involve a lot of overhead in the form of theorems for equality or elementhood and the like, we try to avoid it unless necessary.

 

 

On proof size:  While there is no hard and fast rule for the maximum
size of a proof, I prefer proofs that compress in under a second using
'save proof xxx /compressed' in the metamath program, in order to make
my routine maintenance of set.mm easier.  If it takes longer than that,
you can break up the proof into two or more smaller lemmas.

I can't tell if this is in response to something specific, so some general thoughts.  My prejudice is that if (after set w 79; sh n/c) the proof is taller than it is wide, it's too long.  I've noticed that the proof assistant becomes quite sluggish around 30k uncompressed steps, which has happened twice so far and resulted in an immediate sidetrack to look for places to split.  I'll apply the compression-time heuristic from now on as well.

Lol, this is a response to me, since I have published theorems that take 40+ minutes to compress. The reason is because mmj2 works with compressed proofs directly (or at least, it uses a form that maintains the identical-subtree interning), so it doesn't experience a significant slowdown on things that increase the compression ratio, and I don't realize until I put it in metamath that the theorem is a million steps long uncompressed (and reasonably sized when compressed). The metamath has a power-law time consumption compared to the number of steps that I estimated around n^2.5, so the problem gets really bad really fast if the step count gets too large.

 

I shouldn't comment too much on your choice of size limit, since I probably have bad habits, but my size limit is about 700 steps, which is about 6 times your suggestion. Norm's average theorem size is much closer to your figure than mine.

I seem to have a particular problem with proofs that rely heavily on algebraic manipulation.  I don't suppose you know any magic bullets for those.  (I do have an idea I've been exploring, but it involves a change to ~ df-op and that's probably overstepping my bounds as a newbie juuuust a tad.)

This is understandably a pain, right now. I have several ideas for magic bullets, some of which are in current development for mmj2, but this is by and large a manual process (although mmj2 will make stuff like closure proofs much easier of you have autocomplete enabled).

 

Hopefully this isn't too many questions for today.  Part of my motivation for asking all this here is so that the answers are openly visible for the next person to come along.  (One last: How do you pronounce Megill?)

Actually, I'd like to know this too. I think I said meh-GILL at the conference, hope I didn't mess that up and sound weird. :/

Mario

[Mario Carneiro]

On Wed, Oct 15, 2014 at 5:58 AM, Mario Carneiro <di....@gmail.com> wrote:

I usually break before, but there are some that break after

Oops, switch that around. I put binary operation symbols at the *end* of a line.

 

Mario

[fl]

> What constitutes ready in this case?  

I suppose you can send Norm, your mathbox now. He will create a mathboxe for you. Et voilà.

> Looking at the revision log in set.mm, it seems like active contributors feed their changes back every couple weeks.  Is that a good model to follow?

No. You do what you want, when you want. It's a credit to Norm that the functioning of the site is very flexible. Not formal at all.

> If you use modified set.mms, what's the standard practice for updating them when they change upstream?  

Normally your mathbox is never modified. That means you simply retrieve a new version of set.mm and replace
the old version your mathbox with the new one.

> Would you have any idea what a Pell14QR is? 

It doesn't matter. The normal way to look for a theorem in set.mm is to use regexp to find keywords just like Ring or things like that and then retrieve
the name to apply it.

--
FL

[n...@alum.mit.edu]

Hi Stefan,

> Do we have a list of surface syntax conventions to follow, beyond those
> that are enforced by rewrap?  I found a description of the section break
> comment syntax hidden in "HELP TEX".  I've been breaking after
> connectives — I'll switch to before for consistency.

Early theorems in set.mm tend to break after the connective.
A few years ago, someone convinced me it was more natural (consistent
with mathematical texts) to break before the connective, such as
a string of equalities in the literature with each line beginning
with "=", and I've adopted that practice ever since, even retrofitting
some old ones occasionally.

> On Monday, October 13, 2014 7:34:03 PM UTC-7, n...@alum.mit.edu wrote:
>
> >   It looks like you've done some impressive work.  When you are ready,
> >   send me an email with a link to the latest version, and I will create a
> >   mathbox for you in the official set.mm.
>
>
> What constitutes ready in this case?  I expect that late next week or so
> I'll be revisiting most of the old proofs to remove mathboxes and apply
> any "lessons learned".  Would after that be a good point?

You should do 2 things for it to be ready for me to put into a mathbox:

1. Eliminate other mathbox refs unless you'd like to see the theorem
in the main set.mm (and let me know which).

2. Manually format your $p,$e,$a statements to be less than 80
characters wide, so rewrap won't mangle them.

Some people think that requiring 79-char lines is archaic, but there
are still reasons for it.  Here is python's rationale:
http://legacy.python.org/dev/peps/pep-0008/#maximum-line-length

> (So far, I have basically not touched working proofs.  If it verifies
> and the statement is correct, I've left it be.  This will be changing
> soon.)
>
> Looking at the revision log in set.mm, it seems like active contributors
> feed their changes back every couple weeks.  Is that a good model to
> follow?

There are no guidelines, it's whenever you want.  The longer between
releases usually means less work for me, so every day would be a
pain; every two weeks seems reasonable if you are very active.

It is helpful not to let it get too far out of sync with set.mm label
changes etc., although I'm usually able to update without too much
trouble mathboxes people send me that are based on long-obsolete
set.mm's.  Of course I appreciate it if you make sure it's updated to
the latest set.mm before submission.


Regarding your notes at the end of your mathbox file:


>   2. WRITE SOURCE with $[ $] would make my life much easier

This is on my to-do list (has been for many years).  I'll move up its
priority.

>   3. Namespaces - see separate doc

See the 13-May-04 entry in http://us.metamath.org/mpegif/mmnotes2004.txt
for the rationale behind label naming at that time.  At the top of
set.mm, you can see there has been fine-tuning of thousands of label
names over time to improve consistency.

I notice that you use upper case in some labels.  So far, almost all
labels are lower case for ease of typing, although this is the
convention more than a prohibition.  Others may wish to discuss this.

>   7. disjoint variables in PA would save me much time

On my to-do list.  I haven't made it a priority since mmj2 does a fine
job creating the dv list.  (Personally, I use a bash script that reads
set.mm, verifies the proof of the statement given by its argumenet, and
formats the error output.)

>   8. vim highlighting

If you do this, I'll add it to the highlighting page
http://us.metamath.org/screen1.html

>   9. PA should collapse identical proof stages; possibly add an improve option to seek out commonality by using incomplete subtrees

I don't have plans for this right now.  Some people use the 'dummylink'
 and 'idi' theorems to their advantage; personally I often use all kinds of
ad hoc 'submit' scripts built from the proof listing.  You are aware of
course that 'improve' will fill in identical stages once the first
instance is completely proved (occasionally you need to 'improve all'
twice).  With mmj2 experience you may no longer consider this
important, assuming you even use MM-PA anymore.  :)

>   10. experiment with the proof shrinking potential of deduction versions of the algebra theorems
>       10b. <. A , B >. = if ( B e. _V , { A , { A , B } } , 1o )

Mario's technique for deductions (adding ph -> before each hypothesis
and the final theorem, with all antecedents broken out into hypotheses,
has probably made the dedth stuff more or less obsolete (although I
still think dedth is an interesting technical device).

>   11. PA should display [-NN] in sh n/u listing

Good suggestion, I'll think about that.  Added "think about it" to to-do list.

>   12. automatic improve and loud warning when a ground wff cannot be proved?

Maybe, not sure right now how big a job it will be; mmj2 is much better at this.

>   13. command to list changed proofs

Let me think about; shouldn't be too hard to do.  Added to to-do list.

>   14. I just reproved 19.26 because I had no way of finding it :x

We've renamed many of the 19.* labels over time.  Suggestions for more
consistent naming are always welcome.

>   15. Last command in HELP DEMO is wrong ( (_ is C_ )

Will be fixed in next version of program.  Historically, (_ was changed
to C_ in set.mm because of complaints that emacs couldn't distinguish it
from an opening parenthesis.

>   16. Some kind of macro/repeat command.  Needs much more though

There is the 'submit' command, but it doesn't not have the ability to
take arguments.  I have submit scripts to build submit scripts using the
'tools' commands (or rarely bash CLI utilities) to change things like
the 'show labels' output (using 'open log') into say running 'minize' on
the whole database with a newly added prop calc theorem.

>   19. MATCH would be much more awesome if it took a name wildcard

Actually I have never found 'match' very useful and have informally
considered it deprecated, but I'll think about it some more.  I haven't
used it in years.

>   20. Blank lines before/after SHOW PROOF would help

The metamath program is very stingy with blank lines in order to fit as
much info on the screen as possible.  Historically, terminal windows
were fixed at 24x80 and are still the typical default.  If you still
consider this problematic after more experience w/ the program, bring it
up again.

>   21. backrefs in SEARCH

Not sure what you mean.

>   22. how can the PA (in particular SHOW PROOF) be made more usable with very large proofs?  common syntax-subtree mining / abbrevification?  reduce indent without going all the way to LEMMON?  better control over the proof tree fragment to display?

mmj2

>   23. Pony: catch SIGINT, make MINIMIZE_WITH and IMPROVE interruptable, suppress output

Perhaps.  I'll add a to-do note to look into it.  Right now I just make
sure I've saved everything before trying a possibly long-running command.

>   24. IMPROVE LHF: switch to iterated deepening to avoid idiVD, use the first of a set of equivalent theorems to avoid grothomex syndrome ( but prefer axioms if later )

I plan to add options to IMPROVE to avoid certain statements, avoid
mathboxes by default, and to scan forward instead of reverse.

>   25. SHOW STATEMENT NEW would be cool

Good suggestion, I've wanted that myself.  Added to to-do list.

>   26. ASSIGN with $e does not work as described.  it would be much more useful if out of scope $e's were excluded

Can you be more specific?  When assigning hypotheses, I often do 'assign
last *.a' if the local hypothesis is 'abc.a' and there are no global
labels matching *.a.

>   27. /WIDTH to SHOW PROOF

'set width' sets the default width for all output, including proofs.

>   28. LET [VAR] $1 = $2 = ...

Not sure how often this would be used.  Hopefully you use rlwrap to
call metamath so that the uparrow key will recall the last command,
then just erase the last $2 to make it $3 or whatever.

>   29. LET STEP seems possibly nonfunctional, need to investigate

Let me know if you can pin down a problem.  Personally I rarely use it
(like almost never) so it's possible it has a bug I missed.

>   30. V P {MY-MATHBOX}

Not sure if it is worth the effort - is 'verify proof *' too slow?  I also use
'verify proof */s' to find my unproved theorems quickly.  Currently there is
nothing that identifies "your" mathbox except when you are inside of MM-PA.

>   31. MMPE: hover over GIFs to see original math symbol?

Actually, this would be a set.mm thing:  add 'title=' in addition to
'alt=' in the htmldef.  Or can we just replace 'alt' with 'title' to
help conserve page size?  Anyone know whether this would cause problems
with some browsers?

Note that 'alt=' causes copy/paste into a text editor to show the
original symbol.

>   32. MMPE: hover over subexpression, see "parse" (highlight smallest wff/class around cursor)?

This may be hard to do without making page size huge or invoking
server-side stuff on the fly.  Right now all the pages are static,
because it makes volunteer mirror site configuration more difficult or
possibly impossible depending on the web server used by the volunteer.
Maybe javascript could do it looking only at the page itself together
with some ad-hoc code customized to set.mm, but I've tried hard to make
the site strictly "Web 1.0", which several people have said they
appreciate, and maintenance is a lot simpler with a KISS philosopy.

Norm

[Mario Carneiro]

On Wed, Oct 15, 2014 at 12:14 PM, <n...@alum.mit.edu> wrote:

Hi Stefan,

> Do we have a list of surface syntax conventions to follow, beyond those
> that are enforced by rewrap?  I found a description of the section break
> comment syntax hidden in "HELP TEX".  I've been breaking after
> connectives — I'll switch to before for consistency.

Early theorems in set.mm tend to break after the connective.
A few years ago, someone convinced me it was more natural (consistent
with mathematical texts) to break before the connective, such as
a string of equalities in the literature with each line beginning
with "=", and I've adopted that practice ever since, even retrofitting
some old ones occasionally.

Hm, I didn't know this bit of history. It's worth mentioning that the Python style guide you linked to also recommends breaking after a connective (although opinions tend to be split in programming languages - http://yohanan.org/steve/projects/java-code-conventions/ recommends breaking before every connective except a comma). Regarding mathematical texts, I would argue that the behavior of breaking before equals is limited to the equals sign or other binary relations like < , while operations like + tend to be either at the end of the line or on both lines (although I dislike the practice of putting it on both lines since then it doesn't make any sense if you delete the line breaks).

 

Mario

[Mario Carneiro]

>   10. experiment with the proof shrinking potential of deduction versions of the algebra theorems

This has been on my to do list for a looong time, because ever since I started using deductions extensively it became much more common to use theorems like addcl or addcom in deduction form (via syl2anc or syl3anc) than inference form, even though most of these theorems have an inference form from the time when we used dedth for this stuff. To do this properly needs a study on how it affects proof length, though, and that's a big project. The simplest algorithm here is to make deduction form theorems of every algebra theorem that is already in inference form and theorem form, since that's probably the most commonly used ones.

>       10b. <. A , B >. = if ( B e. _V , { A , { A , B } } , 1o )

I'm not sure what the idea is with this definition. Why 1o = { (/) } ? What problem does this definition solve? The issue with using <. A , B >. = { A , { A , B } } is that you need ax-reg to prove opth because otherwise if x = {y} and y = {x} then <. x , x >. = <. y , y >. , and this is not desirable (ax-reg affects very little mathematically, and we like to keep it that way). Furthermore, even though usually definitions are subject to change (and I have been responsible for MANY definition changes over the time I've been contributing), practically speaking the Kuratowski definition of df-op is holding up a lot more theorems than you would think - it doesn't just stop at opth - for example ovprc2 or brrelex, also rankop, which are themselves holding up many more theorems.

[Stefan O'Rear]

On Wednesday, October 15, 2014 8:08:16 PM UTC-7, Mario Carneiro wrote:

>       10b. <. A , B >. = if ( B e. _V , { A , { A , B } } , 1o )

I'm not sure what the idea is with this definition. Why 1o = { (/) } ? What problem does this definition solve? The issue with using <. A , B >. = { A , { A , B } } is that you need ax-reg to prove opth because otherwise if x = {y} and y = {x} then <. x , x >. = <. y , y >. , and this is not desirable (ax-reg affects very little mathematically, and we like to keep it that way). Furthermore, even though usually definitions are subject to change (and I have been responsible for MANY definition changes over the time I've been contributing), practically speaking the Kuratowski definition of df-op is holding up a lot more theorems than you would think - it doesn't just stop at opth - for example ovprc2 or brrelex, also rankop, which are themselves holding up many more theorems.

Since you asked, the point is actually to break ovprc2.  The second A is supposed to be { A } - that's just a typo.  The intent here is that the pair becomes symmetrical in its treatment of proper classes; < _V, x > is already 1o, under the notional change < x , _V > is also 1o and we can conclude ( < A , B > =/= 1o <-> ( A e. _V /\ B e. _V ) ).  This in turn allows for a strong symmetrical form of brrelex: ( ( Rel R /\ A R B ) -> ( A e. _V /\ B e. _V ) ), and also gives us ( -. ( A e. CC /\ B e. CC ) -> ( A + B ) = (/) ), which means that addcom, etc can be proven with no antecedents at all.

Throw in ax-cnmario $a -. (/) e. CC $. from earlier this year, and we can strengthen this to ( ( A + B ) e. CC <-> ( A e. CC /\ B e. CC ) ), which allows all polynomial identities where both sides have the same two or more variables (i.e. not npcan, but would allow stuff like muladd and sub4) to become similarly antecedent-free.  Effectively what has happened is that (/) is now playing the role of an IEEE 754 NaN value; any arithmetic formula where some operations don't make sense evaluates to (/), and since (/) is not a complex number, this propagates up to the top and satisfies the equality.  We don't get npcan because ( ( 1 - _V ) + _V ) = (/) =/= 1, although we could (very likely a net loss, so will not pursue this sub-suggestion further) slightly weaken the antecedent on npcan to A e. ( CC u. 1o ) which is interesting as the domain of absolute closure of arithmetic operations.

In non-algebra parts of set.mm, ensymg loses its antecedent, while numth gains one; so far, the only example I've found where antecedents increase is numth and other theorems which use the same construction, but I'm sure I'd find a lot more if I ever started this project in earnest.

I tried for about an hour earlier to retrofit set.mm to use Wiener pairs, which have the same symmetric proper class property, and did indeed discover that it broke rankop, but also broke the U. U. idiom for extracting domain and range for a relation, which seemed like a major pain to rework.  Since this version reduces to the current definition when B is a set (and in particular when B is a set variable), there is a glimmer of hope it could be less disruptive.  I haven't spent any significant time on the current iteration of the proposal; I expect it to be dismissed quickly for most of the same reasons from the -. (/) e. CC thread, and also because there's a significant principle-of-least-surprise violation potential for <. A , B >. being anything other than a basic Kuratowski pair.  (Although I could also argue that proper classes are "undefined behavior" for Kuratowski and we're free to do whatever is most convenient in that case...)

On a mostly unrelated note, the current lttrd and friends have 2-3 unnecessary antecedents: from A < B we can already infer A e. RR* and B e. RR* (since < is irreflexive, it doesn't matter whether we use the current opprc2 or the notional new one).

So.  Ridiculous proposal?  Or worth further discussion?  Still feeling rather self-conscious about being that guy who shows up and immediately demands for everything to be changed.

[Stefan O'Rear]

Most of this makes sense and doesn't need a response; I've make a separate post to elaborate on my wacky df-op idea.  Further comment on the proof assistant will be suspended until I've gotten around to trying mmj2.

Mario: I apparently have out of date or wrong ideas about what gives git fits.  I'll try out your single-file flow.

On Wednesday, October 15, 2014 9:14:55 AM UTC-7, n...@alum.mit.edu wrote:

>   2. WRITE SOURCE with $[ $] would make my life much easier

This is on my to-do list (has been for many years).  I'll move up its
priority.

Although if I switch to working in a single file per Mario that'll go way down on my personal to-do list.

 

>   3. Namespaces - see separate doc

See the 13-May-04 entry in http://us.metamath.org/mpegif/mmnotes2004.txt
for the rationale behind label naming at that time.  At the top of
set.mm, you can see there has been fine-tuning of thousands of label
names over time to improve consistency.

This item was intended to refer more to math symbols, as in "what if two unrelated fields want to define a J function"?

 

I notice that you use upper case in some labels.  So far, almost all
labels are lower case for ease of typing, although this is the
convention more than a prohibition.  Others may wish to discuss this.

The uppercase labels are ridiculous.  I'm going to fix those later.

 

>   20. Blank lines before/after SHOW PROOF would help

The metamath program is very stingy with blank lines in order to fit as
much info on the screen as possible.  Historically, terminal windows
were fixed at 24x80 and are still the typical default.  If you still
consider this problematic after more experience w/ the program, bring it
up again.

That note was intended to refer specificially to SHOW PROOF /COMPRESSED.  The idea here is that blank lines would make it easier to copy and paste the proof without requiring quite so much mouse finesse / editing after to remove the surrounding text.  Again, less of an issue if I switch to a single-file / WRITE SOURCE approach.

 

>   21. backrefs in SEARCH

Not sure what you mean.

Suppose I've forgotten the name of the simp2 theorem.  I can currently search for "|- ( ( ?? /\ ?? /\ ?? ) -> ?? ) and find simp2, but I also find simp1 and simp3.  If I could instead write "( ?? /\ ?1 /\ ?? ) -> ?1" and have it automatically restrict to matches where the *same* symbol appeared for both uses of ?1, this would be useful on occasion, although it's a PA-related feature so mmj2 might already have this.  Incidentally the first time I read the documentation for SEARCH I misunderstood it to mean that ? matched a single *math symbol* and was quite confused that propositional theorems couldn't be found by it, but that turned out to be pure PEBKAC.

 

>   26. ASSIGN with $e does not work as described.  it would be much more useful if out of scope $e's were excluded

Can you be more specific?  When assigning hypotheses, I often do 'assign
last *.a' if the local hypothesis is 'abc.a' and there are no global
labels matching *.a.

What I've seen is that "a l *.1" throws a massive ambiguity error because (my build, my computer, and the one time I tried it) it seemed to be finding all the .1 hypotheses, not just the single one that was in scope.  Quite likely I was just imagining this; I need to debug it later.

>   27. /WIDTH to SHOW PROOF

'set width' sets the default width for all output, including proofs.

This was a wishlist item so that "sh n/c/w 79" would output a proof suitable for copying in a single step, as opposed to my current process of "set w 79" "sh n/c" "set w 270".

 

>   28. LET [VAR] $1 = $2 = ...

Not sure how often this would be used.  Hopefully you use rlwrap to
call metamath so that the uparrow key will recall the last command,
then just erase the last $2 to make it $3 or whatever.

Just a little idea for a slight improvement.  The other half of that item was making VAR optional.

 

>   29. LET STEP seems possibly nonfunctional, need to investigate

Let me know if you can pin down a problem.  Personally I rarely use it
(like almost never) so it's possible it has a bug I missed.

OK, will do.

 

>   30. V P {MY-MATHBOX}

Not sure if it is worth the effort - is 'verify proof *' too slow?  I also use
'verify proof */s' to find my unproved theorems quickly.  Currently there is
nothing that identifies "your" mathbox except when you are inside of MM-PA.

I think at the time I wrote this I wanted to do a super-quick verify of my proofs as part of a git pre-commit hook, and the idea was to use a statement range rather than making it tied to mathboxes alone.  Either way, I have no current need for this.

 

>   31. MMPE: hover over GIFs to see original math symbol?

Actually, this would be a set.mm thing:  add 'title=' in addition to
'alt=' in the htmldef.  Or can we just replace 'alt' with 'title' to
help conserve page size?  Anyone know whether this would cause problems
with some browsers?

Note that 'alt=' causes copy/paste into a text editor to show the
original symbol.

I'll admit I never tried the copy and paste thing.

[Mario Carneiro]

On Thu, Oct 16, 2014 at 1:02 AM, Stefan O'Rear <stef...@cox.net> wrote:

On Wednesday, October 15, 2014 8:08:16 PM UTC-7, Mario Carneiro wrote:

>       10b. <. A , B >. = if ( B e. _V , { A , { A , B } } , 1o )

I'm not sure what the idea is with this definition. Why 1o = { (/) } ? What problem does this definition solve? The issue with using <. A , B >. = { A , { A , B } } is that you need ax-reg to prove opth because otherwise if x = {y} and y = {x} then <. x , x >. = <. y , y >. , and this is not desirable (ax-reg affects very little mathematically, and we like to keep it that way). Furthermore, even though usually definitions are subject to change (and I have been responsible for MANY definition changes over the time I've been contributing), practically speaking the Kuratowski definition of df-op is holding up a lot more theorems than you would think - it doesn't just stop at opth - for example ovprc2 or brrelex, also rankop, which are themselves holding up many more theorems.

Since you asked, the point is actually to break ovprc2.  The second A is supposed to be { A } - that's just a typo.  The intent here is that the pair becomes symmetrical in its treatment of proper classes; < _V, x > is already 1o, under the notional change < x , _V > is also 1o and we can conclude ( < A , B > =/= 1o <-> ( A e. _V /\ B e. _V ) ).  This in turn allows for a strong symmetrical form of brrelex: ( ( Rel R /\ A R B ) -> ( A e. _V /\ B e. _V ) ), and also gives us ( -. ( A e. CC /\ B e. CC ) -> ( A + B ) = (/) ), which means that addcom, etc can be proven with no antecedents at all.

I would consider this the strongest point of your proposal, although I'd revise it to ( <. A , B >. e. ( _V X. _V ) <-> ( A e. _V /\ B e. _V ) ), because it seems a bit peculiar to refer explicitly to 1o except for theorems immediately after the definition. I find the asymmetry itself to be a principle-of-least-surprise violation, especially since most people haven't thought about how the Kuratowski definition interacts with proper classes, and I agree that that is an "undefined" region for the usual statement of the definition.

 

Throw in ax-cnmario $a -. (/) e. CC $. from earlier this year, and we can strengthen this to ( ( A + B ) e. CC <-> ( A e. CC /\ B e. CC ) ), which allows all polynomial identities where both sides have the same two or more variables (i.e. not npcan, but would allow stuff like muladd and sub4) to become similarly antecedent-free.  Effectively what has happened is that (/) is now playing the role of an IEEE 754 NaN value; any arithmetic formula where some operations don't make sense evaluates to (/), and since (/) is not a complex number, this propagates up to the top and satisfies the equality.  We don't get npcan because ( ( 1 - _V ) + _V ) = (/) =/= 1, although we could (very likely a net loss, so will not pursue this sub-suggestion further) slightly weaken the antecedent on npcan to A e. ( CC u. 1o ) which is interesting as the domain of absolute closure of arithmetic operations.

As the result of that thread suggests, you probably won't get far with this part. The best approach is to see what is derivable assuming that the truth of (/) e. CC is unknown and also not assuming ax-addopr if you can help it. Indeed this was the main reason I wanted to introduce that axiom in the first place, but I respect wanting to have an "axiomatic" treatment of the reals, so that's that. (Another antecedent-simplifying modification would be defining (x/0)=0, but Norm likes to follow the literature whenever possible, and the usual language suggests that the function is not defined at zero.)

 

In non-algebra parts of set.mm, ensymg loses its antecedent, while numth gains one; so far, the only example I've found where antecedents increase is numth and other theorems which use the same construction, but I'm sure I'd find a lot more if I ever started this project in earnest.

(I assume you mean numth2, since numth doesn't use binary operations.) It's interesting that you mention this, because Gerard Lang actually emailed me once for clarification on how this theorem could be true for proper classes, since if you extend the meaning of "equinumerous" to proper classes and assume that ~~ still works in this domain, then it's obviously false; so in that sense it's a documented failure of "principle of least surprise".

 

I tried for about an hour earlier to retrofit set.mm to use Wiener pairs, which have the same symmetric proper class property, and did indeed discover that it broke rankop, but also broke the U. U. idiom for extracting domain and range for a relation, which seemed like a major pain to rework.  Since this version reduces to the current definition when B is a set (and in particular when B is a set variable), there is a glimmer of hope it could be less disruptive.  I haven't spent any significant time on the current iteration of the proposal; I expect it to be dismissed quickly for most of the same reasons from the -. (/) e. CC thread, and also because there's a significant principle-of-least-surprise violation potential for <. A , B >. being anything other than a basic Kuratowski pair.  (Although I could also argue that proper classes are "undefined behavior" for Kuratowski and we're free to do whatever is most convenient in that case...)

The main alternative to the Kuratowski definition I've considered is something like the Morse definition, because it works for proper classes as well as sets and also only increases the rank by 1 IIRC. But then I discovered that it's already defined as df-cda, although the name doesn't make it obvious and it doesn't work on proper classes right now because it's defined as a binary op instead of a syntax operation. (It also works as a "disjoint union" operator.)

 

On a mostly unrelated note, the current lttrd and friends have 2-3 unnecessary antecedents: from A < B we can already infer A e. RR* and B e. RR* (since < is irreflexive, it doesn't matter whether we use the current opprc2 or the notional new one).

I've noticed this, and fixing it is on my to do list, although Norm may object because this relies on < being a binary op and not a syntax construction. Since < is a derived operation, though (the axiomatic relation is <RR ), you may be okay here.

 

So.  Ridiculous proposal?  Or worth further discussion?  Still feeling rather self-conscious about being that guy who shows up and immediately demands for everything to be changed.

I am a strong believer that in the field of mathematics it is one's proofs and ideas that are relevant, not more ego-related notions such as age, popularity or even educational status, quite unlike many other fields of academia, which is a major reason which drove me toward mathematics. Not too long ago I was in the same position (including the demand that many things be changed), so I can definitely understand where you're coming from and I'd like to think that we can see past seniority concerns.

>   3. Namespaces - see separate doc

See the 13-May-04 entry in http://us.metamath.org/mpegif/mmnotes2004.txt
for the rationale behind label naming at that time.  At the top of
set.mm, you can see there has been fine-tuning of thousands of label
names over time to improve consistency.

This item was intended to refer more to math symbols, as in "what if two unrelated fields want to define a J function"?

Currently the best way this is handled is via so-called "temporary definitions", since that allows you to reuse the same names over and over without any conflicts, although you have to keep restating the definition or else have all the theorems dealing with the function in a contiguous block. If you think it deserves a true definition, then you have to use a subscript or a prefix or something to globally disambiguate it - that's the closest we get to symbol namespaces. Since metamath can't abbreviate symbols, although it would be possible, defining a NumberTheory.Pell.J symbol would be too verbose in practice. This came up for me recently when I defined the Gauss prime pi function, whose symbol "ppi" is indistinguishable from "pi" in most math texts. Even if the symbol pi is just used visually on the web pages, it can still lead to confusion because although the fields are unrelated, they aren't unrelated enough for me to prove that since ppi(pi)=2, <. pi , 2 >. e. ppi and so rank(pi) e. rank(ppi) (which would look *really* confusing in proof display).

Mario

[fl]

 

> I am a strong believer that in the field of mathematics it is one's proofs and ideas that are relevant.

 

Seems too pure.

 

> See the 13-May-04 entry in http://us.metamath.org/mpegif/mmnotes2004.txt
> for the rationale behind label naming at that time.

 

In    http://us.metamath.org/mpegif/mmnotes2004.txt all what is related to the names of the theorems

is disparate and more concerned with the theorems at the top of set.mm than with the current ones.

What might be of more use is a system of prefixes according to the field.

 

--

FL

[Norman Megill]

On Thursday, October 16, 2014 2:34:10 AM UTC-4, Mario Carneiro wrote:

On Thu, Oct 16, 2014 at 1:02 AM, Stefan O'Rear <stef...@cox.net> wrote:

Throw in ax-cnmario $a -. (/) e. CC $. from earlier this year, and we can strengthen this to ( ( A + B ) e. CC <-> ( A e. CC /\ B e. CC ) ), which allows all polynomial identities where both sides have the same two or more variables (i.e. not npcan, but would allow stuff like muladd and sub4) to become similarly antecedent-free.  Effectively what has happened is that (/) is now playing the role of an IEEE 754 NaN value; any arithmetic formula where some operations don't make sense evaluates to (/), and since (/) is not a complex number, this propagates up to the top and satisfies the equality.  We don't get npcan because ( ( 1 - _V ) + _V ) = (/) =/= 1, although we could (very likely a net loss, so will not pursue this sub-suggestion further) slightly weaken the antecedent on npcan to A e. ( CC u. 1o ) which is interesting as the domain of absolute closure of arithmetic operations.

As the result of that thread suggests, you probably won't get far with this part. The best approach is to see what is derivable assuming that the truth of (/) e. CC is unknown and also not assuming ax-addopr if you can help it. Indeed this was the main reason I wanted to introduce that axiom in the first place, but I respect wanting to have an "axiomatic" treatment of the reals, so that's that.

As Mario implies, I want to keep CC completely independent from its construction, so that in principle (and possibly in the future) we could swap in a different construction to achieve the same final axioms.  For example, the constructions RR in Quine's Set Theory and Its Logic, as well as in Levy's Basic Set Theory, build the successive layers (ZZ, QQ, RR) on top of ordinals as strict supersets, so that NN0 = omega; thus (/) is the number 0 in those constructions.  There's a certain appeal to that, since in principle finite ordinals and NN0 could share the same theorems, although in practice we probably still wouldn't do that in order to keep CC construction-independent.

Unlike most things in set.mm, the complex numbers have a larger audience that is sometimes unsophisticated mathematically, and I want to give them a development from complex number "axioms" that is as straightforward and set-theory-independent as possible, avoiding tricks that make use of say the out-of-domain behavior of df-fv.  Outside of complex numbers, I use and encourage such tricks to shorten theorem statements and proofs.

 

(Another antecedent-simplifying modification would be defining (x/0)=0, but Norm likes to follow the literature whenever possible, and the usual language suggests that the function is not defined at zero.)

(clipped from an old email to Mario:)
I don't want to change the domain to include 0, for reasons that aren't
entirely mathematical.  I realize that with our definition of df-fv,
both evaluate to (/), although this df-fv behavior is just our arbitrary
choice for convenience and not universal in the literature.  But there
is a psychological aspect.  For one thing, it makes it immediately
obvious that 0 should be excluded in normal use.  Also, in the 1990s,
there were many heated Usenet debates on sci.math about what the value
of division by 0 should be, and part of my reason for excluding 0 from
the domain was to be agnostic about it and not subject the Metamath site
to that debate (most people wouldn't dig deep enough to understand the
out-of-domain df-fv).  People also send me emails wanting to argue about
such things (some who might be considered "cranks") and I don't want to
unnecessarily open that can of worms for them.  Note also that division
rings in general (df-drng) exclude 0 from the multiplicative inverse
function.

Interestingly, HOL Light postulates that division by 0 equals 0, and uses that to shorten some proofs.  However, HOL has a somewhat steeper "price of admission" than clicking on a Metamath web page, probably filtering out a lot of amateur math critics.

On a mostly unrelated note, the current lttrd and friends have 2-3 unnecessary antecedents: from A < B we can already infer A e. RR* and B e. RR* (since < is irreflexive, it doesn't matter whether we use the current opprc2 or the notional new one).

I've noticed this, and fixing it is on my to do list, although Norm may object because this relies on < being a binary op and not a syntax construction. Since < is a derived operation, though (the axiomatic relation is <RR ), you may be okay here.

I would object to this because the axioms for CC (excluding RR*) could be restated to use < as primitive.  The <RR is basically a kind of workaround to let us later use the same < symbol for reals and extended reals for a somewhat prettier overall presentation.  But the "intent" of the early theorems that don't reference RR* is that < means <RR, and we should be able to swap in <RR (renaming it to < if we took out RR*) to obtain a "purer" development of RR without extended reals.

This is a subjective matter, and I'm not sure if I'm conveying it well, but in some sense I want the axiomatic development of CC to be as free of set-theoretical tricks as practical.  This applies mostly to the early development of elementary algebra the non-set-theorists might follow.  Later on, in advanced stuff using CC, I'm a lot more tolerant because anyone getting that far must learn a lot of set theory.

BTW the heavy use of the awkard dedth in that development probably violates the rule, although actually dedth can be done with nothing but propositional calculus; the "if()" stuff just makes it more compact for use with set theory.  Eventually we may want to phase it out, perhaps using Mario's deduction method or always using the closed theorem form, but that's very low priority right now.

>> Hopefully this isn't too many questions for today.  Part of my motivation for asking all this here is so that the answers are openly visible for the next person to come along.  (One last: How do you pronounce Megill?)

> Actually, I'd like to know this too. I think I said meh-GILL at the conference, hope I didn't mess that up and sound weird. :/

I usually pronounce it muh-GILL, although in Brazil I've resigned myself to meh-ZHEE-oo since it always seems to end up pronounced that way after a couple of iterations of people repeating it to others.  Historically, it was McGill until someone changed it to Megill in the 1800s for reasons unknown, possibly an ancestor who disliked the shift key, a characteristic that lives on in the set.mm labels.

Norm

[Norman Megill]

On Wednesday, October 15, 2014 10:05:23 PM UTC-4, Mario Carneiro wrote:

On Wed, Oct 15, 2014 at 12:14 PM, <n...@alum.mit.edu> wrote:

Hi Stefan,

> Do we have a list of surface syntax conventions to follow, beyond those
> that are enforced by rewrap?  I found a description of the section break
> comment syntax hidden in "HELP TEX".  I've been breaking after
> connectives — I'll switch to before for consistency.

Early theorems in set.mm tend to break after the connective.
A few years ago, someone convinced me it was more natural (consistent
with mathematical texts) to break before the connective, such as
a string of equalities in the literature with each line beginning
with "=", and I've adopted that practice ever since, even retrofitting
some old ones occasionally.

Hm, I didn't know this bit of history. It's worth mentioning that the Python style guide you linked to also recommends breaking after a connective

Yes, I noticed that.  Python, though a nice language, is strange anyway by making the amount of white space significant, although not as bad as the Whitespace language :).

(although opinions tend to be split in programming languages - http://yohanan.org/steve/projects/java-code-conventions/ recommends breaking before every connective except a comma).

Actually that's the convention I've used throughout the metamath program, more or less subconsciously.  To me it has the advantage of letting you know immediately what is connecting the current line to the previous, since all the operators are lined up neatly in indented columns, vs. putting them at the end of the previous line, causing your eyes to zig-zag back and forth finding them due to variable line lengths.
 

Regarding mathematical texts, I would argue that the behavior of breaking before equals is limited to the equals sign or other binary relations like < , while operations like + tend to be either at the end of the line or on both lines (although I dislike the practice of putting it on both lines since then it doesn't make any sense if you delete the line breaks).

Yes, I've encountered a few books like that and I also dislike it.

As for set.mm, I don't impose any particular convention, do whatever you prefer.  In the far future, someone will probably come along with a pretty-print reformatting program anyway.

---

On a different topic, in the far far future, Metamath may evolve into a different language (hopefully just as simple but perhaps cleaner in some way), but our proofs will be timeless with our names forever attached to them, a nice feeling compared to the ephemeral rewards of writing software that will be obsolete and forgotten in 5 years.  And it's nice to know that what you create is bug-free, so you'll never have to worry about maintaining it unless you want to. 

Personally I think its approach is the right way to express mathematics, even if the existing language/implementation has some warts and the creation of proofs not currently well automated.  (Quoting from a private email to some of you,) I believe Metamath is the most transparent language by far, with perfect and absolute fidelity to the underlying mathematics (the axioms of logic and ZFC).  I don't think other languages (aside from derivatives like Ghilbert) can make those claims; for example, none of them can produce proofs that can be easily traced back to first-order logic axioms as far as I can tell.

Norm

[fl]

On a different topic, in the far far future, Metamath may evolve into a different language (hopefully just as simple but perhaps cleaner in some way), but our proofs will be timeless [...]

Or forgotten for the rest of the eternity. People are so negligent. Who is reading "Principia Mathematica" nowadays?

--
FL

[Mario Carneiro]

On Fri, Oct 17, 2014 at 8:32 AM, fl <freder...@laposte.net> wrote:

On a different topic, in the far far future, Metamath may evolve into a different language (hopefully just as simple but perhaps cleaner in some way), but our proofs will be timeless [...]

Or forgotten for the rest of the eternity. People are so negligent. Who is reading "Principia Mathematica" nowadays?

Um... we are? I don't think that's a very good example for your point. Where do you think theorem 19.26 came from? It's quite likely that in the future some new math system will come along that is as different to Metamath as PM is today. However, the *proofs* are nevertheless portable, and the prediction is that these proofs will live on beyond the lifespan of the system itself.

Mario

[fl]

Um... we are? I don't think that's a very good example for your point. Where do you think theorem 19.26 came from?

 

It's a bad counterexample. Norm only used the first chapters in Principia Mathematica. Only what is

related to propositional calculus. Then he turned to other textbooks.

 

And even if he did so, do you think that Principia Mathematica is as read as -- let's say -- The husband's secret,

by Liane Moriarty.

 

No obviously no.

 

So who is reading Principia Mathematica? nobody I'm afraid.

 

And what's worse, what will happen if the center of wolrd is no longer the United States of America but

China or Africa or South America? Metamath will no longer be read because the central language

will be changed.

 

Except for the first part -- about propositional calculus.

 

What I regret.

 

--

FL

[Mario Carneiro]

The thing about the QED system is that every proof builds on every other proof, so that even if the proofs aren't being read they are being used as essential components of other proofs. In that sense the proofs will be continually referred back to, in the same way that we can reference the prime number theorem in modern proofs because someone went to the trouble of proving it, and once we have the same in metamath we too will be able to reference it. Barring some nuclear war that destroys all records, once a theorem is proven it can't be unproven, and the effort of the person who created the proof will leave a permanent mark on future generations of mathematicians.

--

[fl]

 

So who is reading Principia Mathematica? nobody I'm afraid.

 

 

And you must also take into consideration stupid, oppressive education even in the

democratic parts of the world. You know gender considerations or cultural ones.

 

No, really I don't believe that eternity or universality can be envisioned seriously.

 

--

FL

[fl]

 

No, really I don't believe that eternity or universality can be envisioned seriously.

 

 

A very good thing with set.mm is that it is free. When you compare with the other

mathematical books -- Knuth's ones for instance but Knuth is not the most expensive --

and some are moderatly interesting -- but Knuth is always very interesting -- it comes to your

mind that Norm has made us a very beautiful present and must be thanked for that.

 

--  

FL

[fl]

 Norm has made us a very beautiful present and must be thanked for that.

 

Norm and the other contributors obviously. I had forgotten the other contributors.

But the other contributors to a lesser extent.

 

--  

FL

[Mario Carneiro]

I'm not sure, but I think you are thinking too ego-centrically about this. I don't mean that in a bad way, but my point is that the proofs themselves can live long past their attachment to us as individuals. For example, consider the invention/discovery of gunpowder. Who invented it? I don't know, and I'm sure even historians only have guesses about it. Yet the invention is utilized for guns and fireworks even today, because it is useful and relevant. In this sense the person who invented gunpowder has made a permanent contribution which lives on to today, even though his name might be totally lost. It is in this context that I think eternal contribution can be considered seriously. The greatest danger to this is some cataclysm that turns back the clock on society or destroys it entirely - the usual process of political upheaval and education concerns would be very hard-pressed to permanently suppress an invention or discovery after it is made public.

[fl]

I'm not sure, but I think you are thinking too ego-centrically about this.

No I think that ego is annoying.
 

I don't mean that in a bad way, but my point is that the proofs themselves can live long past their attachment to us as individuals. For example, consider the invention/discovery of gunpowder.

Sure. A definitive contribution to the history of humanity.

--
FL

[fl]

Sure. A definitive contribution to the history of humanity.

And that normally leads to a non eternal existence of the opposite man.

--
FL

[fl]

 

I'm not sure, [...]

 

 

 

I've seen that you have derived ZFC axioms into hol.mm (well a weaker form of them I suppose).

It's fine. Now I think we can easily translate them into set.mm which will settled down a link

between the  two theories.

 

(There is something that annoys me. In hol.mm you definitely have metavariables by the construction

of metamath. It shouldn't exist in HOL. can it have an side effect on the theory?)

 

--

FL

[Mario Carneiro]

--

[Mario Carneiro]

On Sat, Oct 18, 2014 at 9:40 AM, fl <freder...@laposte.net> wrote:

 

I'm not sure, [...]

 

 

 

I've seen that you have derived ZFC axioms into hol.mm (well a weaker form of them I suppose).

It's fine. Now I think we can easily translate them into set.mm which will settled down a link

between the  two theories.

Actually, the most reasonable means of getting hol.mm proofs into set.mm will be via yet another virtualization of HOL, now directly inside set.mm. Although I haven't started work on this, I think it would involve steps that look like:

 |- A e. HOLType
|- HOLStep f ( T. -> { p e. ~P A | { x e. A | ( x e. p -> ( ( f ` A ) ` p ) e. p ) } e. !H [ A ] } e. !H [ A ] )

This is a direct translation of ax-ac from hol.mm. The predicate "A e. HOLType" substitutes for the implicit "type al" in hol.mm proofs, while translating the other syntax constructions treats the type bool specially, so that ( F A ) becomes A e. F if F is of type ( al -> bool ) and ( F ` A ) otherwise. Similarly \ x : al . F becomes ( x e. A |-> F ) or { x e. A | F } depending on whether F : bool or something else. I'm not sure if this will work for everything, though; if I get into more trouble I'll just declare bool = {{{ (/) }}, {{ 1o }}} and work with that instead. Constants like !H (which correspond to ! from hol.mm) need all type parameters explicitly declared, because of the restrictions on constant declarations - the definition of ! in hol.mm has a free type variable, which the set.mm definition checker would reject, but HOL has different rules and this is okay for them since it shows in the type of the constant.

The f built into the HOLStep predicate is a global choice function on every element of HOLType. That is, ( f ` A ) is a choice function for A, which takes a member of ~P A and returns an element of it. HOLStep is defined so that

( HOLStep F ph /\ A e. HOLType ) -> ( F ` A ) e. if ( GlobalChoiceFunctions =/= (/) , ChoiceFunctions(A) , ( A ^m ~P A ) )

That way you don't need AC to prove that HOLStep f ph implies ph, or to prove that f is well typed, but you do in order to prove that ( f ` A ) is a choice function, so you don't need AC unless you actually use ax-ac, as it should be. The upside of all this is that it may be possible to actually virtualize an entire proof in HOL and get out a statement in set.mm lingo, which has been the whole point of all this.

 

 (There is something that annoys me. In hol.mm you definitely have metavariables by the construction

of metamath. It shouldn't exist in HOL. can it have an side effect on the theory?)

I wrote about this a little while ago, but after studying the foundations of both systems I now understand that the 'metavariable' rhetoric is actually a red herring. From the point of view of HOL, metamath doesn't have metavariables. It has two kinds of term variables, and a "subst" rule built into metamath that allows one to substitute a class term variable for a term and change bound variables in an expression. There is no difference between this and the subst/INST rule built into HOL, except that HOL's rule handles proper substitution and dummy renaming, which is not relevant since you can do all that beforehand anyway.

In hol.mm, I have distinguished term variables from 'var' variables in the set.mm tradition, even though there is no such distinction in HOL. I did this because sometimes (mainly when dealing with bound vars) you need to have 'var' variables, but for most other cases it is easier to use term variables because then you can leverage metamath's substitution rule. It's not necessary, though, since you can just use ax-inst to do the same. Similarly, since type variables are never bound, they are all of the kind that can be substituted by metamath automatically without needing a separate INST_TYPE rule.

Mario

[Raph Levien]

I just wanted to point people to http://levien.com/garden/ghilbert/hol/hol-zfc.gh if they are not already aware of it. That's an interpretation of a fairly large fragment of HOL axioms in the set.mm ZFC universe. One limitation is that it implements the iota operator (definite choice) but not epsilon. There _are_ ways to do the latter (see http://us.metamath.org/downloads/choice.txt and http://us.metamath.org/downloads/megillaward2005he.pdf) but it's not quite as convenient.

I haven't dug into the new hol.mm stuff deeply enough to see how close that is to the work I was doing, but perhaps there is some interest. I've been wanting to have more time for Metamath/Ghilbert, but have been insanely busy helping get Lollipop out the door, so just haven't had any time at all.

Raph

--

[Mario Carneiro]

Hi Raph,

Nice to hear you're still around. Indeed much of my current work is similar to your previous work, and I have kept the discussion in choice.txt in mind while drafting all of this. Since the HOL universe is a ZFC set, the easiest way to get the indefinite descriptor in set.mm that I can see is to use AC to find a global choice function on the HOL universe, then just use that as an argument to each HOL step, as I've indicated in the previous message. You could even posit that if there is no global choice function, then it acts like a definite descriptor, so that as long as you can prove that there is a unique element satisfying the property then you can still use the function f to choose it without needing AC. (However, the proofs I'm going to be importing are probably not going to do that, and instead assume AC all over the place since the axiomatization makes it easy to do so.)

[fl]

I just wanted to point people to http://levien.com/garden/ghilbert/hol/hol-zfc.gh if they are not already aware of it.

We are not already aware of it. It is regrettable.  It shows at least that a fancy presentation in the style of metamath
pages (with colors, hyperlink, comments) has its importance.

--
FL