Reworking recursion

[Scott Fenton]

Hi all,

I'd like to move my theorem fsumkthpow (giving the value of the finite sum of powers) into the main body of Metamath, since it's a 100 theorem. However, that depends on the definition of Bernoulli polynomials, which I define using my well-founded recursion theorems. This is a fairly large body of theorems, so I'd like to get opinions before moving the three sections that this requires up.

If there's support for this, is there support for reworking transfinite recursion to be a special case of well-founded recursion? tfr1 through 3 can be easily expressed by setting recs ( F ) = wrecs ( _E , On , F ). I'd like to make this the official definition of recs, since it expresses that the important part of recursion is well-foundedness, not anything special about the ordinals themselves. Any thoughts?

-Scott

[Norman Megill]

On Wednesday, July 29, 2020 at 11:09:40 AM UTC-4, Scott Fenton wrote:

Hi all,

I'd like to move my theorem fsumkthpow (giving the value of the finite sum of powers) into the main body of Metamath, since it's a 100 theorem. However, that depends on the definition of Bernoulli polynomials, which I define using my well-founded recursion theorems. This is a fairly large body of theorems, so I'd like to get opinions before moving the three sections that this requires up.

This is nice work, and I am in favor of moving it into the main set.mm.
 

If there's support for this, is there support for reworking transfinite recursion to be a special case of well-founded recursion? tfr1 through 3 can be easily expressed by setting recs ( F ) = wrecs ( _E , On , F ). I'd like to make this the official definition of recs, since it expresses that the important part of recursion is well-foundedness, not anything special about the ordinals themselves. Any thoughts?

Certainly we can state "recs ( F ) = wrecs ( _E , On , F )" as a theorem (it looks like it is already there, ~tfrALTlem) that provides an alternate definition called ~dfrecs3. (There is already a ~dfrecs2.)

What concerns me is that the present ordinal-based development is very close to textbooks (most textbooks I think, although I'm not sure), with detailed references to Takeuti-Zaring in particular that match the textbook almost exactly. Transfinite recursion is already a somewhat difficult topic, in a way the first "deep" theorem about ordinals, and I'm wondering if it makes sense to discard that in favor of the more general well-founded recursion. In other words, would we be throwing away a useful didactic tool? I'm not sure how many people have used the present ordinal tfr to assist self-learning; one I know of was Alan Sare.

I'd like to see more discussion of this point.

Norm

[David A. Wheeler]

On Wednesday, July 29, 2020 at 11:09:40 AM UTC-4, Scott Fenton wrote:
> > I'd like to move my theorem fsumkthpow (giving the value of the finite sum
> > of powers) into the main body of Metamath, since it's a 100 theorem.
> > However, that depends on the definition of Bernoulli polynomials, which I
> > define using my well-founded recursion theorems. This is a fairly large
> > body of theorems, so I'd like to get opinions before moving the three
> > sections that this requires up.

On Thu, 30 Jul 2020 07:51:36 -0700 (PDT), Norman Megill <n...@alum.mit.edu> wrote:
> This is nice work, and I am in favor of moving it into the main set.mm.

Excellent, I agree. I think that all the Metamath 100 theorems (and their dependencies)
should be moved into the main body eventually, possibly after some reviews &
clean-ups where important.

