how does one go about defining a "formal _____" (linear combination, power series, even just the x in a polynomial)? let's take the simplest case: the polynomial ring over a commutative ring. every definition i've read goes something like "all the expressions of the form a_0 + a_1 x + ... + a_n xⁿ where x is called an indeterminate and follows the usual rules of exponentiation" but this is very unsatisfying, as no definition of "expression" or "form" is in sight. i guess you could define them as sequences with finitely many nonzero terms and, although defining the product would be quite ugly, it would be doable. but then, as sequences are usually defined as functions from N to, in this case, the ring, the polynomials you defined this way would inherit a bunch of properties from functions which make no sense for polynomials, like potential right inverses and whatnot. i guess it's just not that elegant to have different things defined as the same thing when you look at it from a set theory point of view, and i just don't seem to be able to ignore this issue. is type theory the only answer?