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/c8452908-94fe-4b96-8d9d-4501332b511an%40googlegroups.com.
---- Axiom scheme ax-13 (Quantified Equality)---- ax13v: ax-13 ax13lem1: ax-13 ax13: ax-13 ax13lem2: ax-13 nfeqf2: ax-13 dveeq2: ax-13 nfeqf1: ax-13 dveeq1: ax-13 nfeqf: ax-13 axc9: ax-13 ax6e: ax-13 ax6: ax-13 axc10: ax-13 spimt: ax-13 spim: ax-13 spimed: ax-13 spime: ax-13 spimv: ax-13 spimvALT: ax-13 spimev: ax-13 spv: ax-13 spei: ax-13 chvar: ax-13 chvarv: ax-13 cbv3: ax-13 cbval: ax-13 cbvex: ax-13 cbvalv: ax-13 cbvexv: ax-13 cbvalvOLD: ax-13 cbvexvOLD: ax-13 cbv1: ax-13 cbv2: ax-13 cbv3h: ax-13 cbv1h: ax-13 cbv2h: ax-13 cbv2OLD: ax-13 cbvald: ax-13 cbvexd: ax-13 cbvaldva: ax-13 cbvexdva: ax-13 cbval2: ax-13 cbval2OLD: ax-13 cbvex2: ax-13 cbval2vv: ax-13 cbvex2vv: ax-13 cbvex4v: ax-13 equs4: ax-13 equsal: ax-13 equsex: ax-13 equsexALT: ax-13 equsalh: ax-13 equsexh: ax-13 axc15: ax-13 ax12: ax-13 ax12b: ax-13 ax13ALT: ax-13 axc11n: ax-13 aecom: ax-13 aecoms: ax-13 naecoms: ax-13 axc11: ax-13 hbae: ax-13 hbnae: ax-13 nfae: ax-13 nfnae: ax-13 hbnaes: ax-13 axc16i: ax-13 axc16nfALT: ax-13 dral2: ax-13 dral1: ax-13 dral1ALT: ax-13 drex1: ax-13 drex2: ax-13 drnf1: ax-13 drnf2: ax-13 nfald2: ax-13 nfexd2: ax-13 exdistrf: ax-13 dvelimf: ax-13 dvelimdf: ax-13 dvelimh: ax-13 dvelim: ax-13 dvelimv: ax-13 dvelimnf: ax-13 dveeq2ALT: ax-13 equvini: ax-13 equviniOLD: ax-13 equvel: ax-13 equs5a: ax-13 equs5e: ax-13 equs45f: ax-13 equs5: ax-13 dveel1: ax-13 dveel2: ax-13 axc14: ax-13 sb6x: ax-13 sbequ5: ax-13 sbequ6: ax-13 sb5rf: ax-13 sb6rf: ax-13 ax12vALT: ax-13 2ax6elem: ax-13 2ax6e: ax-13 2ax6eOLD: ax-13 2sb5rf: ax-13 2sb6rf: ax-13 sbel2x: ax-13 sb4b: ax-13 sb4bOLD: ax-13 sb3b: ax-13 sb3: ax-13 sb1: ax-13 sb2: ax-13 sb3OLD: ax-13 sb4OLD: ax-13 sb1OLD: ax-13 sb3bOLD: ax-13 sb4a: ax-13 dfsb1: ax-13 spsbeOLDOLD: ax-13 sb2vOLDOLD: ax-13 sb4vOLDOLD: ax-13 sbequ2OLDOLD: ax-13 sbimiOLD: ax-13 sbimdvOLD: ax-13 equsb1vOLDOLD: ax-13 sbimdOLD: ax-13 sbtvOLD: ax-13 sbequ1OLD: ax-13 hbsb2: ax-13 nfsb2: ax-13 hbsb2a: ax-13 sb4e: ax-13 hbsb2e: ax-13 hbsb3: ax-13 nfs1: ax-13 axc16ALT: ax-13 axc16gALT: ax-13 equsb1: ax-13 equsb2: ax-13 dfsb2: ax-13 dfsb3: ax-13 sbequiOLD: ax-13 drsb1: ax-13 sb2ae: ax-13 sb6f: ax-13 sb5f: ax-13 nfsb4t: ax-13 nfsb4: ax-13 sbnOLD: ax-13 sbi1OLD: ax-13 sbequ8: ax-13 sbie: ax-13 sbied: ax-13 sbiedv: ax-13 2sbiev: ax-13 sbcom3: ax-13 sbco: ax-13 sbid2: ax-13 sbid2v: ax-13 sbidm: ax-13 sbco2: ax-13 sbco2d: ax-13 sbco3: ax-13 sbcom: ax-13 sbtrt: ax-13 sbtr: ax-13 sb8: ax-13 sb8e: ax-13 sb9: ax-13 sb9i: ax-13 sbhb: ax-13 nfsbd: ax-13 nfsb: ax-13 nfsbOLD: ax-13 hbsb: ax-13 sb7f: ax-13 sb7h: ax-13 dfsb7OLDOLD: ax-13 sb10f: ax-13 sbal1: ax-13 sbal2: ax-13 sbal2OLD: ax-13 sbalOLD: ax-13 2sb8e: ax-13 ----Alternate definition of substitution---- sb2ALT: ax-13 sb4ALT: ax-13 stdpc4ALT: ax-13 dfsb2ALT: ax-13 dfsb3ALT: ax-13 sbftALT: ax-13 sbfALT: ax-13 sbnALT: ax-13 sbequiALT: ax-13 sbequALT: ax-13 sb4aALT: ax-13 hbsb2ALT: ax-13 nfsb2ALT: ax-13 equsb1ALT: ax-13 sb6fALT: ax-13 sb5fALT: ax-13 nfsb4tALT: ax-13 nfsb4ALT: ax-13 sbi1ALT: ax-13 sbi2ALT: ax-13 sbimALT: ax-13 sbrimALT: ax-13 sbanALT: ax-13 sbbiALT: ax-13 sblbisALT: ax-13 sbieALT: ax-13 sbiedALT: ax-13 sbco2ALT: ax-13 sb7fALT: ax-13 dfsb7ALT: ax-13 ----Uniqueness and unique existence---- nfmod2: ax-13 nfmod: ax-13 nfmo: ax-13 eujustALT: ax-13 nfeud2: ax-13 nfeud: ax-13 nfeu: ax-13 sb8eu: ax-13 sb8mo: ax-13 cbvmo: ax-13 cbveu: ax-13 cbveuALT: ax-13 moexex: ax-13 moexexv: ax-13 2moex: ax-13 2euex: ax-13 2moswap: ax-13 2euswap: ax-13 2exeu: ax-13 2eu1: ax-13 2eu1OLD: ax-13 2eu2: ax-13 2eu3: ax-13 2eu3OLD: ax-13 2eu5OLD: ax-13 2eu7: ax-13 2eu8: ax-13 ----Intuitionistic logic---- axi9: ax-13 axi10: ax-13 axi12: ax-13 axi12OLD: ax-13 axbnd: ax-13 axbndOLD: ax-13 ----ZF Set Theory - start with the Axiom of Extensionality---- hbabg: ax-13 nfsabg: ax-13 cbvab: ax-13 cbvabvOLD: ax-13 hblemg: ax-13 clelsb3f: ax-13 clelsb3fOLD: ax-13 nfabg: ax-13 nfaba1g: ax-13 drnfc1: ax-13 drnfc1OLD: ax-13 drnfc2: ax-13 nfabd: ax-13 nfabd2: ax-13 nfabd2OLD: ax-13 nfabdOLD: ax-13 dvelimdc: ax-13 dvelimc: ax-13 nfcvf: ax-13 nfcvf2: ax-13 nfcvfOLD: ax-13 nfrald: ax-13 nfral: ax-13 nfra2: ax-13 rgen2a: ax-13 nfrexdg: ax-13 nfrexg: ax-13 ralcom2: ax-13 nfreud: ax-13 nfrmod: ax-13 nfreu: ax-13 nfrmo: ax-13 nfrab: ax-13 cbvralf: ax-13 cbvrexf: ax-13 cbvral: ax-13 cbvrex: ax-13 cbvreu: ax-13 cbvrmo: ax-13 cbvralv: ax-13 cbvrexv: ax-13 cbvreuv: ax-13 cbvrmov: ax-13 cbvral2v: ax-13 cbvrex2v: ax-13 cbvral3v: ax-13 cbvralsv: ax-13 cbvrexsv: ax-13 cbvrab: ax-13 cbvrabvOLD: ax-13 vtoclgftOLD: ax-13 pm13.183OLD: ax-13 euxfr2: ax-13 euxfr: ax-13 cdeqal1: ax-13 cdeqab1: ax-13 nfcdeq: ax-13 nfccdeq: ax-13 nfsbcd: ax-13 nfsbc: ax-13 sbcco: ax-13 cbvsbc: ax-13 cbvsbcv: ax-13 cbvcsb: ax-13 csbco: ax-13 nfcsbd: ax-13 nfcsb: ax-13 cbvralcsf: ax-13 cbvrexcsf: ax-13 cbvreucsf: ax-13 cbvrabcsf: ax-13 cbvralv2: ax-13 cbvrexv2: ax-13 sbcnestgf: ax-13 csbnestgf: ax-13 sbcnestg: ax-13 csbnestg: ax-13 sbcco3g: ax-13 csbco3g: ax-13 nfiung: ax-13 nfiing: ax-13 cbviung: ax-13 cbviing: ax-13 cbviunvg: ax-13 cbviinvg: ax-13 nfdisj: ax-13 cbvopab1g: ax-13 cbvmptfg: ax-13 cbvmptg: ax-13 cbvmptvg: ax-13 ----ZF Set Theory - add the Axiom of Power Sets---- dtrucor2: ax-13 nfcvb: ax-13 copsexg: ax-13 opabid: ax-13 ssopab2b: ax-13 eqopab2b: ax-13 dfid3: ax-13 dfid2: ax-13 nfiotad: ax-13 nfiota: ax-13 cbviota: ax-13 cbviotav: ax-13 sb8iota: ax-13 iotaeq: ax-13 elfvmptrab1: ax-13 ralrnmpt: ax-13 rexrnmpt: ax-13 nfriotad: ax-13 cbvriota: ax-13 cbvriotav: ax-13 oprabid: ax-13 ssoprab2b: ax-13 eqoprab2b: ax-13 elovmporab1: ax-13 ---ZF Set Theory - add the Axiom of Union---- fsplitOLD: ax-13 nfixp: ax-13 ----ZFC Axioms with no distinct variable requirements---- nd1: ax-13 nd2: ax-13 nd4: ax-13 axextnd: ax-13 axrepndlem1: ax-13 axrepndlem2: ax-13 axrepnd: ax-13 axunndlem1: ax-13 axunnd: ax-13 axpowndlem2: ax-13 axpowndlem3: ax-13 axpowndlem4: ax-13 axpownd: ax-13 axregndlem1: ax-13 axregndlem2: ax-13 axregnd: ax-13 axinfndlem1: ax-13 axinfnd: ax-13 axacndlem1: ax-13 axacndlem2: ax-13 axacndlem3: ax-13 axacndlem4: ax-13 axacndlem5: ax-13 axacnd: ax-13 zfcndext: ax-13 zfcndrep: ax-13 zfcndun: ax-13 zfcndpow: ax-13 zfcndreg: ax-13 zfcndinf: ax-13 zfcndac: ax-13 ----REAL AND COMPLEX NUMBERS---- brfi1indALT: ax-13 nfsum: ax-13 ----BASIC ALGEBRAIC STRUCTURES---- cygablOLD: ax-13 ----GRAPH THEORY---- frgrwopreglem5ALT: ax-13 -------------------END OF MAIN--------------------- ----Mathbox for Thierry Arnoux---- opreu2reuALT: ax-13 ----Mathbox for Jonathan Ben-Naim---- bnj1441g: ax-13 bnj985: ax-13 bnj1018g: ax-13 ----Mathbox for Scott Fenton---- axextprim: ax-13 axrepprim: ax-13 axunprim: ax-13 axpowprim: ax-13 axregprim: ax-13 axinfprim: ax-13 axacprim: ax-13 axextdfeq: ax-13 ax8dfeq: ax-13 axextdist: ax-13 axextbdist: ax-13 exnel: ax-13 distel: ax-13 axextndbi: ax-13 ----Mathbox for Anthony Hart---- subsym1: ax-13 ----Mathbox for BJ---- bj-ax6elem1: ax-13 bj-ax6e: ax-13 axc11n11: ax-13 axc11n11r: ax-13 bj-ax12v3: ax-13 bj-ax12v3ALT: ax-13 bj-axc10: ax-13 bj-alequex: ax-13 bj-spimt2: ax-13 bj-cbv3ta: ax-13 bj-cbv3tb: ax-13 bj-hbsb3t: ax-13 bj-hbsb3: ax-13 bj-nfs1t: ax-13 bj-nfs1t2: ax-13 bj-nfs1: ax-13 bj-hbaeb2: ax-13 bj-hbaeb: ax-13 bj-hbnaeb: ax-13 bj-dvv: ax-13 bj-equsal1t: ax-13 bj-equsal1ti: ax-13 bj-equsal1: ax-13 bj-equsal2: ax-13 bj-equsal: ax-13 ax6er: ax-13 exlimiieq1: ax-13 exlimiieq2: ax-13 bj-sbsb: ax-13 bj-dfsb2: ax-13 bj-sbievv: ax-13 bj-sbidmOLD: ax-13 bj-dvelimdv: ax-13 bj-dvelimdv1: ax-13 bj-dvelimv: ax-13 bj-nfeel2: ax-13 bj-axc14nf: ax-13 bj-axc14: ax-13 bj-nfcsym: ax-13 ----Mathbox for Wolf Lammen---- wl-hbae1: ax-13 wl-spae: ax-13 wl-speqv: ax-13 wl-19.8eqv: ax-13 wl-19.2reqv: ax-13 wl-nfae1: ax-13 wl-nfnae1: ax-13 wl-aetr: ax-13 wl-axc11r: ax-13 wl-dral1d: ax-13 wl-cbvalnaed: ax-13 wl-cbvalnae: ax-13 wl-exeq: ax-13 wl-aleq: ax-13 wl-nfeqfb: ax-13 wl-nfs1t: ax-13 wl-equsald: ax-13 wl-equsal: ax-13 wl-equsal1t: ax-13 wl-equsal1i: ax-13 wl-sb6rft: ax-13 wl-sb8t: ax-13 wl-sb8et: ax-13 wl-sbhbt: ax-13 wl-sbnf1: ax-13 wl-equsb3: ax-13 wl-equsb4: ax-13 wl-2sb6d: ax-13 wl-sbcom2d-lem1: ax-13 wl-sbcom2d-lem2: ax-13 wl-sbcom2d: ax-13 wl-sbalnae: ax-13 wl-sbal1: ax-13 wl-sbal2: ax-13 wl-mo2df: ax-13 wl-mo2tf: ax-13 wl-eudf: ax-13 wl-eutf: ax-13 wl-euequf: ax-13 wl-mo3t: ax-13 wl-sb8eut: ax-13 wl-sb8mot: ax-13 wl-ax11-lem1: ax-13 wl-ax11-lem2: ax-13 wl-ax11-lem3: ax-13 wl-ax11-lem4: ax-13 wl-ax11-lem5: ax-13 wl-ax11-lem6: ax-13 wl-ax11-lem8: ax-13 wl-ax11-lem9: ax-13 wl-ax11-lem10: ax-13 wl-clelsb3df: ax-13 wl-dfrabf: ax-13 ----Mathbox for Giovanni Mascellani---- exlimddvfi: ax-13 sbccom2: ax-13 sbccom2f: ax-13 sbccom2fi: ax-13 csbcom2fi: ax-13 oprabbi: ax-13 mpobi123f: ax-13 opabbi: ax-13 ----Mathbox for Peter Mazsa---- brabidga: ax-13 ----Mathbox for Norm Megill---- dvelimf-o: ax-13 dveeq2-o: ax-13 dveeq1-o: ax-13 dveeq1-o16: ax-13 axc11n-16: ax-13 dveel2ALT: ax-13 ax12eq: ax-13 ax12el: ax-13 ax12indalem: ax-13 ax12inda2ALT: ax-13 ax12inda2: ax-13 ax12inda: ax-13 ax12v2-o: ax-13 ax12a2-o: ax-13 axc11-o: ax-13 ----Mathbox for Stefan O'Rear---- sbcrexgOLD: ax-13 2sbcrexOLD: ax-13 sbc2rexgOLD: ax-13 sbc4rexgOLD: ax-13 ----Mathbox for Richard Penner---- frege54cor1b: ax-13 frege55lem2b: ax-13 frege55b: ax-13 frege56b: ax-13 frege57b: ax-13 ----Mathbox for Rohan Ridenour---- spALT: ax-13 rexlimdvaacbv: ax-13 rexlimddvcbv: ax-13 ----Mathbox for Andrew Salmon---- pm11.58: ax-13 sbeqal1: ax-13 sbeqal1i: ax-13 sbeqal2i: ax-13 dropab1: ax-13 dropab2: ax-13 ----Mathbox for Alan Sare---- sb5ALT: ax-13 cbvexsv: ax-13 onfrALTlem1: ax-13 onfrALT: ax-13 ax6e2eq: ax-13 ax6e2nd: ax-13 ax6e2ndeq: ax-13 2sb5nd: ax-13 2uasbanh: ax-13 2uasban: ax-13 e2ebind: ax-13 onfrALTlem1VD: ax-13 onfrALTVD: ax-13 ax6e2eqVD: ax-13 ax6e2ndVD: ax-13 ax6e2ndeqVD: ax-13 2sb5ndVD: ax-13 2uasbanhVD: ax-13 e2ebindVD: ax-13 sb5ALTVD: ax-13 e2ebindALT: ax-13 ax6e2ndALT: ax-13 ax6e2ndeqALT: ax-13 2sb5ndALT: ax-13 ----Mathbox for Glauco Siliprandi---- eliuniincex: ax-13 cbvrabv2: ax-13 ----Mathbox for Alexander van der Vekens---- cbvral2: ax-13 cbvrex2: ax-13 dfich2OLD: ax-13 ichnfimlem1: ax-13 ichnfimlem2: ax-13 ichnfimlem3: ax-13 ichnfim: ax-13 ichnfb: ax-13 ----Mathbox for Emmett Weisz---- nfiundg: ax-13 spd: ax-13
