Re: [Metamath] The set.mm section "Recent label changes"

If someone wants to maintain this, that's fine with me, although adding another file to remember to update doesn't seem ideal. Another possibility that doesn't require a separate file is to state at the end of a truncated list something like "Older entries can be found in set.mm version of ,

[Metamath] Re: The set.mm section "Recent label changes"

I agree that we don't need to keep a complete history of all theorems moved from mathboxes. Sometimes I have found it useful to know the recent ones to be aware of changes made to the main part. Perhaps we could have a policy of deleting the ones over say 1 year old like we do for *OLD

Re: [Metamath] Re: Two cleanliness scripts

You can update my mathbox. However, this is clearly a maintenance edit, and in principle no permission is needed per http://us.metamath.org/mpeuni/mathbox.html: "other people may make maintenance edits to your mathbox for things like keeping it synchronized with the rest of set.mm, reducing

Re: [Metamath] Re: Erweiterung df-cleq (English translation: Extending df-cleq)

em, it seems). > Where do you see this? In any case, can't we just apply ax-gen as needed if open formulas are problematic? Norm > > That is not necessarily a proposal to change the axiomatic, and certainly > not in a hurried way. At least it's here for future reference. I looked a >

Re: [Metamath] Suffix d for theorems not in "deduction form"

On Sunday, November 28, 2021 at 1:23:01 PM UTC-5 Benoit wrote: > Jim: indeed, maybe versions related to Mario's algorithm for the deduction > theorem should all be labeled xxxd, whether they have zero or more > hypotheses. > I agree with this, and I think we should change ~conventions to say

Re: [Metamath] Re: Erweiterung df-cleq (English translation: Extending df-cleq)

ioms, abstracting from the details of > construction. > > Wolf > > Norman Megill schrieb am Samstag, 27. November 2021 um 20:36:18 UTC+1: > >> On Saturday, November 27, 2021 at 11:21:49 AM UTC-5 Benoit wrote: >> >>> Here is a complement to Mario's, Thierry's, and Wolf's

Re: [Metamath] Re: Erweiterung df-cleq (English translation: Extending df-cleq)

the solution where we do not overload equality `=` >>>> and membership `e.`, but instead have different versions of those >>>> predicates for sets. >>>> >>>> For those interested, I've published the resulting experiment here: >>>> https://gith

[Metamath] Re: Mandatory "standard" formatting prior to submitting a pull request?

As I indicated on github, I support adding this CI check. The next metamath.exe version (0.199) fixes a minor /rewrap issue that affects 4 lines in set.mm, and these will annoyingly flip-flop back and forth in PRs until everyone updates to 0.199. So I think it makes sense to hold off

Re: [Metamath] Re: Erweiterung df-cleq (English translation: Extending df-cleq)

x / y] ph. The transformed df-clab and > ax-9c instances are theorems of S, and none of the other axioms mention cab > or wvel. Since Phi is not changed by the transformation, Phi is derivable > from S. > > On Fri, Oct 29, 2021 at 12:24 PM Benoit wrote: > >> On Friday, Oc

Re: [Metamath] Re: Erweiterung df-cleq (English translation: Extending df-cleq)

Can you remind me what the minimal positive calculus is? On Friday, October 29, 2021 at 11:58:02 AM UTC-4 Benoit wrote: > The hypothesis of bj-df-cleq corresponds to setvar substitutions into A >> and B. Do we know that other substitutions into A and B can't generate FOL= >> statements that

Re: [Metamath] Re: Erweiterung df-cleq (English translation: Extending df-cleq)

