> > 0. Thanks to Benoit Jubin for applying the rubric at the top of > CONTRIBUTING.md which enhances the instructions in > https://github.com/metamath/set.mm/wiki/Getting-started-with-contributing > <https://www.google.com/url?q=https%3A%2F%2Fgithub.com%2Fmetamath%2Fset.mm%2Fwiki%2FGetting-started-with-contributing&sa=D&sntz=1&usg=AFQjCNEgX45g0dunS3KBmzkk-sh_-oElqQ> > . >
You're welcome! There is indeed a hyperlink from the former to the latter, but I'll have to add a link in the other direction. Benoit Jubin also wielded Solomon's knife and cut the long line of math > notation in two! Hmm, this list is off to a poor start as a list of > controversial topics. Best to start the count over from 1. > I saw that it generated a warning for being too long (and I thought warnings prevented Travis from passing, but apparently, this is the case for only some warnings). I replaced ´ long expression ´ with ´ long ´ ´ expression ´ which is not ideal semantically, but I think this is not a big deal. You may break the line at another place. 1. ~ coemptyd , ~ conrel1d , ~ conrel2d , and ~ xptrrel ( and therefore ~ > xpintrreld and ~ restrreld ) depend on ~ coeq0 in Stefan O'Rear's mathbox . > Could we move ~ coeq0 somewhere after ~ rnco ? I think it makes pedagogical > and narrative sense immediately after ~ dmco . > I think coeq0 is indeed important and I agree to move it to the main part. Maybe after ~ dmco ? > 2. There isn't yet an application for ~ cotrgen other than to make ~ > rp-cotr trivial. Will anyone ever need to talk about ` ( A o. B ) C_ C ` in > other than the ` ( R o. R ) C_ R ` case covered by ~ cotr ? If S is the > transitive closure of R, then ` ( R o. R ) C_ S ` holds (as does ` ( R ^r N > ) C_ S ` but see #10 below). > I would move both to the main part. I would say: if a theorem in the main part is a special instance of another theorem, then put that theorem too in the main part. I would also add to the comment of ~ rp-cotr "Special instance of ~ cotrgen" even if this is clear from the proof. I would also replace "Generalized by..." in the comment of ~ cotrgen to something like: "Generalized from the former proof of ~ cotr . (Revised by..." In order to keep the number of keyword to a low count (for the moment, it is "Contributed by", "Proof shortened by", and "Revised by"). Maybe also label it cotrg ? 6. Since ~ ax-3 implies ~ axfrege28 , ~ axfrege31 and ~ axfrege41 , it > seems to me that an effort to study (or document) the various ways that > these statements imply each other might be useful. Is it known that ~ ax-3 > is the strongest starting point? > Yes, basically everything is known in this domain! As for the documentation, if you mean "within Metamath", see the attachment to my post on this group https://groups.google.com/d/msg/metamath/mYchAks747s/TDntf_0CAAAJ . Indeed, ax-3 implies the other statements, but not conversely: * axfrege28 is a minimalistic form of contraposition; * axfrege31 (double negation elimination) is neither intuitionistic nor in "classical-refutability", but I do not think that it suffices together with ax-1 and ax-2: you may also need the minimalistic contraposition (on the other hand, minimal calculus together with double negation elimination gives you classical calculus); * axfrege41 (double negation introduction) is minimalistic. > 8. ~ bj-frege52a and ~ bj-frege54cor0a ( et. seq. ) leverage ~ df-bj-if > in Benoit Jubin's Mathbox. I could engineer around this dependence, but it > makes more sense to the spirit of Frege's overloaded equivalence connective > if I explore "logical functions of logical variables" and "universal > quantification over a logical variable" which I think can be done with the > least damage by depending on ~ df-bj-if . > This is great news! ~ df-bj-if is indeed a very natural operator, which has other advantages: it eases understanding of several sections of the main part. As such, it was bound to have applications; thanks for giving some! See https://groups.google.com/d/topic/metamath/zq_oZ15SFc8/discussion After this, I think the last resistance to keep it off the main part will vanish. In particular, in bj-frge52a, I would replace the consequent from an implication to a biconditional, label it "ifcbi" and comment it as "Equivalence theorem for the conditional operator on propositions." This is a common pattern in set.mm, see for instance ~ ifbi . Note that I label most theorems in my mathbox as bj-xxx in order to be able to do things like MM> verify proof bj-* or some other batch manipulations, like minimizations, so I would recommend you label yours rp-xxx. 10. Frege then introduces the concept of the transitive closure of a > relation, which is why I want to build up the tools we have to work. Do we > need this concept before the introduction of the real numbers? I think I > need something like relational exponentiation indexed on finite ordinals or > finite sets so that such work can be moved earlier. ( Right now ^r is > defined in terms of NN0 ). Current work on transitive closure of relations > seems to be in multiple places. My guide to this field is > https://proofwiki.org/wiki/Equivalence_of_Definitions_of_Transitive_Closure_(Relation_Theory) > I would simply prove that transitivity is a property stable under intersection, and define the transitive closure as the intersection of all transitive relations containing the given one, hence the smallest one. David A. Wheeler recently introduced reflexive relations and there was an ensuing discussion at https://github.com/metamath/set.mm/pull/1286 Merry Christmas! Benoît -- 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/21d55577-15eb-4634-8491-9acc7b31127d%40googlegroups.com.
