Merry Christmas from Richard Penner

[Richard Penner]

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)

[Benoit]

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.

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

[Norman Megill]

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.

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 "&lt;" 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