On 10/28/21 2:20 PM, Benoit wrote: > I think we should keep the "overloading" of equality and membership. > The assumption is not hidden in set.mm, but explicit: it is ~cv > (http://us2.metamath.org/mpeuni/cv.html). I still favor the forms > bj-df-cleq/bj-dfclel, which imply minimal changes

Re: [Metamath] Re: Erweiterung df-cleq (English translation: Extending df-cleq)

On 10/27/21 9:55 PM, Mario Carneiro wrote: > An example of a ZFC+classes expression containing class variables that > has no equivalent without class variables is "x e. A". Any expression > equivalent to this must contain the variable "A". "A" can be introduced and eliminated by substitution

Re: [Metamath] Re: Erweiterung df-cleq (English translation: Extending df-cleq)

(The us2 server was down most of the afternoon due to a power failure caused by a storm. It should be back up now.) On Wednesday, October 27, 2021 at 1:18:17 PM UTC-4 di wrote: > On Wed, Oct 27, 2021 at 11:40 AM Norman Megill wrote: > >> I discuss the issue of whether to call

Re: [Metamath] Re: Erweiterung df-cleq (English translation: Extending df-cleq)

only when you > introduce the whole set of axioms at once, and even then we must assume the > full set of FOL axioms (like ax-9) to start with. Metamath does not have an > adequate mechanism for introducing new conservative sorts, and I think we > should just own up to this and admit these a

[Metamath] Re: Erweiterung df-cleq (English translation: Extending df-cleq)

On Tuesday, October 26, 2021 at 6:07:19 PM UTC-4 ookami wrote: > Norman Megill wrote Tuesday, 26. Oktober 2021 at 21:46:35 UTC+2: > >> Which comment of Benoît you are referring to? >> >> In PR #2267 he described the phenomenon of the vanishing ax-9 as an > arti

[Metamath] Re: Erweiterung df-cleq

Which comment of Benoît you are referring to? Anyway, he has brought this up before; see bj-ax9, which derives ax-9 from df-cleq (with the help of additional axioms ax-1 through ax-7, ax-12, and ax-ext), and bj-df-cleq, which is proposed as a replacement for df-cleq. See also my comment at

[Metamath] Re: Is there a proof for "2+2=4" without passing through the reals?

Thank you, Norman. > > El dia divendres, 1 d’octubre de 2021 a les 16:36:43 UTC+2, Norman Megill > va escriure: > >> In our construction of the complex numbers, even the "simple" natural >> numbers are complicated objects, and there isn't a simple direct ZFC pro

[Metamath] Re: Is there a proof for "2+2=4" without passing through the reals?

In our construction of the complex numbers, even the "simple" natural numbers are complicated objects, and there isn't a simple direct ZFC proof of 2+2=4 that doesn't require going through the construction, leading to the large number of steps you see. However, there is

[Metamath] Re: How tricky is it to define predicate calculus without equality?

You may want to look at the [Tarski] reference at http://us.metamath.org/mpeuni/mmset.html#bib showing how to formulate predicate calculus without equality on p. 78: Tarski, Alfred, "A Simplified Formalization of Predicate Logic with Identity," Archiv für Mathematische Logik und

Re: [Metamath] would fvexd be a bad idea?

On Wednesday, September 8, 2021 at 7:58:31 AM UTC-4 ookami wrote: > Norm once told me (several years ago!) that the threshold value is 7 > theorems: If the introduction of a convenience theorem affects this many or > more theorems, its value outperforms the downside of having more theorems..

Re: [Metamath] New community verifier?

> Since there was broad agreement to build a community project on Rust, could we move the repository into GitHub's Metamath organization ? Norm, would you agree? ? That's fine by me. Norm On Sunday, August 15, 2021 at 9:23:56 AM UTC-4 Thierry Arnoux wrote: >

Re: HF set theory – Re: [Metamath] Predicate Calculus Functions

In the mmset.html ref. [KalishMontague], p. 81 footnote says: "The fact that (B7') [our ax-6] can be replaced by the weaker axiom (B7) [our ax-6v] is stated implicitly in the abstract [5], where also the rather obvious possibility is mentioned of extending the approach to predicate logic with

[Metamath] Re: List of most frequently used assertions

Feel free to update the comment in your next PR. :) On Tuesday, July 20, 2021 at 5:09:39 PM UTC-4 Alexander van der Vekens wrote: > I think the list of the most commonly referenced assertion in set.mm, > mentioned in the comment of ~syl, is not up-to-date anymore. Running show > usage * for

[Metamath] Re: List of most frequently used assertions

There's no command to show such a list directly, but it can be constructed from information provided by the program. There are many ways to do this (and maybe someone has a better way) but here is one way: MM> open log usage.txt MM> show usage * Statement "a1ii" is not referenced in the proof

Re: [Metamath] Re: Recommendations for metamath hosting?

