What is the formal definition of polynomial ring of several variables?
Let's consider a polynomial ring of single variable.
One can define them informally by saying $P(X)=\sum_{i=1}^n a_n X^n$ while $X$ is an indeterminate variable.
However, since mathematics is based on first-order logic, one can only talk about something that actually exists (as a set). So as its name says, indeterminate variable is not a sentence in $ZFC$.
Nevertheless, we can formally define a polynomial ring $R[X]$ as a subset of $R^\omega$ whose support is finite. ($R$ is a commutative ring with unity)
Just like a single variable, I want to know what would be the formal definition of a polynomial ring of several variables. What would be a formal definition?
===
I have figured out a candidate. That is,
Candidate for a "Definition of a polynomial ring $R[X_1,...,X_n]$". ($R$ is a commutative ring with unity)
Let $R[X_1,...,X_n]$ be the set of all functions $f:\omega^n \rightarrow R$ whose support is finite.
Define $(f+g)(a,b,c)=f(a,b,c)+g(a,b,c)$ and $(f•g)(a'',b'',c'')=\sum_{a+a'=a''} f(a,b,c)•g(a',b',c')$ (Note that in this way, $+,•$ are well defined.)
Then, it can be checked that $(R[X_1,...,X_n],+,•)$ is a ring.
Is this a formal definition of a polynomial ring?
Your attempt is in the right direction, but it's unclear what you mean by $f(a,b,c)$.
Define an operation $+$ on $\omega^n$ in the obvious way, that is, componentwise. A function $f\colon \omega^n\to R$ is a polynomial in $n$ indeterminates if (and only if) $f(t)=0$ for all but a finite number of elements $t\in\omega^n$ (has finite support, in other words). For two polynomials $f$ and $g$ define $$ f+g\colon t\mapsto f(t)+g(t) $$ and $$ fg\colon t\mapsto \sum_{u+v=t}f(u)g(v) $$ After verifying that these operations are well defined in the set of polynomials, it's just a tedious verification showing that this set is a ring. The embedding of $R$ in this ring is the map sending $r$ into the function $\bar{r}$ that is $r$ on $(0,0,\dots,0)\in\omega^n$ and zero elsewhere: $$ \bar{r}(t)=\begin{cases} r&\text{if $t=(0,\dots,0)$}\\ 0&\text{otherwise} \end{cases} $$ Note that the set of polynomials is, under addition, the free $R$-module on $\omega^n$.
In any case, thinking to polynomials from a higher point of view (that is, free objects in a suitable category) is more rewarding.