On Wednesday, December 25, 2019 at 11:37:24 AM UTC-5, Benoit wrote: > > 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. >
If you need to display a formatted equation, you can use HTML tags. Currently, the presence of the tag "<HTML>" anywhere in the comment will prevent converting "<" to "<" for the whole comment. (Comments cannot be partially HTML.) The tags "<HTML>" and "</HTML>" (which is optional and has no effect) are discarded. "<HTML>" also prevents wrapping the comment with "write source.../rewrap", so any ASCII text formatting is also preserved in set.mm. (The handling of HTML will be changed at some point, per another discussion somewhere on this group, but it is nothing to be concerned with now.) > > 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 ? > I agree. Benoit, could you do this? > >> 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. > Moving ~cotrgen is OK. ~ rp-cotr is already there in the form of ~ cotr, it's just a matter of using ~ cotrgen to reprove ~ cotr in one step, and then ~rp-cotr can be deleted. > 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 don't know if this should be a hard and fast rule. ~ cotr is specifically intended to demonstrate the idiom ( R o. R ) C_ R as a way of saying "R is transitive", but generally situations where we would want to show a special case with a 1-step proof are pretty rare. > 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 ? > I think I would favor ~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 > Well, my opinion expressed there still holds.:) I have never seen it defined in any set theory book or even a book on mathematical logic. I think there are very few theorems in the main set.mm prop calc that would benefit. ~cases and ~cases2 would be direct applications, but they are used only 4 times total, 2 of which are by BJ's mathbox. Since 2 people want to use it, and our informal guideline has been to move up shared mathbox theorems, I suggest the following. Create a new section for it just above ~df-tru and move the shared theorems, their dependencies, and maybe a few more that might be useful in the future. Benoit can do that. If any standard prop calc theorems would benefit, such as ~cases2, reprove the if- versions in that section. I would be interested to see ~elimh, ~dedt, and ~con3th reproved in that section using the if- notation. I might replace these with the if- versions on the "Weak Deduction Theorem" (mpeuni/mmdeduction.html) page. I would not like to see the definition ~df-if restated with if-, because I think if- will hardly ever be used, and it would require the reader interested only in df-if to learn two definitions instead of one. The definition of df-if in terms of if- could be proved as a theorem though, say ~dfif7. Norm > 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/2ffc196c-c21b-44ca-9662-6e807809c221%40googlegroups.com.
