I am seeking a comprehensible yet formal definition of a varaible.
I have already looked at the post What is the formal definition of a variable?, yet it is largely incomprehensible for someone who have never studied first-order logic.
My thoughts:
When writing proofs, we usally say
Let $x\in\mathbb{R}$ be given.
What exactly are we saying here? We are saying let an arbitrary element in $\mathbb{R}$ be given the name $x$. But when people talk about varaible, it seemes like variables are subject to change.
Consider the production fucntion in economics $Q(K,L)=K^{.5}L^{0.5}$
It is intutive to call $K$ and $L$ variables. Sometimes, people even describe the function as
$Q=K^{.5}L^{0.5}$
and call $Q$ a variable instead of function.
It also seemes popular in many textbooks to write the following:
$Q=Q(x)$
Also consider OLS linear regression, practioners usally write
$\mathbb{E}[y]=\alpha +\beta x$
and treat $x,y$ as variables, while mathematicians often write
$\mathbb{E}[Y\mid X=x]=\alpha + \beta x$
where $Y,X$ are random variables, which are functions, and $x$ is a variable. Motivated by the examples above, it seems adequate to define a varaible as a random variable, or a function. Then a variable can take a varieties of values and its definition can be statisfactory resolved on the basis of material set theory; since a variable will be a function and a function is a set, a variable will be a set.
Help to make my question concise and a satisfactory answer are greatly apprecaited. I am not looking for a philosophical answer.
There is a lot of ambiguous notation in practice of math, especially in calculus and analysis.
The notion of a variable is tightly connected to the notion of a type. One of the (informal) definitions of a type is that a type is the range of significance of a variable.
When asserting that $x\in\mathbb{R}$, it means that $x$ has a type which is equipped with the structure of real numbers. Actually we should say something like "$x$ is of a type $A$, and $A$ has the structure of $\mathbb{R}$".
Then, for example, there may be some other variable $y$ of a type $B$ which also has the structure of $\mathbb{R}$, but $x$ and $y$ are not allowed to inter-operate in general, if only we don't know that $A=B$.
So here the algebraic structure and the carrier are (ambiguously!) denoted by the same symbol $\mathbb{R}$.
Another ambiguous notation is to call a function and it's value on an implicit arguments by the same name.
So for example when one speaks that $Q = \text{an expression on } x$, they mean that $Q$ is the value of an implicit function on a fixed argument $x$, and they often denote that implicit function by the same name as the value, so to write "$Q=Q(x)$".
P.S. Your idea of defining a variable via set theory is outdated at best, in modern mathematics sets are quite not basic notion, but type, variable and function are. Not to speak about that "random variable" has quite different meaning in the rest of mathematics than in statistics.