e. Norm On Tuesday, June 15, 2021 at 10:41:25 PM UTC-4 Norman Megill wrote: > Thanks, Cris. I applied for an an Open Source Account via the link you > provided. We'll see what happens. > > Norm > > On Monday, June 14, 2021 at 9:31:02 PM UTC-4 Cris Perdue wrote: > >&

Re: [Metamath] Re: Recommendations for metamath hosting?

tributors. > > (One way to check disk usage would be to do "du -sh" at the shell prompt > at the root of the website directory tree.) > > > On Mon, Jun 14, 2021 at 4:03 PM Norman Megill wrote: > >> On Saturday, June 12, 2021 at 11:57:47 AM UTC-4 David A. Wheeler

[Metamath] Re: Recommendations for metamath hosting?

On Saturday, June 12, 2021 at 11:57:47 AM UTC-4 David A. Wheeler wrote: > All: > > Does anyone have recommendations for a better hosting site for the main > site us.metamath.org and/or for the build/staging site us2.metamath.org? > Personal experience (or close to it) preferred. Alternatively,

Re: [Metamath] Some questions about AI’s which can generate proofs. I’d welcome any and all answers and feedback :)

On Wednesday, June 9, 2021 at 4:45:08 PM UTC-4 di.gama wrote: > On Wed, Jun 9, 2021 at 11:21 AM Jon P wrote: > ... > Is it true that any AI system built on metamath will need these same >> foundations? For instance it will need a parser for the database, a >> verifier and also it will need a

[Metamath] Re: Planning to change mreexexd in main database.

I think that removing dependence on AC is usually a good thing. Norm On Friday, May 14, 2021 at 4:14:24 AM UTC-4 tbrend...@gmail.com wrote: > You might've already noticed when I posted my first attempt to prove that > the algebraic numbers were a field, but I made a minor change to the proof

Re: [Metamath] Re: Metamath verifier in Lean 4

Done. On Saturday, May 8, 2021 at 7:43:46 PM UTC-4 di wrote: > Could you update the name of the verifier to "mm-lean4"? "Metamath.lean" > is a bit generic (file names in lean 4 have to follow some package-oriented > naming conventions like in java). > -- You received this message because

Re: [Metamath] Re: Metamath verifier in Lean 4

If what you mean is the link in the list of verifiers, I updated it: http://us2.metamath.org/other.html#leanmmverify Norm On Saturday, May 8, 2021 at 7:13:01 PM UTC-4 di@gmail.com wrote: > It's still basically in one file, although now that file is >

[Metamath] Re: [Question on Formalization] How can I write number in base other than 10

Sorry for the duplicate post. I deleted the original to edit a detail that FL didn't want publicly exposed. (In Aug. 2020, Google Groups removed the ability to edit posts.) Forwarded Message Subject: Positional representation Date: Sat, 24 Apr 2021 13:25:26 +0200 (CEST) From:

[Metamath] Re: [Question on Formalization] How can I write number in base other than 10

FL asked me to post this for him. Forwarded Message Subject: Positional representation Date: Sat, 24 Apr 2021 13:25:26 +0200 (CEST) From: frederic.line To: Megill Norman ‌Hi Norm, can you post this mail: To represent numbers in any basis, we can also use finite sequences of

[Metamath] Re: [Question on Formalization] How can I write number in base other than 10

You are right that numbers use only base 10 in set.mm, via the definition df-dec $a |- ; A B = ( ( 10 x. A ) + B ) $. This definition (due to Mario) nicely incorporates decimal number notation into set.mm with a standard definition, without extending the the Metamath language or introducing

Re: [Metamath] Sketchy looking proof shortening

There are several possibilities for defining out-of-domain behavior of function values. We chose the empty set in large part because it is very convenient to have function values exist unconditionally (fvex and consequently ovex). Another possibility is to define out-of-domain function value to

[Metamath] Re: False malware report for metamath.exe executable?

I received a response from Malwarebytes concerning the VirusTotal detection: (begin quote) Our engine format and configuration in VirusTotal is different than our products' default configuration. In VirusTotal we use a command-line engine with more aggressive detection techniques and

[Metamath] False malware report for metamath.exe executable?

