metamath/set.mm

Metamath source file for logic and set theory

set.mm's Issues

The Ballot Problem (metamath 100 #30)

Prove The Ballot Problem (metamath 100 #30). 4 other formalization tools have done so.

Mario: This is an elementary combinatorics problem in the same vein as the birthday problem. We probably have the tools for this one now if you use binomial coefficients, but if you use Catalan numbers they will need to be defined first.

2Ideal needs htmldef statement

metamath is throwing this error on set.mm:
?Error: The token "2Ideal", which was defined in a $v or $c statement, was not
declared in an htmldef statement.

Cauchy's integral theorem

Cauchy's integral theorem states that the contour integral around a closed rectifiable path over a holomorphic function on CC is zero.

• Blocks most advanced complex analysis theorems (including the identity theorem and existence/uniqueness of analytic continuations)
• Requires a formalization of path integrals over rectifiable paths on CC

df-sbc update

I am ready to do the df-sbc update. This is a massive change involving about 900 label changes: xxx to xxxSBC for uses of the old df-sbc and xxxNSB to xxx for uses of the new df-sbc. All pull requests need to be closed out and any recent changes by Mario applied. I'll wait to hear from Mario and David.

Norm

Bug 256 when showing HTML in a file which has errors (metamath.exe)

If I am working on a file with several proofs that don't verify, it is pretty common for show statement /alt_html to cause metamath to abort with a BUG 256 message.

I was not able to find a small file which reproduces the problem, but here is a non-small file which does. I've enclosed the file and the sequence of metamath commands. The desired behavior would be for the HTML display to continue to work (possibly with some output like ?Error but with the parts of the page unaffected by the error intact).

iset.mm.txt

$ rlwrap ../metamath/metamath/metamath 
Metamath - Version 0.161 2-Feb-2018           Type HELP for help, EXIT to exit.
MM> read iset.mm
Reading source file "iset.mm"... 1417403 bytes
1417403 bytes were read into the source buffer.
The source has 13506 statements; 139 are $a and 3685 are $p.
No errors were found.  However, proofs were not checked.  Type VERIFY PROOF *
if you want to check them.
MM> show statement snprc
11592 snprc $p |- ( -. A e. _V <-> { A } = (/) ) $= ... $.
MM> show statement snprc/alt_html
Creating HTML file "snprc.html"...
Reading definitions from $t statement of iset.mm...
143 typesetting statements were read from "iset.mm".
Reading HTML bibliographic tags from file "mmil.html"...
?BUG CHECK:  *** DETECTED BUG 256

To get technical support, please send Norm Megill ([email protected]) the
detailed command sequence or a command file that reproduces this bug,
along with the source file that was used.  See HELP LOG for help on
recording a session.  See HELP SUBMIT for help on command files.  Search
for "bug(256)" in the m*.c source code to find its origin.

Press S <return> to step to next bug, I <return> to ignore further bugs,
or A <return> to abort program:  A

The program was aborted.
$ ^C
$ 

Gödel's Incompleteness Theorem (metamath 100 #6)

Prove Gödel's Incompleteness Theorem (metamath 100 #6). 4 other formalization tools have done so.

Mario: Model theory. So many ways to do this one, and all of them require a lot of preparation and potential incompatibilities down the line, so I've been indecisive about this.

Should distinctness be decidable in iset.mm?

That is, do we want an axiom of the sort A. x x = y \/ -. A. x x = y?

Another option is A. x x = y \/ F/_ x y because A. x x = y \/ -. A. x x = y has some possibly undesirable decidability statements equivalent to DECID(the universe has one element) in the absence of dtru. Note that iset.mm doesn't have F/_ yet, but presumably it could (and see #192 (comment) for a bit more elaboration).

Note that ax-i12 states that ( A. z z = x \/ ( A. z z = y \/ A. z ( x = y -> A. z x = y ) ) ) which is along these lines, and it would be even stronger if the last disjunct also had A. x, that is ( A. z z = x \/ ( A. z z = y \/ A. x A. z ( x = y -> A. z x = y ) ) ). In fact that strengthened version of ax-i12 would make fairly easy work of the remaining work on #339 which is the main remaining piece of predicate logic which is unproven in iset.mm.

For past discussion see #362 and #192 .

I (@jkingdon) don't have a particularly good feel for the consequences of these decisions. It is very tempting to say "well of course a variable is just a string of unicode characters (or equivalently, a natural number) and so of course distinctness should be decidable". But saying it that way is almost inviting the parallels to non-Euclidian geometry or intuitionistic logic or other cases where it turned out to be fruitful to make fewer "obvious" assumptions. That is, does adding additional axioms about what a "variable" is restrict the possible models or otherwise rule out useful possibilities?

And on the flip side, what is the advantage of such an axiom? Is it the only way to solve #339 and if not, what kinds of theorems are possible with decidable distinctness but which are not possible without it? Is decidable distinctness independent of the existing axioms? Is it worth examining whether ax-i12 itself is even too strong and what kind of logic would we get if we omitted it or replaced it with an alternative?

Prove Descartes’ Rule of Signs (Metamath 100 #100)

Cramer's Rule (Metamath 100 #97)

Prove Cramer's Rule (Metamath 100 #97). 4 other formalization tools have done so.

Mario says: Needs Determinants, and matrix algebra more generally. Stefan has made some great strides in this direction, with the important theorems about even permutations, but I don't think determinants are ready for use yet.

Need bibliograph entries for Sanford and Lopez-Astorga

How can bibliographic entries be added? I need these:

[Sanford]
If P, then Q: Conditionals and the Foundations of Reasoning
David H. Sanford
Second edition, 2003.
https://books.google.com/books?id=h_AUynB6PA8C&pg=PA39#v=onepage&q&f=false

[Lopez-Astorga]
The First Rule of Stoic Logic and its
Relationship with the Indemonstrables*
Miguel López-Astorga
Tópicos, Revista de Filosofía 50 (2016), 9-23.
http://www.scielo.org.mx/pdf/trf/n50/n50a1.pdf
page 11.

What should we do with classical theorems in iset.mm?

Right now, ax-3 is present but marked with "New usage is discouraged". The whole point, of course, of iset.mm is that we can develop logic without ax-3.

Currently, 414 theorems use ax-3 according to show usage ax-3/recursive, so we should either delete them (and ax-3), or put "(New usage discouraged.)" in them.

The arguments for retaining ax-3 and theorems derived from it are to contrast classical logic with intuitionistic logic (sort of like ax-groth, I guess, although there is probably less danger of accidentally overusing ax-groth or getting confused by its presence). Ideally, there would be a better way to express how different axiom sets relate to each other - like http://wikiproofs.org/w/index.php?title=From_intuitionistic_to_classical_propositional_logic - but in the absence of something like ghilbert-style modules, we're left with approaches like the way we handle the various sets of predicate logic axioms (ax12o and all that stuff). Having said all that, I'd probably lean towards deleting all the classical theorems. How would we refer to classical theorems from the intuitionistic pages if we did that? Would we just link to URLs like http://us.metamath.org/mpeuni/anor.html ?

Add intuitionistic exclusive-or to iset.mm

The discussion so far has been in #316 and #349 but neither one is exactly about the project of adding intuitionistic exclusive-or. I'm tagging this as good first issue because I think some of it is pretty simple although I'm not sure I have a full understanding of which parts are easier or harder.

Basic definitions of xor are now merged (see for example #351 and #357 ). The parts remaining are:

• bring excxor over from set.mm and find an intuitionistic proof
• bring xorass and xorcom over from set.mm (need new proofs but those should be straightforward)
• go over the classical exclusive-or section near the end of iset.mm . Figure out what, if anything, can be intuitionized and bring that into the intuitionistic logic section. Revise the comments for the parts which remain classical to refer to the intuitionistic theorems. Bring it into closer resemblence to current set.mm (use the exclusive-or symbol, for example).
• see what else is in set.mm which might work in iset.mm

ENF transition

Use ENF x : ph in place of ( ph -> A. x ph ) everywhere. See https://groups.google.com/forum/#!topic/metamath/yMgoFfmBnMQ.

Lindemann–Weierstrass theorem (metamath 100 #56)

The Lindemann–Weierstrass theorem states that if if α1, ..., αn are algebraic numbers which are linearly independent over QQ, then e^α1, ..., e^αn are algebraically independent over QQ. Definitions df-aa and df-algind may be helpful in writing the statement. Metamath 100 theorem # 56.

• Blocks Metamath 100 theorem # 53 (pi is trancendental)
• Blocks Metamath 100 theorem # 67 (e is trancendental)

Flesh out exclusive-or in iset.mm

We now have a definition (df-xor) and a number of theorems concerning exclusive or.

I'm tagging this as good first issue since some of it is definitely easy (and the rest probably is, but might involve a little more figuring out what the theorems should be).

Remaining known tasks are:

• bring xorass and xorcom over from set.mm (need new proofs but those should be straightforward)
• figure out what to do with xordi. Does ( ( ph /\ ( ps \/_ ch ) ) <-> ( ( ph /\ ps ) \/_ ( ph /\ ch ) ) ) hold or is this theorem, or some variation thereof, dependent on some propositions being decidable?
• go through xor related theorems in set.mm and see if there are any more which should be brought over, either as-is or with decidability conditions added.

This issue replaces #350 and also builds on #405 (and other xor work to date).

Add decidability connective to iset.mm

As discussed in some comments on #350 it would be good to have a notation for decidability. This can be used as an antecedent or a hypothesis (which probably will be a more graceful way to display classical results than to try to keep track of what does and does not depend on ax-3).

Decidability can also be used as a conclusion (if a formula implies the decidability of an arbitrary proposition, then that formula cannot be a theorem of intuitionistic logic).

My work in progress is here: https://github.com/metamath/set.mm/compare/develop...jkingdon:decidability-connective?expand=1 but before I make that into a pull request, I would like comments on:

1. Notation. One option at #350 (comment) was LEM ph but that strikes me as confusing, since the Law of the Excluded Middle (LEM) is generally taken to be the assertion that all propositions are decidable, rather than being about decidability of a particular proposition. I also considered DECIDABLE ph but my current branch has DECID ph which I was thinking is a compromise between the explicitness of DECIDABLE ph and something even more concise (I'm a little cool on something very concise, given that there isn't a standard notation for this that I know of, short of ph is decidable in words).

2. Anything about the syntax or semantics of this definition. It seems straightforward (with the syntax being very much like -. and the semantics being, well, just like ph \/ -. ph). But I won't claim to be any flavor of expert.

3. Typesetting. Right now it typesets with small caps DECID next to the formula and spacing similar to ¬ (so DECID x = y is typeset similarly to ¬ x = y). Coming up with something which people find readable is relevant to whether this is a good notation.

4. Anything else?

Prove irreflexivity of set membership in iset.mm

In set.mm we have elirrv which is proved from ax-reg. The question is whether we can prove it in iset.mm from ax-setind. If so, this unlocks a number of theorems (some listed at #629 which takes irreflexivity of set membership as a given).

Most literature I know on this subject is for classical logic (and does not proceed from set induction but from one of the classically equivalent formulations of the axiom of foundation). Presumably there is an intuitionistic proof published somewhere but I'm not even sure where I'd look for it. Or I can just see whether @digama0 immediately sees it off the top of his head 😉 .

Proving irreflexivity, given a well-founded relation, but without assuming the axiom of set induction, is presumably similar but separate: see #646

Principle of Inclusion/Exclusion (metamath 100 #96)

Prove Principle of Inclusion/Exclusion (metamath 100 #96).
4 other formalization tools have done so.

Mario: Multivariate binomial theorem, not a particularly hard proof with the "new" (not really that new) finite sums notation. Closely related to the fundamental theorem of symmetric polynomials, which ties up with matrix algebra.

Make iset.mm typesetting match set.mm

This should be relatively straightforward, just a matter of comparing the typesetting section (htmldef, latexdef, etc) between the two. We can take set.mm as the authority as to what we want to do.

A more ambitious way of approaching this would be to somehow sync the two in a more automated (or semi automated) way, probably using the split files features in recent versions of metamath. As a question of policy, I don't think there is any need for the two to have different typesetting for the same syntax (although there are tokens which only exist in iset.mm, DECID at least, and a larger number which only exist in set.mm).

Multi-file transition: making it happen

Synopsis

Create tools to convert between a multi-file representation of the database and a single-file representation. Ensure they can round-trip, including after a WRITE SOURCE from metamath.exe.

Convert this repository to the multi-file format, with a filter-branch to avoid any large objects in the history.

Rationale

Most style guides recommend keeping source code files in computer programs under 1000–5000 lines, for industrial-psychology reasons. set.mm is not really a computer program and those rules are not applicable as such, but it's similar enough to one that we want to use many of the same tools, including git, git-based change visualizers, and programmer-oriented text editors. However, those tools are optimized for a world where "large projects" like the Linux kernel consist of many relatively small files (v4.6 has 22787 *.c files, median 354 lines, 99th percentile 4836 lines). Some of them can handle a single 29MB file just as easily; others not so much.

Also, we are moving deeper and deeper into a world where individual developments don't depend on the whole available database. Tooling today struggles to maintain responsiveness with the whole database, and this will only get worse. We need to be able to point tools at subsets of the database, and the most natural way to do that (IMO) is by pointing tools at a subset of the files.

Since the biggest (current!) problems with the large file are related to the git repository, any solution must involve converting the git repository. Additionally, backdating the conversion will make initial clones much happier.

What the database will look like

We already have a facility in the Metamath language to spread a database across several files, the file-inclusion mechanism, and I want to minimize the amount of ecosystem fragmentation this change creates so I will be using that same mechanism. There are two ways that can look:

1. Dependency graph:

   $( basics.mm $)
   ...
   $( topology.mm $)
   $[ basics.mm $]
   ...
   $( polynomials.mm $)
   $[ basics.mm $]
   ...
   $( polynomials_are_continuous.mm $)
   $[ topology.mm $]
   $[ polynomials.mm $]
   ...
   

2. "Project file"

   $( basics.mm $)
   ...
   $( topology.mm $)
   ...
   $( polynomials.mm $)
   ...
   $( polynomials_are_continuous.mm $)
   ...
   $( top.mm $)
   $[ basics.mm $]
   $[ topology.mm $]
   $[ polynomials.mm $]
   $[ polynomials_are_continuous.mm $]
   

The "dependency graph" approach makes it easier to work with subsets, but "project file" is better suited to automatic round-trip conversion. I'll probably start with the latter then make another ticket later to switch to the first.

Tooling requirements

Some tools will prefer the single file. Some users of tools that are themselves neutral prefer the single file. Some tools presently require the single file; in particular, the only tool that can currently make automated semantic changes to Metamath databases, metamath.exe, supports reading collections of files but will always write as a single file.

To support both use cases, tools will be created to convert back and forth between single-file and multi-file. Actually, we already have a splitter program, but it got little buy-in. I assume the reason for that is the difficult Node.js/Babel.js installation story, and a SMM3-based converter which could be distributed as a single statically-linked binary might be better received? (Metamathicians, is this a fair assessment?)

When?

That's the question. This ticket exists so that we can determine when the tooling requirements are met and coordinate a time for the mass filter-branch and force push.

Merge developments of R^n

On Thursday, April 7, 2016 at 8:34:08 AM UTC-4, fl wrote:

I think that ( RR ^N ) and ( CC ^ N ) in my mathbox or what is related to euclidean spaces in Madsen's mathbox deserve to be made official.

The version I would prefer to see (personal taste only) is R^n and C^n as Hilbert spaces, meaning the structure product of n copies of RR or CC with an inner product and induced norm. This will allow for reusing structure theorems for groups, vector spaces etc. (which FL's mathbox version doesn't do) and will also allow dealing with the inner product structure (which supercedes JM's definition of the norm).

If you like Madsen's mathbox version, an easy way to get it into main is just to use it in your mathbox. Since mathboxes are independent, any common work will be moved up.

That said, I'd really like to have some theorem that depends essentially on the structure being R^n / C^n to justify the definition. So far it's all statements that apply to all vector spaces or all Hilbert spaces. Madsen's proof that boundedness is equivalent to total boundedness in R^n is a good example, but if it's just the one theorem it is not really worth it.

As you say, we currently have three versions of R^n in the database. The only way this will be moved up is if someone takes it upon themselves to unify all three developments, meaning that a new development (or extension of one of these three) must encompass all the major results of the other two developments.

The Tarskian geometry approach is interesting, but I think your "planar incidence geometry" approach is the better one. Essentially, define the geometry axioms in general and form a new structure for them (and prove what results you can from this structure), then show that R^n has a compatible structure, so that R^n acquires the geometry theorems. (EDIT: I don't mean to suggest here that Aitkin's axioms for planar incidence geometry are better than Tarski's, but rather that we should use the "axiomatic" approach which is not R^n-specific - this applies equally to either axiomatization.)

Add support for Euclidean Geometry

I think it'd be possible to select some well-known set of "axioms" defining 2D/3D Euclidean Geometry, e.g., those by Hilbert, Tarski, or Birkhoff. Then you can build up to usual Side-Angle-Side (SAS), Angle-Side-Angle (SAS), Side-Side-Side (SSS), and CPCTC... and then many other proofs would become much easier (because they can be expressed as traditional Euclidean geometry proofs). E.g., the isosceles triangle theorem would be trivial to prove with these tools. It seems to me it'd be possible to connect existing axioms to Euclidean geometry, just as numbers are "created" from set and logic axioms. I'm sure there are implications I'm not thinking of, but I thought I'd record the idea here.

How do I contribute to mmil.html?

Hey, before I put this in pull request form, just wanted to check whether this is the right place.

I came up with an expansion to mmil.html (basically, a start on an axioms section for intuitionistic propositional logic) which can be found here; digama0/set.mm#1

I'm not quite sure what version of mmil.html I should be starting from or how I should be formatting my submission (or even whether that file is generated from something else, for that matter). I'd be glad to do some of that if I can usefully do so,, or alternatively, just take a look at the diff at the above URL if that is sufficient.

As for my larger interests, I wrote the intuitionistic proofs and text over at http://wikiproofs.org/w/index.php?title=Category:Subsystems_of_classical_logic and would love to bring that to a larger community with more mature tools. I'd also like to look into type theory of various kinds, although that's a bigger topic (partly because I'm still learning type theory, partly because how to fit it into metamath is, I guess, less obvious than intuitionistic propositional/predicate logic).

Thanks,

Jim

Prove Taylor's Theorem (metamath 100 #35)

Taylor's theorem has a few possible statements. One form states that if f : R -> R is a function k-times differentiable at a e. R, then there exists a function h : R -> R such that h(a)=0 and h is continuous at 0, and f(x) = (sum_ n e. (0...k) f^(n)(a) (x-a)^n / n!) + h(x) (x-a)^k . (This is called the Peano form of the remainder.)

This is Metamath 100 theorem # 35. This is one of the most commonly-proved theorems by formalization tools (7 others), but not by Metamath.

This only needs calculus and power series work, mostly all there.

L'Hôpital's Rule (metamath 100 #64)

Prove L'Hôpital's Rule (metamath 100 #64). 5 other formalization systems have proven it.

This one is mostly annoying for its various special cases involving
different kinds of limits. Otherwise, it's probably simpler than Taylor's theorem.

Quotient lifting pattern

Currently, there are several places where maps from a quotient are used, e.g. frgpupval, orbstaval, pi1coval, and others where the quotient is implicit with a function e.g. cygznlem2. Currently, the well-definedness condition is being rederived in each case, but they have a common structure that can be extracted.

These can be replaced by the pattern

|- F = ran ( x e. X |-> <. A , B >. )

which is the function such that ( F ` A(x) ) = B(x), provided that the well-definedness condition A(x) = A(y) -> B(x) = B(y) is satisfied. In the special case where the function is being defined over an equivalence relation, this can be replaced with

|- F = ran ( x e. X |-> <. [ x ] R , B >. )

where now the well-definedness condition is x R y -> B(x) = B(y), and it satisfies ( F ` [ x ] R ) = B(x) in this case.

This idiom has the advantage that it requires no dummy variables other than the essential ones, and does not need an iota construction.

pm11.07 in set.mm is not what it appears to be

The distinct variable constraints in http://us2.metamath.org:88/mpeuni/pm11.07.html make the theorem a trivial one, which has little application.

The distinct variable constraints between 𝜑 and 𝑥, and between 𝜑 and 𝑧, mean that both sides of the theorem ([𝑤 / 𝑥][𝑦 / 𝑧]𝜑 and [𝑦 / 𝑥][𝑤 / 𝑧]𝜑 immediately simplify to 𝜑 (via nfv and sbf and the usual machinery around sbbii and biconditional transitivity).

In case the above is unclear, here's the trivial proof above as a metamath compressed proof of pm11.07 (this is for the 20-Jan-2018 version of set.mm but applies with slight changes to iset.mm too):

$=    ( wsb nfv sbf sbbii bitri bitr4i ) ADCFZBEFZAADEFZBCFZMABEFALABEADCADGZHI
      ABEABGZHJOABCFANABCADEPHIABCQHJK $.

As for what *11.07 in Principia really is, here is the text from page 152 of https://ia600602.us.archive.org/35/items/PrincipiaMathematicaVolumeI/WhiteheadRussell-PrincipiaMathematicaVolumeI_text.pdf :

*11·07. "Whatever possible argument x may be, 𝜑(x,y) is true whatever possible argument y may be" implies the corresponding statement with x and y interchanged except in "𝜑(x, y)". Pp.

I don't think I can confidently turn that into metamath notation. The translation given in pm11.07 might be roughly correct with different distinct variable constraints, or it might just map to the fact that metamath theorems are all (implicitly) theorem schemas, or perhaps something else.

As for what to do about it, perhaps just delete pm11.07? The history seems to say this came from a mathbox originally, don't know if that user is still active or if anyone else wants to pick up the baton.

Isosceles Triangle Theorem (metamath 100 #65)

A triangle has two equal sides iff it has two equal angles. This can also be stated w.r.t a specific vertex on the triangle. Metamath 100 theorem # 65.

Change mpt2 to mpo

Does anyone object to changing the label fragment for two-argument mapping from mpt2 to mpo? The former often conflicts with numbered theorems about single argument mapping. It has also been mentioned as a proposal at the top of set.mm for many years, where it is also accompanied by a proposal to change mpt to mpf. How do people feel about these changes?

Current status (August 2023, by @jkingdon ): mpt2 to mpo rename is underway. Remaining tasks:

• finish renaming theorems in set.mm
• finish renaming theorems in iset.mm (there's at least one which isn't also in set.mm)
• update comment for section "Special maps-to operations" above opeliunxp2f - both set.mm and iset.mm
• update proposed renames entry in changes-set.txt
• update references in missing theorems list in mmil.html
• update reference in mmnatded.raw.html
• update references in mmnotes.txt

Additional Definitions/Theorems for Words

In my Mathbox, I provided some additional definitions and many additional theorems about Words (df-word), see section 19.23.4 "Additional definitions and more theorems about Words". I would propose to take them over into the main part of set.mm.

Doing this, the sections 5.6.9 "Words over a set" and 5.6.10 "Longer string literals" should be restructured. I would propose the following structure (lifting up the section 5.6.9 by one level, incrementing the number of the following sections by 1):

5.7. Words over a set
5.7.1 Definitions and basic theorems
5.7.2 Last symbol of a word
5.7.3 Singleton words
5.7.4 Concatenations of words
5.7.5 Concatenations with singleton words
5.7.6 Subwords
5.7.7 Subwords of subwords
5.7.8 Subwords of concatenations
5.7.9 Splicing words (substring replacement)
5.7.10 Reversing words
5.7.11 Cyclic shifts of words
5.7.12 Longer string literals

What is your oppinion about this? I think Words are used very often in other Mathboxes, so we can collect the common "knowlegde" in the main part.

Use iota consistently

Currently, there are five variants on "the unique element such that ph" in use, namely (1) U. { x | ph }, (2) U. { x e. A | ph }, (3) ( iota x ph ), (4) ( iota x ( x e. A /\ ph ) ), (5) ( iota_ x e. A ph ). We should adjust the library to encourage the forms (3) and (5) and eschew the others. ((1) and (3) are the same, as are (2) and (4); (5) is almost the same as (2),(4) except in the handling of non-unique properties. Personally I would prefer to define (5) to equal (4), but this is a separate issue. While this definitional difference exists, (4) can be used when the difference is important.)

Prove Laws of large numbers (Metamath 100 #59)

Prove the laws of large numbers, #59 on the metamath 100 list.

It's not clear which laws were meant; I'm guessing that at least the "weak" and "strong" ones were meant. Summary here:
https://en.wikipedia.org/wiki/Law_of_large_numbers

A summary of these laws, along with summaries of their dependencies and sketches of proofs, are here: http://www.math.uah.edu/stat/sample/LLN.html

Note: No formal math proof system has proved this to date - not even HOL Light. I'm adding an issue anyway because I started looking into this, and wanted to create a place for people to record hints and pointers to help.

Does Travis check run before or after a tentative merge?

In develop commit ecfef6d, the Travis check passes

Reading source file "set.mm"... 32541516 bytes
32541516 bytes were read into the source buffer.
The source has 147512 statements; 2150 are $a and 30795 are $p.
No errors were found.  However, proofs were not checked.  Type VERIFY PROOF *
if you want to check them.
MM> verify proof *
0 10%  20%  30%  40%  50%  60%  70%  80%  90% 100%
..................................................
All proofs in the database were verified in 4.66 s.

If I copy the set.mm file of commit ecfef6d and run locally, I get

Reading source file "copied-set.mm"... 32649120 bytes
32649120 bytes were read into the source buffer.
The source has 147926 statements; 2150 are $a and 30852 are $p.
No errors were found.  However, proofs were not checked.  Type VERIFY PROOF *
if you want to check them.
MM> v p *
0 10%  20%  30%  40%  50%  60%  70%  80%  90% 100%
................................
?Error on line 381432 of file "copied-set.mm" at statement 95065, label "f1od2", type
"$p":
      csb cvv sbcbidv sbcan wb fvex ax-mp sbcel1gv anbi12i bitri sbceq2g sbcbii
                                          ^^^^^^^^
This token is not the label of an assertion or optional hypothesis.
..................

Based on file size, it looks like Travis checked the set.mm already in the develop branch before the merge. The merged set.mm correctly fails due to a label change.

Is this the expected behavior? I don't recall seeing this before, or maybe we have just been lucky.

(PS I fixed this error in commit 83d92df, which was because I renamed sbcel1gv to sbcel1gvOLD; Thierry, you don't need to concern yourself with it. I will take care of updating it to the sbcel1gv replacement.)

Norm

Add pm2.18da to iset.mm

I quickly brought over many theorems that correspond to common natural deduction rules that are valid in intuitionistic logic. However, I did not bring in pm2.18da as that didn't just copy over. iset.mm does have pm2.18dc, so it might be easy to convert.

Merge develop into master

The latest development branch has lots of goodness, however, it's not obvious because the default branch is 'master'. Simple solution: at some point, merge develop into master.

Prove extra axioms of intuitionistic propositional logic in set.mm

There is a section of set.mm (currently 1.8.3) which proves statements of predicate logic which are theorems in set.mm but axioms in iset.mm.

We should do the same for propositional logic (this would be a good beginner project if anyone wants to get started with metamath, but if no one picks it up, I eventually will).

Here's a summary of the situation from Gérard Lang:

Four of them are already provided as follows: axia1 is simpl
(443), axia2 is simple (447), axia3 is pm3.2 (434) and axin2 is pm2.21
(100).
Concerning the two last axioms ax-in1 and ax-io, [Gérard Lang] only found partial
results like pm2.02 (160) for ax-in1, and jao (498) and prth (554), but
no exact proof of theorems axin1 and axio.

Prove sbco2, hbsb, sbco3 and related theorems in iset.mm

We are one distinct variable constraint away from having these. See sbco2v, hbsbv, and sbco3v for versions with the extra constraint. In classical logic, it is possible to prove two cases, where a pair of variables are identical or where they are distinct, and use pm2.61 to get the desired result. In intuitionistic logic, one needs a disjunction (a la nfsb2or), direct application of ax-i12, or some other technique.

We can also add sbcom to the list of theorems in this family; see #348 for the connection with sbco3.

Feel free to ask me (@jkingdon) for more background on what I have tried or discovered. But also feel free to try new things, because so far the breakthroughs have come in ways that have been hard for me, at least, to anticipate.

Oh, and if you do make progress, submitting frequent pull requests is encouraged. There may be other people working on this or closely related things.

The Area of a Circle (metamath 100 #9)

Prove the Area of a Circle (metamath 100 #9).

Prove moabex in iset.mm

http://us.metamath.org/mpeuni/moabex.html is a theorem in set.mm which we do not have (yet at least) in iset.mm but which seems potentially provable.

The weaker version http://us.metamath.org/mpeuni/euabex.html is easy to prove:

${
  $d y x $.  $d y ph $.
  $( The abstraction of a wff with existential uniqueness exists.
     (Contributed by NM, 25-Nov-1994.) $)
  euabex $p |- ( E! x ph -> { x | ph } e. _V ) $=
    ( vy weu cab csn wceq wex cvv wcel euabsn2 vex snexg ax-mp mpbiri
    cv eleq1 exlimiv sylbi ) ABDABEZCPZFZGZCHTIJZABCKUCUDCUCUDUBIJZUA
    IJUECLUAMNTUBIQORS $.
$}

As for how to prove moabex the following are things we can show:

1. From mo3, elsn and logic:

|- ( E* x ph
   <-> A. x
         ( ph
          -> A. y
                ( [ y / x ] ph -> y e. { x } ) ) )

2. { x | ph } = { y | [ y / x ] ph } follows from cbvab

3. We do have some potentially helpful theorems like abss and ss2ab.

I can't really tell whether those are on the right track or not. At times it seems like moabex should just be a few easy steps away, at other times it feels like I'm running right into "there are two cases: the set has one element or it has none" or other territory which won't work.

As for why it would be useful, moabex would lead to snex and other good stuff.

Add well-founded predicate to iset.mm

Right now iset.mm does not have a well-founded predicate (Fr in set.mm). This means that some ordinal theorems may require the Axiom of Set Induction (the IZF equivalent to the Axiom of Foundation/Regularity in ZF). Being able to do some of this development without that axiom is the purpose of the well-founded predicate in set.mm (if we assume regularity/foundation in classical logic, set membership is well-founded on any class - see zfregfr in set.mm).

Presumably the "right" notion of well founded is the inductive one, that is, a property that satisfies the epsilon (or R) induction principle is always true. To state this in set theory, you can say something like this:

R Fr A <-> A. s ( A. x ( A. y ( y R x -> y e. s ) -> x e. s ) -> A C_ s )

This definition has some problems when A is a proper class. As such, ax-setind has to be stated as a schema instead:

A. x ( A. y ( y e. x -> y e. S ) -> x e. S ) -> S = _V

There are two ways to say no infinite descending sequence, using E. -. or -. A., which are not intuitionistically equivalent. Furthermore there are some trivial commutations that are not intuitionistically valid. So I think that makes the following definition possibilities:

R Fr A <-> A. s ( A. x ( A. y ( y R x -> y e. s ) -> x e. s ) -> A C_ s )
R Fr2 A <-> A. s ( s C_ A -> ( A. x e. s E. y e. s y R x -> s = (/) ) )
R Fr3 A <-> A. s ( s C_ A -> ( E. x x e. s -> E. x e. s A. y e. s -. y R x ) ) 

The set.mm definition is roughly Fr3 (but it uses nonempty in place of inhabited). We can probably just focus on the first definition, but ideally we'd prove it in set.mm (to show that in classical logic it is equivalent to the definition of Fr in set.mm).

(some of this description was adapted from an email by @digama0 ).

Add intuitionistic existential uniqueness to iset.mm

The current treatment of existential uniqueness depends on ax-3 quite heavily.

Existential uniqueness is, at least conceptually, related to exclusive-or, and iset.mm now has an intuitionistic treatment of exclusive-or (see #406 for more on that).

None of df-eu, eu1, eu2, or eu3 are obviously non-intuitionistic, so it is not known that anything fundamental needs to be changed. But one way or another, there is a lot of ax-3 usage currently.

Expand ordinals in iset.mm

This is based on #626 (comment) but omits most theorems which are described there as not provable. It also omits theorems which have been proved since that comment was written.

• onprc: provable (and this is an important one, the Burali-Forti paradox). Follows easily from ordon. (haven't spotted this proof yet. The set.mm proof of onprc depends on ordon and ordirr and we don't yet have the latter in iset.mm) has been proved

• onint: provable if you assume A is inhabited (looks like we need a variant of tz7.5 for inhabited rather than non-empty) not provable

• onint0: not in original comment but looks like in addition to onint it may need a bit more work not provable

• onssmin: provable if you assume A is inhabited (this will substitute for most proofs by well foundedness) set.mm proof uses onint not provable

• onminesb, onminsb: provable set.mm proof uses onint not provable

• oninton (with non-empty changed to inhabited): This one I think can still be salvaged though. From the fact that it is inhabited you get that it exists, and is a subset of an ordinal x. It is an intersection of transitive sets so it is transitive, and of course all its members are members of x so they are transitive too. And E. Fr A falls to subsets.

• onintrab, onintrab2: provable set.mm proof uses oninton

• onnmin: May be able to replace trichotomy with irreflexibility. If B e. A and B e. |^| A, then |^| A C_ B so B e. B, violating ordirr.

• onminsb set.mm proof relies on trichotomy

• oneqmin: provable if B is inhabited, and you replace -. x e. B with B C_ x

• onminex falls as written because it implies onint, but it might be useful to keep the reverse direction for subsets that do have a minimum.

• sucon: provable The set.mm proof will work if we get onprc

• ordsuc. The set.mm proof relies on case elimination (on whether A is a proper class). Proved for the A e. _V case in #641

• ordpwsuc: not provable, but interesting. I think suc' A = ( ~P A i^i On ) may play a role later on, it might be worth having both notions. suc A C_ suc' A, and both are ordinals. Not sure I have an opinion yet about introducing a notation for suc' but at a minimum we can prove a variant of ordpwsuc which has subset rather than equality in the consequent.

• sucelon see #641

• onpsssuc: provable (for both suc's)

• ordsucss, ordelsuc see #636

• onsucmin: provable for suc, not suc'

• ordsucelsuc: provable with suc on the left and suc' on the right. This could be a problem... there might be some one directional versions here too.

• ordsucsssuc: provable for suc, the proof is a bit complicated and uses injectivity of suc. For suc' it is provable and easy.

• ordsucuniel: provable

• ordsucun: not provable in the forward direction (implies some order totality)

• ordunisuc: provable

• orduniss2: provable (hey look, it's ordunisuc')

• onsucuni2: provable for both suc's

• 0elsuc: provable for both suc's

• limon now proved, see #634

• onuninsuci, ordununsuc: not provable in the reverse direction We should prove the forward direction if we can then.

• onsucssi: provable

• nlimsucg: provable

• ordunisuc2: provable (and nicely intuitionistic), works for both suc's see comments below

• A e. B <-> suc A C_ B for ordinals. See comment below. proved as ordelsuc in #636

• ord0eln0 seems like this should hold when non-empty is changed to inhabited but how to prove it? set.mm proof relies on trichotomy.

• dflim4: use this as the definition

• limsuc: provable

• limsssuc: provable

• limuni: provable if you assume A is inhabited

Proposal: Move Stoic logic from David A. Wheeler's mathbox

I suggest adding Stoic logic, which is about 2000 years old, from the "Stoic logic indemonstrables (Chyrysippus of Soli)" section in my mathbox. The more obvious place to put it is the "Other axiomatizations of classical propositional calculus" section. It could be added just before the "Predicate calculus mostly without distinct variables".

Stoic logic used 5 axioms. Two are already there;

• modus ponendo ponens (modus ponens) - already an axiom in ~ ax-mp ,
• modus tollendo tollens (modus tollens) - already proven as a derived theorem in ~ mto ,

Here are the others, which are all provable from the existing axioms:

• modus ponendo tollens I ~ mpto1 ,
• modus ponendo tollens II ~ mpto2 , and
• modus tollendo ponens (exclusive-or version) ~ mtp-xor (original Stoic logic version)
• modus tollendo ponens (inclusive-or version) ~ mtp-or (what the name now more commonly means; I haven't found when this shift occurred, because a lot of people aren't careful to disinguish between the 2 kinds of "or"s, but I think it was in antiquity)

It would be quite possible to add "(New usage is discouraged.)" On the other hand, these theorems have ancient names and are much better known than the ones that are currently used, and it wouldn't be surprising if they are quite useful - there's no specific reason their use needs to be discouraged. They have the advantage of being "intuitive" to many people (as evidenced by their early identification).

"SHOW RESTRICTED" in Travis

The latest version of metamath.exe includes a command SHOW RESTRICTED that will allow us to verify that (New usage/Proof modification is discouraged.) marks are honored. Norm writes:

I finished implementing the "is discouraged" markup in metamath.exe and will release it after some more testing.

For comparing set.mm to previous versions, I decided against reading two files in metamath.exe because I think external scripting of the diff can provide more flexibility. A new command, "show restricted", simply lists all statements containing the "discouraged" comment markup for diff comparison with a previous set.mm. I think you mentioned this was sufficient for a travis script.

Comparing proofs is somewhat problematic because changing labels and reordering hypotheses can make them mismatch completely. One thing that is constant is the number of steps, so I am listing that instead of the actual proof. In practice, I think this is sufficient to detect 99.99% of overridden proofs because it seems very unlikely that a revised proof would have exactly the same number of steps. For the use case I'm most concerned about, minimize_with, the number of steps would always be different.

Here is a sample session. I prefixed each line with the string "SHOW RESTRICTED:" for easy identification of the lines with a script.

To make diff results easier to interpret, I am listing each usage on a new line with both the original statement and its target.

--- begin sample session ---

MM> help show restricted
Syntax:  SHOW RESTRICTED

This command shows the usage and proof statistics of statements with
"(Proof modification is discouraged.)" and "(New usage is
discouraged.)" markup tags in their description comments.  The output
is intended to be used by scripts that compare a modified .mm file
to a previous version.

MM> show restricted
SHOW RESTRICTED:  Proof of "id1" is restricted (26 steps).
SHOW RESTRICTED:  Proof of "dfbi1gb" is restricted (100 steps).
SHOW RESTRICTED:  Proof of "jcabOLD" is restricted (42 steps).
SHOW RESTRICTED:  Usage of "jcabOLD" is restricted (0 uses).
SHOW RESTRICTED:  Proof of "pm3.43OLD" is restricted (17 steps).
SHOW RESTRICTED:  Usage of "pm3.43OLD" is restricted (0 uses).
SHOW RESTRICTED:  Proof of "con3th" is restricted (65 steps).
SHOW RESTRICTED:  Proof of "tru2OLD" is restricted (9 steps).
SHOW RESTRICTED:  Usage of "tru2OLD" is restricted (0 uses).
SHOW RESTRICTED:  Usage of "ax-meredith" is restricted (13 uses).
SHOW RESTRICTED:  "ax-meredith" is used by "merlem1".
SHOW RESTRICTED:  "ax-meredith" is used by "merlem2".
SHOW RESTRICTED:  "ax-meredith" is used by "merlem1".
SHOW RESTRICTED:  "ax-meredith" is used by "merlem2".
SHOW RESTRICTED:  "ax-meredith" is used by "merlem3".
SHOW RESTRICTED:  "ax-meredith" is used by "merlem4".
SHOW RESTRICTED:  "ax-meredith" is used by "merlem5".
SHOW RESTRICTED:  "ax-meredith" is used by "merlem7".
SHOW RESTRICTED:  "ax-meredith" is used by "merlem8".
SHOW RESTRICTED:  "ax-meredith" is used by "merlem9".
SHOW RESTRICTED:  "ax-meredith" is used by "merlem10".
SHOW RESTRICTED:  "ax-meredith" is used by "merlem11".
SHOW RESTRICTED:  "ax-meredith" is used by "merlem13".
SHOW RESTRICTED:  "ax-meredith" is used by "luk-1".
SHOW RESTRICTED:  "ax-meredith" is used by "luk-2".
SHOW RESTRICTED:  "ax-meredith" is used by "luk-2".
SHOW RESTRICTED:  Proof of "merlem1" is restricted (62 steps).
SHOW RESTRICTED:  Usage of "merlem1" is restricted (3 uses).
SHOW RESTRICTED:  "merlem1" is used by "merlem2".
SHOW RESTRICTED:  "merlem1" is used by "merlem5".
......  etc. .............

This command can easily be converted to a usage generator script:

 ./metamath 'read set.mm' 'show restricted' exit | grep 'SHOW RESTRICTED' > set.usage

will calculate the usage in set.mm and output it to set.usage. Treated as a function from mm files to usage files, whenever a change is introduced that changes the usage output, this change ought to be marked as "override" or something similar.

The problem is that Travis is not designed for evaluating a build in the context of previous builds. It's not that it's impossible - it's as simple as checking out the HEAD^ version of set.mm and comparing the generated set.usage files. But if this fails, it represents a non-repeatable "error", since pushing the exact same commit a second time will resolve the failure.

One way to solve this is to store the usage file in the repo. Then the correctness check that can be performed by Travis is that the generated usage matches the stored usage file, and the equivalent of an "override" in this context is an update to the usage file in the commit using the above command. This does mean that anyone who is not capable of running this command (adapted for their platform) will not be able to override usage checks, but this seems like a reasonable compromise.

Thoughts?

Category theory

Some work is needed to unify existing developments of category theory in FL's mathbox with the rest of extensible structure-based formalism in main set.mm.

Add more T. (true) and F. (false) theorems to iset.mm

I ran search * 'T.' and search * 'F.' in set.mm and found a lot of theorems which are not in iset.mm yet. The vast majority hold intuitionistically, and the proofs probably aren't especially hard. In some cases the proofs from set.mm will work unmodified.

This would be a good beginner project for someone who is learning logic or metamath.

Order theory import

Import some of Norm's general order theory definitions into main set.mm.

Request: Document how to "Intuitionize" in iset.mm's documentation

I would love to see the iset.mm documentation explain more about how to "intuitionize", including citations pointing to especially good books/papers and specific explanations of how to do it in metamath ("when you see X, you often need to convert to Y by following steps Z"). Pointing to a few examples of theorems that are especially good at explaining the changes (and how to do something similar) would be great.

This is probably especially a request to @jkingdon ... but anyone else's input would be welcome.

I am intrigued by intuitionistic logic, but I am hopelessly steeped in classical logic :-). A little more explanation of what you have to change would be helpful for me, and probably for others.

Rewrite "no ph is ps" in Aristotelian section

Currently "no ps is ps" is written as -. E. ( ph /\ ps ) in the Aristotelian section. I suggest rewriting as A. ( ph -> -. ps ) ; it would make the proofs shorter, and that suggests that this would be the more natural representation in metamath anyway.

problem with commit 641e2b5

Something went wrong with some scripts I wrote to assist the df-sbc conversion. Please don't use this commit or merge with it until I fix it in a day or so.

Norm