Merry Christmas from your October DNS detective and Math dilettante. I'm the one from *Mathematical Biosciences*, Vol 101, Issue 2, pp. 285-287 (October 1990) and (1/n) A189766(n) = A178790(n) = sum (2k_1) A005259(k) in OEIS, not one of the more famous researchers (or anyone with a University position) you might read about.
It wouldn't be a Christmas dinner without fighting over politics, so I have bestowed upon you a brand new Mathbox full of discussion items. Dinner Table Arguments with Mathbox for Richard Penner 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. 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. 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 . 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). 3. Should ~ ax-frege1 and ~ ax-frege2 exist or would it be better to use only ~ ax-1 and ~ ax-2 ? Should the goal be a Frege1879 fairyland with axfrege* statments proving from the bulk of set.mm that the ax-frege* axioms are valid or is total isolationism pointless once we have to accept set theory to work concretely with Frege's universal quantification? 4. Should every ax-frege* come with (New usage is discouraged.) and every frege* where the proof closely followed the 1879 proof be tagged with (Proof modification is discouraged.) ? 5. The first citation of [Frege1879] in ~ axfrege8 and ~ ax-frege8 should be changed to "Frege's 1879 work" to prevent very long entries in column one of the Bibliographic Cross-Reference table. (My fix got delayed by github's scorn of pushes from shallow clones and network instability while attempting to unshallow my clone. I just about have this fixed so I'll try to push tonight. ) 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? 7. In the main body of set.mm the Frege1879 statements are called Propositions while I describe them as Axioms and Propositions. Since our usage of these terms is philosophically different than in the Nineteenth century, is the labeling of these Frege statements (not a bibliographic keyword) as Axioms, Theorems, Lemmas and Definitions desirable? 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 . 9. Frege introduces the concept of heritable relation on a class (well actually on a logical predicate, but his notation becomes too ugly to live at that point). Should I introduce a binary primitive "R he A" or leave it in terms of image and subset even though that double-references one of the classes. 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) -- 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/eac3c8a5-df79-4f67-af7c-69cc1b860218%40googlegroups.com.
