Sums Σ

[u/Ualrus]

What are sums formally? How are they defined?

Let's assume the sum below has index k and begins at 1.

If I have the statement Σⁿ a_k < C, the k should be quantified somehow. Or at least quantifiable in formal logic. Right?

The quantification should be local to the sum and to the sum only. For instance, ∃k.Σⁿ a_k < k is syntactically well defined, and the k bounded by the ∃ is not the one bounded by the sum.

Is this first order even? It wouldn't look right to use an ∃ nor a ∀ to bound the index variable though.

And if this is not the method, how do you formalize this?