I have a question on equational reasoning in theories, which is made quite often in mathmeatics, and I am trying to make this more formal.
So for my attempt to make this more rigouros, I choosed first-order logic. Suppose a first-order language consisting of relational symbols, variables and the usual connectives and quantifiers is given. Terms and formulas are defined as usual.
Now suppose in my language I have terms $t_i(y)$ with one variable $y$, and terms $s_i(x_1, \ldots, x_n)$ with $n$ variables, and suppose I have $m$ variables $y_1, \ldots, y_m$ and $n$ variables $x_1, \ldots, x_n$ and a formulae $$ \varphi(y_1, \ldots, y_m, x_1, \ldots, x_n) $$ putting certain requirements on my variables (this could be termed axioms, or the theory in which my variables "life").
Further between the variables and terms the following relationsships (or formulae) should hold \begin{align*} t_1(y_1) & = s_1(x_1,\ldots, x_n) \\ t_2(y_2) & = s_2(x_1,\ldots, x_n) \\ \ldots \\ t_m(y_m) & = s_m(x_1,\ldots, x_n). \end{align*} Now the requirement formula $\varphi(y_1,\ldots,y_m, x_1, \ldots, x_n)$ yields that only $r$ variables of the $m$ variables $y_i$ could be choosen freely, also just $s$ of the $x_i$ could be choosen freely (this could be termed degrees of freedom for the variables), now I claim just $r - s$ of the above mentioned formulas involving the terms and variables are independent, i.e. the other could be derived from just $r - s$ of them.
Could this be proven? Are there any approaches in logic similar to my thoughts? Do you get what I was trying to achieve, or does it just sounds like non-sense to you?