Definition talk:Summation

From ProofWiki
Jump to navigation Jump to search

I sense some trouble here. I have added a handwavery template on a proof yesterday because it used ellipsis for summation. Now, I find that our very definition of summation has the same problem. We really ought to give an inductive definition (perhaps by well-founded recursion on the finite subsets of $\N$) as a precise definition to fall back on.

There are some nasty theorems waiting out there once we're done defining (for example that the sum over a finite set $I$ is well-defined, as in independent of the bijection $I \to n$ chosen). I'll put it on my to-do list for when I get back from my vacation (which should be around July 22). — Lord_Farin (talk) 13:57, 3 July 2013 (UTC)

I have started the nasty work. I'm currently using elements of an abelian group as values, but this can easily be replaced by a more general thing, if needed. That's not my main concern at this point. --barto (talk) 05:49, 19 October 2017 (EDT)
Can we keep the specific-to-numbers stuff? --prime mover (talk) 06:54, 19 October 2017 (EDT)
Seconded. Tasty genericity should not alienate the high school student looking a bit beyond their textbook. — Lord_Farin (talk) 12:27, 19 October 2017 (EDT)
You mean for example using $\R$ instead of any abelian group? Fine for me, but it will imply that we will have to duplicate all those proofs for abelian groups. But okay, it is probably worth the effort making a distinction. --barto (talk) 12:57, 19 October 2017 (EDT)
Though I have mixed feelings about duplicating this proof and requiring any edits to be applied to both copies. --barto (talk) 15:48, 19 October 2017 (EDT)
We aim to be accessible to people who may not have studied abstract algebra, and are familiar only with the standard arithmetic structures $\N$, $\Z$, $\Q$, $\R$ and possibly $\C$. Same as with polynomials, which evolved suddenly from a simple definition of $a_n x^n + a_{n - 1} x^{n - 1} + \cdots + + a_1 x + a_0$ to something so abstract that it was incomprehensible to anyone not studying abstract algebra at masters level. While it may be the opinion of some that somebody so stupid as not to be completely familiar with the more abstract concepts does not deserve to be allowed to benefit from $\mathsf{Pr} \infty \mathsf{fWiki}$ (such sentiments have in the past been expressed), it has been suggested by others that it would be a good idea to allow for basic concepts to be couched in the language of the more familiar and everyday structures, as well as the deeper and more abstract frameworks. --prime mover (talk) 16:52, 19 October 2017 (EDT)

It is to some extent acceptable to refer to the generic proof from the specific theorem. But it's also worthwhile to keep the distinction because often a structure with more properties facilitates more, easier proofs than the most abstract one. Please be pragmatic. — Lord_Farin (talk) 16:33, 19 October 2017 (EDT)


This interesting discussion has to be merged with recent summation definition, please do not remove this logs since it is really informative!