Many thanks, Gino, for your efforts. I think we have a good intermediate result now, which, however, can still be improved (manually). I will try to eliminate the usage of ax-13 in my Mathbox and the following theorems of main:
- REAL AND COMPLEX NUMBERS: 2 theorems (~brfi1indALT and ~nfsum) - GRAPH THEORY: 1 theorem (~frgrwopreglem5ALT) Alexander [email protected] schrieb am Samstag, 20. April 2024 um 21:57:57 UTC+2: > I announce the successful completion of the project. As of April 20, 2024, > there are a total of 589 theorems that depend on ax-13, which is better > than forecasted in this mailing list (back in January I anticipated 819 > theorems left). > > Among these 589 theorems, there are 50 "OLD" proofs in main, which will be > deleted during the year. Additionally, there are 59 "ALT" theorems which > may contain candidates for ax-13 removal (I generally skipped theorems with > a "proof modification is discouraged" tag except for a few occurrences). > > > --------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------- > > Below I show a summary of the locations of those 589 theorems. 400 of them > are in main, and 189 in mathboxes: > > * Axiom scheme ax-13 (Quantified Equality): 186 theorems > > * Alternate definition of substitution: 30 theorems (it has recently been > proposed to delete this section > https://github.com/metamath/set.mm/pull/3924#pullrequestreview-2007403060) > > * Uniqueness and unique existence: 27 theorems > > * Intuitionistic logic: 6 theorems > > * ZF Set Theory - start with the Axiom of Extensionality: 90 theorems > > * ZF Set Theory - add the Axiom of Power Sets: 24 theorems > > * ZF Set Theory - add the Axiom of Union: 2 theorems (~fsplitOLD and > ~nfixp) > > * ZFC Axioms with no distinct variable requirements: 31 theorems > > * REAL AND COMPLEX NUMBERS: 2 theorems (~brfi1indALT and ~nfsum) > > * BASIC ALGEBRAIC STRUCTURES: 1 theorem (~cygablOLD) > > * GRAPH THEORY: 1 theorem (~frgrwopreglem5ALT) > > -----------------END OF MAIN------------------- > > * Mathbox for Thierry Arnoux: 1 theorem (~opreu2reuALT) > > * Mathbox for Jonathan Ben-Naim: 3 theorems > > * Mathbox for Scott Fenton: 14 theorems > > * Mathbox for Anthony Hart: 1 theorem (~subsym1) > > * Mathbox for BJ: 39 theorems > > * Mathbox for Wolf Lammen: 53 theorems > > * Mathbox for Giovanni Mascellani: 8 theorems > > * Mathbox for Peter Mazsa: 1 theorem (~brabidga) > > * Mathbox for Norm Megill: 15 theorems > > * Mathbox for Stefan O'Rear: 4 theorems (all *OLD) > > * Mathbox for Richard Penner: 5 theorems > > * Mathbox for Rohan Ridenour: 3 theorems > > * Mathbox for Andrew Salmon: 6 theorems > > * Mathbox for Alan Sare: 24 theorems (many of these have a "proof > modification" discouragement tag) > > * Mathbox for Glauco Siliprandi: 2 theorems > > * Mathbox for Alexander van der Vekens: 8 theorems > > * Mathbox for Emmett Weisz: 2 theorems > > > -------------------------------------------------------------------------------------------------------------------------------------------------------------------------- > > All theorems in main depending on ax-13 are discouraged, which provides > decent confidence that use of this axiom won't rise inadvertently. However > this mechanism is not perfect, it can be circumvented by moving a theorem > using ax-13 from a mathbox to main (not all theorems in mathboxes have a > discouragement tag). Therefore I reccommend to manually check ax-13 usage, > say, once a year. > > I attached a file containing the full list of theorems utilizing ax-13, > categorized by the respective chapters. You can use it to check out whether > you can find further improvements in your own mathbox or in main. > > Il giorno martedì 12 marzo 2024 alle 16:05:59 UTC+1 [email protected] ha > scritto: > >> On Mon, Mar 11, 2024 at 11:36 AM Jim Kingdon <[email protected]> wrote: >> >>> If this is just a hypothetical question I guess we don't really need to >>> come up with a definitive answer, but I will say that if we want to keep >>> some of our other values (like preferring short proofs), we'd end up >>> with a lot of ALT theorems or other ways in which there is a classical >>> proof, there is an intuitionistic proof, and the intuitionistic proof is >>> much longer. >> >> >> We already have a caveat in the proof shortening rules for this. We want >> shorter proofs but *only* assuming it doesn't take the theorem out of a >> "subsystem of interest". For the most part that means that proof searches >> using MINIMIZE will add /NO_NEW_AXIOMS to ensure that intuitionistic proofs >> stay intuitionistic. So in the variation you are talking about I would >> expect there to only be an intuitionistic proof, and the classical proof >> (if the statement is different) would be the shorter of "do the proof >> directly" and "apply the intuitionistic version and remove the unnecessary >> assumptions", which probably would end up with the latter most of the time. >> >> >>> Proof length aside, I guess I'm just not sure that set.mm would read >>> very nicely if it needed to concern itself with decidability, apartness, >>> additional conditions on things like supremums and convergence, etc. Not >>> to mention topology which beyond a certain point falls apart unless you >>> switch from point-set topology to locales (or so I read, iset.mm hasn't >>> really gotten that far yet). >>> >> >> This is a fair criticism. For those areas like topology where it's still >> unclear how to intuitionize it, the whole thing would simply be classical. >> But I would expect a cover-to-cover reader of set.mm to already know >> that it is trying to simultaneously cover intuitionistic and classical >> logic, and the abstractions that work in intuitionistic logic are also >> interesting in their own way. I know I had to search far and wide for >> proofs about measure theory in the absence of the axiom of choice (thanks >> Fremlin!) so it wouldn't be the first time for proofs that go out of their >> way to avoid some axiom. >> >> >>> I'll also say that I do agree about the observations about how iset.mm >>> and set.mm are similar enough that it is also awkward, in different >>> ways, to keep them separate. There are a lot of theorems which can >>> simply be copy-pasted in one direction or the other. >>> >> >> And of course these copy-pasted theorems are a future maintenance issue, >> since people will have to remember to change them in tandem (or not! if the >> change needs classical logic) and this is hard to deal with without a >> global view of all the databases. >> >> -- 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 [email protected]. To view this discussion on the web visit https://groups.google.com/d/msgid/metamath/be0570db-f1e7-4fc4-835a-2a202afd2e8an%40googlegroups.com.