> > If there's support for this, is there support for reworking transfinite
> > recursion to be a special case of well-founded recursion? tfr1 through 3
> > can be easily expressed by setting recs ( F ) = wrecs ( _E , On , F ). I'd
> > like to make this the official definition of recs, since it expresses that
> > the important part of recursion is well-foundedness, not anything special
> > about the ordinals themselves. Any thoughts?
> >
>
> Certainly we can state "recs ( F ) = wrecs ( _E , On , F )" as a theorem
> (it looks like it is already there, ~tfrALTlem) that provides an alternate
> definition called ~dfrecs3. (There is already a ~dfrecs2.)
>
> What concerns me is that the present ordinal-based development is very
> close to textbooks (most textbooks I think, although I'm not sure), with
> detailed references to Takeuti-Zaring in particular that match the textbook

> almost exactly. ...

> Transfinite recursion is already a somewhat difficult
> topic, in a way the first "deep" theorem about ordinals, and I'm wondering
> if it makes sense to discard that in favor of the more general well-founded
> recursion. In other words, would we be throwing away a useful didactic
> tool? I'm not sure how many people have used the present ordinal tfr to
> assist self-learning; one I know of was Alan Sare.

Both alternatives have really good arguments.

If we keep the definitions as they are, I think we need to add a
discussion about this in the comments (with cross-references to make the
discussion easier to find). And, of course, include the proof of the
relationship in the main body.

--- David A. Wheelr

[Scott Fenton]

I don't think much is lost by making well-founded recursion the basic system. The development of the well-founded theorems actually parallels the transfinite case quite closely. It merely emphasizes the difference between a set and it's predecessor set, which I think is a valuable distinction to make. I'm working on getting the Replacement-free versions of the theorems into my branch now, but I don't anticipate any large problems.

There's also the fact that this will more closely follow the NF version of recursion that I'm trying to get underway. In that version, we have to distinguish between a set and its predecessor set, since there are no von Neumann ordinals to fall back on.

--
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 metamath+u...@googlegroups.com.
To view this discussion on the web visit https://groups.google.com/d/msgid/metamath/3f017efb-c8d2-4888-a2de-229612d96392o%40googlegroups.com.

[Norman Megill]

On Thursday, July 30, 2020 at 12:53:08 PM UTC-4, Scott Fenton wrote:

I don't think much is lost by making well-founded recursion the basic system. The development of the well-founded theorems actually parallels the transfinite case quite closely. It merely emphasizes the difference between a set and it's predecessor set, which I think is a valuable distinction to make. I'm working on getting the Replacement-free versions of the theorems into my branch now, but I don't anticipate any large problems.

There's also the fact that this will more closely follow the NF version of recursion that I'm trying to get underway. In that version, we have to distinguish between a set and its predecessor set, since there are no von Neumann ordinals to fall back on.

I like your WFR work and would like to see it in the main set.mm. But I'm still concerned that some people may want to see the traditional textbook ordinal transfinite recursion.

While harmonizing it with the NF development is a nice goal in principle, we also need to look at what is best for set.mm/ZFC. For example, set.mm doesn't build on top of the intuitionistic set theory of iset.mm but has an independent classical development that more closely follows textbook ZFC and its axioms.

Can you give some more detail how you envision replacing the ordinal TFR? What parts of the current ordinal development would be discarded? Where do you propose placing the WFR development?

Is it possible to set up the two developments in a way that we can switch between them by doing something like swapping df-recs and tfrALTlem as the recs definition (maybe with some auxiliary lemmas to make this easier)? That could provide an alternative for the reader interested in the textbook ordinal development (after thus modifying set.mm and regenerating the web pages locally). As long as we have a way to go back without much difficulty if we change our minds later, I'll accept making tfrALTlem the official definition as you propose. That will let us postpone a decision to delete the ordinal TFR.

It would be interesting to hear how other people learned transfinite and/or well-founded recursion, and which is considered "harder" for the beginner.  Is there a reason ordinal TFR is the one that (I think) is mostly used?

Norm

[Jim Kingdon]

On 8/1/20 2:41 PM, Norman Megill wrote:

> It would be interesting to hear how other people learned transfinite
> and/or well-founded recursion, and which is considered "harder" for
> the beginner.  Is there a reason ordinal TFR is the one that (I think)
> is mostly used?

I guess the answer is that I got through a major in undergraduate
mathematics, and a certain amount of recreational mathematics, where
recursion was pretty much assumed and treated informally. This would
mostly be recursion on natural numbers. I had heard of transfinite
recursion, but not well-founded recursion (at least, not by that name, I
couldn't say for sure whether there was some kind of argument applied
informally which amounted to well-founded recursion). I'm not sure we
even got as far as handwaving at something vaguely called the "Recursion
Theorem". So in a way I'm not a good test case, because I didn't really
learn either kind of recursion, at least not with rigor.

Given this, having to formalize recursion for iset.mm was a bit of a
rude awakening. Having the set.mm treatment was helpful, but it breaks
down after tfrlem9 . And although I have found constructive set thoery
references (maybe not exactly textbooks, but close enough in the sense
that they can often be formalized without major changes) for things like
Dedekind cuts, complex division, and others, I found nothing of the sort
for recursion.

Sorry I'm not sure that saying "the number of people who really worry
about how recursion works is much smaller than the number of people who
use recursion without really thinking about it too hard" really answers
your question. But I do share a certain amount of what seems to be your
caution - in terms of whether building in too much generality would make
it even less clear how ordinal recursion is working.

[Benoit]

Not an answer, and not taking position, but this tension between a pedagogical goal and a "reference work" goal has already appeared (e.g. the binomial theorem is now proved in set.mm for general rings, and it is proved that complex numbers form a ring, but the binomial theorem for complex numbers is not proved as a direct corollary of these two facts), and this tension is bound to appear again: these goals are simply not compatible (after all, except for restricted fields, most textbooks are not reference works, and the brilliant reference work by Bourbaki would do a terrible textbook).

By the way: I see that there are things on well-founded recursion in JBN's mathbox (http://us2.metamath.org/mpeuni/mmtheorems.html). How do they compare ?

Benoit

[Scott Fenton]

So you're proposing leaving the tfr* development in place, just turning df-recs into a dfrecs3 or something? I can do that. In fact, I originally had that as a direct proof back before df-recs existed. I'll make the relevant mods and do a pull request.

I'm still interested in hearing about people's experiences with recursion theorems. I'd eventually like to develop a set of recursion theorems that use the transitive closure, so we can say "R Fr A" instead of "R We A". That requires Infinity, so it wouldn't replace any of the current developments. However, it plays well with my long-term goal of formalizing the surreal numbers in MM.

--

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 metamath+u...@googlegroups.com.

To view this discussion on the web visit https://groups.google.com/d/msgid/metamath/d061c9e3-58bc-41d1-a338-13f441fa1c60o%40googlegroups.com.

[fl]

What concerns me is that the present ordinal-based development is very close to textbooks (most textbooks I think, although I'm not sure), with detailed references to Takeuti-Zaring in particular that match the textbook almost exactly. 

This point must be emphasized. For instance by a detailed paragraph in the first theorem of the series and a note saying that a combined use of the formal proofs in set. mm and the explanations in Takeuti-Zaring would be very valuable pedagogical material. Proofs that are very close to a textbook are more  suitable for beginners than the others. But attention should be drawn to this pecularity. A  table of contents enumerating the proofs in the series and a short description of each one might help too.

This kind of material -- close to the book -- might easily be set up for Euclid's books, featuring Euclid's original text, Aitken's handouts and Byrne's intuitive edition with diagrams. It  would also constitute a very valuable material. We would have (in an international language) a full collection of texts connecting the original source, an intuitive presentation (Byrne), an accurate, modern and completely rigorous formulation (Aitken) and the final symbolic formalization. If we add a table with references to these texts put side by side, it would be the perfect tool for those who want to read Euclid and understand where the text is great and where it is inadequate. 

It would not be a repeat of Tarski's system. The treatise describing it is in German and thereby perfectly out of reach for the vast majority of inhabitants of this planet. And anyway Tarski's system is not the original system, it's a modern one. People are more comfortable with Euclid's system. It's the official definition of an euclidean plane, the definition of reference so to speak. And it might be used to show the equivalence of the reference definition with Tarski's system.  It would also be a pity not to use Aitken's very interesting work. 

-- 

FL

[fl]

Thank you guys for your help. It's very kind of you.  Especially since I'm certain that the project is interesting and that

it doesn't harm Thierry's project in any way.

--

FL