What are indexed variables formally?

Question

As far as I know, some formal languages allow for indexed variables, that is for any natural number $n$ we have variables $x_1,...,x_n$. I wonder, what are those variables formally? It appears to me that they behave like function symbols, since statements such as $\forall i \in \{1,...,n\}: P(x_i)$, but they can't be functions in the mathematical sense, since indexed variables are introduced way earlier. So, are there axioms that formalize this behavior of a function symbol for those, or how are they actually behaving formally? I think I have not seen any of these axioms thus far. Would it actually be possible to define indexed variables as functions in the mathematical sense?

Answer 1

In predicate logic, which is one of the tags of your question, you have several kinds of symbols: quantifiers, parentheses, logical connectives... and an infinite set of variables.

The use of subscripts for variables is just a way to denote some of the variables. When you write in your question $\forall i \in \{1,...,n\}: P(x_i) $, the universal quantifier is not a logical sentence of first-order language. It is a way to abbreviate the sentence $P(x_1) \wedge \dots \wedge P(x_n)$.