The company hosting us.metamath.org flagged metamath.exe as malware and has suspended the site. I have temporarily redirected us.metamath.org to a mirror server. As a precaution, I have also removed copies of metamath.exe from all servers until this is resolved. (It may take a day or two for

Re: [Metamath] On Megill's completeness theorem

I will probably add a check to metamath.exe in "verify markup" to issue a warning if a $d statement has multiple wff and/or class variables (along with a qualifier to skip that check if it isn't desired for some reason). We probably don't want to have "verify proof" (or the initial syntax

[Metamath] World Logic Day 2021

Jan. 14 (Tarski's birthday) is World Logic Day 2021, with on-line events in dozens of countries. http://wld.cipsh.international/wld.html There are many events that might be interesting to general audiences, for example "From Aristotle to the iPhone" by Moshe Vardi: "This talk tells the story

Re: [Metamath] Re: Visualization of proofs with javascript and SVG

On Sunday, December 20, 2020 at 11:13:33 AM UTC-5 Norman Megill wrote: > I like this very much. I think I will add a variable to the $t statement > in set.mm so your base URL can be maintained there, instead of being > hard-coded in metamath.exe. (And Thierry's structured version al

Re: [Metamath] Re: Visualization of proofs with javascript and SVG

I like this very much. I think I will add a variable to the $t statement in set.mm so your base URL can be maintained there, instead of being hard-coded in metamath.exe. (And Thierry's structured version also, which is currently hard-coded.) Give me a week or so. An observation (in Chrome

[Metamath] Re: Proposal for on-going proof minimization

It looks like my proposal wouldn't be welcomed, so I will abandon it. As for keeping a list of minimized theorems, I'm not really in favor of that either; it would be one more thing to maintain that people will forget or neglect. As for mathboxes, we've never had a rule about people

[Metamath] Proposal for on-going proof minimization

In the past, every year or two we would run "minimize_with" on the entire set.mm. But as set.mm has grown, doing this has become a somewhat large project. The last time was in Feb., which involved people volunteering their CPUs over several weeks as well as my time managing it. Benoît

Re: [Metamath] Re: Visualization of proofs with javascript and SVG

When this becomes stable, I can add a link to your version on each theorem page of the main site, like the link that now says "Structured version" for Thierry's pages. This will let you have direct control over your content. (To start with, your base URL would be hard-coded in metamath.exe,

[Metamath] Re: Visualization of proofs with javascript and SVG

I like this. I think that showing explicit substitutions like this could be very helpful to a beginner trying to learn how to follow Metamath proofs. Lest it be forgotten, another experiment that shows explicit substitutions is here:: http://us.metamath.org/mpeuni/_mmbrows2p2e4.png This was

[Metamath] Re: Incorrect definition reference in HTML page for ILE 'wal'

The current web page generation algorithm looks for the next "$a |-" using the syntax. If its label starts with "ax-" the syntax is called "primitive" on the web page. I'll have to add an exception for the case of wal, which I'll try to do in the next release of metamath.exe. df-tru has been

[Metamath] Question from Filip about milpgame proof assistant

Filip asked me to post this. Norm Forwarded Message Subject: New feature of proof assistant Date: Thu, 19 Nov 2020 13:35:16 + (UTC) From: Cernatescu Filip To: Norman Megill Hi Norman! I want to put a question on metamath forum: I was thinking about a new feature

[Metamath] Re: A bird's eye view of (fragments of) propositional calculus in set.mm

Stephen Wolfram has been investigating dependencies between theorems, including Metamath's set.mm, and has written up some findings here: https://writings.stephenwolfram.com/2020/09/the-empirical-metamathematics-of-euclid-and-beyond/ He mentions that ~syl is the most popular set.mm theorem (as

[Metamath] Re: New metamath game on Android

Filip asked me to post the following: Xpuzzle 1.2 has been released. New simple levels have been added, and a new UI has been created. I think that would be a good practice environment for Metamath newbies. -- Filip On Tuesday, September 1, 2020 at 6:18:22 PM UTC-4 Norman Megill wrote

Re: [Metamath] Frege's Begriffsschrift

ocessed > output file mmfrege.html and a PDF. > > On Saturday, July 11, 2020 at 9:15:03 AM UTC-7 Norman Megill wrote: > >> On Thursday, July 9, 2020 at 4:41:43 PM UTC-4, Richard Penner wrote: >>> >>> >>> NM has stated (can't find where) that he would p

Re: [Metamath] Re: Verifying Disjoint Variable Restrictions

In addition to Mario's comments, another way to get a feeling for when $d restrictions are needed is to temporarily delete one of them in set.mm and look at the error message, which gives explicit detail of what is being violated. For example, if we remove "$d x ph $." above 2alimdv and try to

[Metamath] Re: Automatic proof verification

On Thursday, September 24, 2020 at 2:41:00 AM UTC-4 ArndtS... freenet.de wrote: > I'm neither a mathematician nor too familiar with Metamath (more of a > crank really), but I'm wondering whether it is possible to build a program > that automatically checks and financially rewards proofs of

Re: [Metamath] Re: Resources for newbies

On Wednesday, September 9, 2020 at 6:06:31 AM UTC-4 ginx wrote: > Norm: > > Thanks for the reply, I’m definitely going to hang out around here more > often. The 100 theorems is my ideal option, I was scheming the list > provided and some theorems caught my eye, like the four colors one, >

[Metamath] Re: Resources for newbies

On Monday, September 7, 2020 at 12:59:59 PM UTC-4 Norman Megill wrote: > ... > Many of the proofs that Metamath is missing have been done with other > provers. David Wheeler built a list of these, along with how many other > provers have proved the theorem. That can provide

[Metamath] Re: Resources for newbies

Welcome! I wouldn't dismiss the 100 theorem list out of hand. Many of them were done by non-mathematicians with a CS bent. It looks like you have 8 or 9 months to work on this, but even if in the end you discover you bit off more than you can chew, the background material that you do develop

Re: [Metamath] Re: metamath.exe - added "/extract" to "write source"

On Saturday, September 5, 2020 at 6:19:34 PM UTC-4 di gmail.com wrote: > The Metamath -> MM0 importer already contains a feature for selecting > which target theorems you want, so it has the same effect as using /extract > on the source database first and then importing it. I've been using

[Metamath] Re: metamath.exe - added "/extract" to "write source"

On Saturday, September 5, 2020 at 2:46:44 AM UTC-4 Alexander van der Vekens wrote: > That's sound really great! I will try this new feature soon, using the > friendship theorem as "root"... > Good choice. I was curious so I added it (temporarily) here:

[Metamath] metamath.exe - added "/extract" to "write source"

The amount of material in set.mm has grown quite large and may be overwhelming for someone who just wants to see what is needed to prove a particular theorem of interest. Organizing set.mm with section headings and splitting it into modules help but only partially address the problem. "show

Re: [Metamath] Re: Matrix indexing start

On Wednesday, September 2, 2020 at 11:11:57 PM UTC-4 David A. Wheeler wrote: > I think there has been a slow march from one-based indexing to zero based > indexing in computing. > > Many systems designed two decades ago supported one based indexing, such > as R and matlab/octave. But newer

Re: [Metamath] Re: Matrix indexing start

Is the issue here the ability to translate to Lean more easily? On the flip side, there has been some interest in translation from set.mm to Mathematica, which would be more difficult with 0-based matrices. Why there is a need for words in the development of matrices? Is any of this already

[Metamath] Re: Matrix indexing start

I don't want to be the one making the decision on this, in part because I won't be doing the bulk of the work, and I don't really have special expertise in the matter. It just seems that starting at 0 goes against virtually all of published mathematics on matrices. I would feel better if

[Metamath] Fwd: New metamath game on Android

Filip Cernatescu asked me to post this. Forwarded Message Subject: New metamath game on Android Resent-From: nm Date: Tue, 1 Sep 2020 12:22:06 + (UTC) From: Cernatescu Filip To: Norman Megill Hi Norm! I have created an Android App called XPuzzle. It is a puzzle with math

[Metamath] Re: Overloading symbol names

On Sunday, August 30, 2020 at 9:38:20 AM UTC-4 Norman Megill wrote: ... > Up to now we have been careful not to overload the displayed symbols (to > my knowledge). For example, we distinguish various kinds of "+" with > subscripts, unlike most of the literature (wh

[Metamath] Re: Overloading symbol names

On Sunday, August 30, 2020 at 4:53:58 AM UTC-4 Alexander van der Vekens wrote: > > By the way, it seems a little confusing at the first glance that the least > common multiple > is defined by a supremum. Actually, it is an infimum, because the inverse > of > "less than" ` ``' < ` is used to

[Metamath] Re: Overloading symbol names

On Sunday, August 30, 2020 at 4:53:58 AM UTC-4 Alexander van der Vekens wrote: > > In my latest PR, I provided a function mapping a set of integers to their > least common multiple (~df-lcmf: ( _lcm `` s ) ) in addition to the > operation calculating the least common multiple of two integers

Re: [Metamath] Re: Matrix indexing start

While I'm not an expert, my guess is that the major uses of 0-based arrays are in computer science and some computer programming languages, where they can offer an advantage for some algorithms. But mathematics is meant for humans, and humans tend to count from 1. That's why we number the

[Metamath] Re: The version date of set.mm is less recent than the contribution date for imadifss

The comment at the top of set.mm says, "To prevent GitHub merge conflicts, please change the above date only if there are no other pull requests in the queue." Since merge conflicts caused by this been a problem, the Travis check uses the "/top_date_skip" qualifier for "verify markup" so that

[Metamath] Re: Promoting to the main body ad4ant* , ad5ant* and a couple more

You have my approval. Norm On Saturday, August 15, 2020 at 9:17:56 AM UTC-4, Glauco wrote: > > I've taken advantage of some theorems, still in mathboxes. Can I set up a > PR for moving them to the main body? > > Here's the list: > > - supadd from Brendan Leahy's mathbox : sup distributes over

[Metamath] Re: Reworking recursion

On Wednesday, July 29, 2020 at 11:09:40 AM UTC-4, Scott Fenton wrote: > > Hi all, > > I'd like to move my theorem fsumkthpow (giving the value of the finite sum > of powers) into the main body of Metamath, since it's a 100 theorem. > However, that depends on the definition of Bernoulli

Re: [Metamath] Re: Canonical location for Metamath databases

wrote: > > Hi, > > Il 12/07/20 21:42, Norman Megill ha scritto: > > While I expect all of the .mm's will be kept updated in the > > http://us.metamath.org/metamath/ directory indefinitely, I suggest we > > add the missing ones (hol.mm ql.mm demo0.mm miu.m

[Metamath] Re: Proposal: Allow primed class variables in set.mm body (e.g., A')

Sometimes things that may seem useful in a local context may be problematic in the bigger picture. In addition to the posts Alexander pointed to, let me elaborate some of my thoughts. In trying to keep things as simple as possible, we have generally resisted adding things to set.mm (such as

[Metamath] Re: Canonical location for Metamath databases

On Sunday, July 12, 2020 at 1:12:32 PM UTC-4, Giovanni Mascellani wrote: ... > I now want to include some example databases too, in a package called > "metamath-databases". I see that set.mm, iset.mm and nf.mm are > maintained in [1], which can be probably considered their canonical >

[Metamath] Re: More proof shortenings from OpenAI's models

This is nice work Stanislas, thank you. On Friday, July 3, 2020 at 5:09:55 AM UTC-4, Stanislas Polu wrote: - `1re` uses more axioms but is much simpler (how do we feel about > that given the comment there?). > A problem with this particular proof is that it uses df-1, which has the tag "(New

[Metamath] Re: (FL) tensor algebra

Forwarded Message Subject: Tensors Date: Sat, 23 May 2020 14:12:40 +0200 (CEST) From: fl To: Megill Norman Hi Norm, Can you post this: so it seems people agree for a tensor algebra development in the Commons part. If Norm has no further concerns, we can begin -- FL As

[Metamath] (FL) tensor algebra

Forwarded Message Subject: tensor algebra Date: Fri, 22 May 2020 14:05:07 +0200 (CEST) From: fl To: Megill Norman Hi Norm, Can you post that: I want to make some proofs in tensor algebra but I don't want to put them in a mathbox of m'y own. Is it possible to put them in the

[Metamath] (FL) Re: Proposal: Change mmj2's CLI

Forwarded Message Subject: Libraries and text files Date: Sat, 16 May 2020 14:32:08 +0200 (CEST) From: fl To: Megill Norman Hi Norm, Can you post this: Many softwares permit to open two kinds of files. Editors for instance. Especially Emacs. You can open libraries (well the

[Metamath] (FL) Re: Proposal: Change mmj2's CLI

Forwarded Message Subject: Widget again Date: Thu, 14 May 2020 14:42:40 +0200 (CEST) From: fl To: Megill Norman Hi Norm, could you post that: I insist once again: why not adding a widget to open a file from the menu. Mmj2 has already been modified by Mario Carneiro and I see

[Metamath] Re: (FL) Re: Proposal: Change mmj2's CLI

Forwarded Message Subject: Widget Date: Wed, 13 May 2020 12:57:06 +0200 (CEST) From: fl To: Megill Norman Hi Norm, can you post this: I insist. Why not opening the files using a widget accessed from the menu ? There are such standard widgets in every library. They are easy

[Metamath] (FL) Re: Proposal: Change mmj2's CLI

Forwarded Message Subject: Opening files Date: Tue, 12 May 2020 10:41:14 +0200 (CEST) From: fl To: Megill Norman Hi Norm, can you post this: and what prevents from opening the file from a menu and switching between set mm and iset.mm from there. -- FL -- You received

[Metamath] (FL) Words, Commons and binomial

Forwarded Message Subject: Words, Commons and binomial Date: Mon, 11 May 2020 14:37:55 +0200 (CEST) From: fl To: Megill Norman Hi Norm, could you post this: I think all what is related to words should be gathered in the "Commons" part of set.mm so that we can have a

Re: [Metamath] Proposed installation conventions so things will be easier to install (FL)

Forwarded Message Subject: Git Date: Thu, 7 May 2020 11:45:59 +0200 (CEST) From: fl To: Megill Norman Hi Norm, Can you post this: providing only communication through git is not a good Idea. Git should be reserved forp who wants to modify the programs (Metamath or mmj2).

Re: [Metamath] Proposed installation conventions so things will be easier to install

On Tuesday, May 5, 2020 at 12:00:28 AM UTC-4, David A. Wheeler wrote: > > > We could continue to post Metamath-exe with a precompiled binary > and have people store it in C:\metamath. That's not how software > is usually installed on Windows, and it's clunky, but it *works*. There are many

Re: [Metamath] Proposed installation conventions so things will be easier to install

Forwarded Message Subject: Current problem Date: Tue, 5 May 2020 20:19:24 +0200 (CEST) From: fl To: Megill Norman Hi Norm, Can you post this. I don't know how you do, but my own version of mmj2 has no problems to find set.mm in the current directory. -- FL On Tuesday, May

Re: [Metamath] Proposed installation conventions so things will be easier to install

Forwarded Message Subject: Directories Date: Tue, 5 May 2020 11:36:00 +0200 (CEST) From: fl To: Megill Norman Hi Norm, Can you post this. For me it's not "/usr/bin" it's "/usr/local/bin" and set.mm is not a library it's a file of data. You have to be able to browse it and

Re: [Metamath] Proposed installation conventions so things will be easier to install

While I'm not sure of the best way to go forward, let me explain why set.mm and the metamath program are currently in the same directory. A significant number of people are completely unfamiliar with command line interfaces on Windows and don't know how to specify directory paths. Even worse,

[Metamath] Re: FL: Nicod, Sheffer Whitehead and Russell

t; On Thursday, April 30, 2020 at 2:53:03 AM UTC+2, Norman Megill wrote: >> >> FL asked me to post this. >> >> Forwarded Message >> Subject: Nicod, Scheffer Whitehead and Russel >> Date: Wed, 29 Apr 2020 10:58:07 +0200 (CEST) >> From: fl &g

[Metamath] Re: FL: Nicod, Sheffer Whitehead and Russell

, Norman Megill wrote: > > FL asked me to post this. > > Forwarded Message > Subject: Nicod, Scheffer Whitehead and Russel > Date: Wed, 29 Apr 2020 10:58:07 +0200 (CEST) > From: fl > To: Megill Norman > > Hi Norm, > > can you post this: > >

[Metamath] FL: Nicod, Sheffer Whitehead and Russell

FL asked me to post this. Forwarded Message Subject: Nicod, Scheffer Whitehead and Russel Date: Wed, 29 Apr 2020 10:58:07 +0200 (CEST) From: fl To: Megill Norman Hi Norm, can you post this: A complement about Nicod. His paper about his axiom is dated 1916, three years

Re: [Metamath] Re: FL: ++; binary connectives

Posted per FL's request. Forwarded Message Subject: Scheffer stroke Date: Mon, 27 Apr 2020 19:21:36 +0200 (CEST) From: fl To: Megill Norman Hi Norm, can you post this: In the commentary it is saïd that it is Russel and Whitehead who discovered that NAND can be used as the

Re: [Metamath] Packaging Metamath for Linux distros

On Monday, April 27, 2020 at 3:11:43 AM UTC-4, heiphohmia wrote: ... >Previously, at the 0.181 update Giovanni asked you to incant the following: > > git commit -m'Release version 0.181.' > git tag v0.181 > git push > git push --tags > > It looks like this automatically

Re: [Metamath] Packaging Metamath for Linux distros

metamath-program.zip has never been on the home page. It was originally added so Travis could download just the program without being slowed down by unnecessarily including the .mm files, and it is still used for that. Later it also become used for Linux distribution, and the compiled Windows

Re: [Metamath] Re: FL: ++; binary connectives

On Monday, April 27, 2020 at 1:01:56 AM UTC-4, Mario Carneiro wrote: ... > > I know, and this is a bigger issue for set.mm than in the mm0 databases > because these are smaller and more purpose driven. One reason I went with > _c notations for characters is because it is easier to read > > _h

[Metamath] us2.metmath.org

The us2 server may or may not go offline today because of maintenance on the utility lines. 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

Re: [Metamath] Re: FL: ++; binary connectives

Posted per FL's request Norm Forwarded Message Subject: Dijkstra's argument Date: Sun, 26 Apr 2020 17:31:09 +0200 (CEST) From: fl To: Megill Norman Hi Norm, can you post this. Dijkstra's argument doesn't seem to apply to our problem. He is dealing with finding a good

[Metamath] Re: FL: ++; binary connectives

Posted per request of FL. Forwarded Message Subject: Operators Date: Sat, 25 Apr 2020 21:21:07 +0200 (CEST) From: fl To: Megill Norman Let's agree: of course the opinion that we should confine ourselvesto the 5 classical operators for the formulation of the theorems. The

Re: [Metamath] Re: FL: ++; binary connectives

On Saturday, April 25, 2020 at 1:33:20 PM UTC-4, Jim Kingdon wrote: > > With respect to exclusive or, there are a lot of theorems in set.mm which > use ?? <-> -. ?? (examples: sotric , posn , nneo , nltpnft ). At least some > of these can be productively thought of as exclusive or and may

Re: [Metamath] Re: FL: ++; binary connectives

>From FL: Forwarded Message Subject: ++, indices and Commons Date: Sat, 25 Apr 2020 11:53:57 +0200 (CEST) From: fl To: Megill Norman Hi Norm, could you post this: Yes I made a mistake. Scott Fenton uses (++) and not ++. So the symbol ++ is available. I would also

[Metamath] Re: FL: ++; binary connectives

> 1. I have no strong opinion on ++ vs. concat, except that "concat" seems > more self-explanatory. "concat" occurs 373 times in set.mm, so ++ would > save 1492 bytes in set.mm size. > > I'll also mention that Tarski used a frown symbol for concatenation in his 1965 paper. His notation is

Re: [Metamath] Re: Denoting morphisms in set.mm

A scan is attached. On Saturday, April 18, 2020 at 10:56:23 AM UTC-4, David Starner wrote: > > On Sat, Apr 18, 2020 at 7:14 AM Norman Megill wrote: > > > > Regarding: > > > > F : A -1-1-> > F : A >--> B > > F : A -onto->

[Metamath] Re: Can a floating hypothesis become essential?

OK, I'll turn it into a warning. If in the future we determine that it has a legitimate use, we can easily turn off the warning. But the warning will at least notify the user that something very unusual is being done. Norm On Saturday, April 18, 2020 at 10:47:30 AM UTC-4, savask wrote: > > I

  1   2   3   >