I have been wondering about the formalism of what 'exactly' a variable is, and its role in proofs in mathematics. I have seen a few questions here, such as this one: Is there a way of defining the notion of a variable mathematically?. However, I have not fully absorbed the responses to those questions, and I believe this question regards somewhat different notions.
Wikipedia defines a variable as "In mathematics, a variable is a symbol used to represent an arbitrary element of a set". There was a great question (and answers') about the role of arbitrary elements in sets, The role of 'arbitrary' in proofs, and it seems to me that per the definition of a variable, it is exactly a symbol to represent some 'arbitrary' element.
My motivation for this question (and my confusion) comes from the role of using arbitrary elements in proofs. I understand that something of the form $P(x)$ is not a statement, it is an open sentence. However, something of the form $P(2)$ is a statement, since we know exactly the mathematical object we are dealing with. For example the statement, $\forall x \in X. P(x)$ means we have a collection of precise statements $$P(x_1) \land P(x_2) \land P(x_3)....$$
Where now the symbols $x_1, x_2, x_3, ...$ represent a precise and distinct mathematical object, for example the numbers $1,2,3,...$ if the set that we quantify over is $\mathbb{N}$.
The trouble in my mind however is we sometimes have proofs of the form, "Let $x$ be some element in $S$. Then... [reasoning about $x$] $\implies$ [some conclusion]. In this case, we are reasoning about $x$ as we would a particular mathematical object $x_1$, but I don't quite understand how we would do this?
To expand on my doubt: What I am confused by is that for a mathematical object (such as an integer) we have precise and formal definitions/constructions/axioms for these objects. Numbers can be defined in terms of sets, so can ordered pairs, etc. So when we reason about these objects, we are reasoning about some particular well defined 'mathematical object'. But with arbitrary elements/variables, it seems to me that we are saying "OK, this symbol refers to some object in this set, but you don't actually know which one". Since this is the case, how could we construct a definition of such an object, that wouldn't itself need to be expressly defined in terms of ALL the objects it could possibly be? And if indeed it is the case that we cannot, then how can we reason about this 'thing' as if it were a precisely defined mathematical object?
Or does this mean there is some definable set for example, which contains an element $x$ that is an 'arbitrary element' of $\mathbb{Z}$?
My apologies if this question is not a good fit for this stack exchange, I am not sure if this is more related to the philosophy of mathematics, but I have seen a few similar questions on the topic so I thought I would post it here.
EDIT: I had a look at the other question, and I do not believe mine is a duplicate (and I don't think the answers clarified my doubts, though I have perhaps not explained myself properly).
For example in document which the accepted answer quotes of, it says two interesting points: "Roughly speaking, a variable is a symbol for which one substitutes names for some objects, usually a number in algebra. A variable is always associated with a set of objects whose names can be substi- tuted for it. These objects are called values of the variable. (p. 70)" and on another page "There is a subtle quandary here. We want students to have the referents (usually real numbers) for variables in mind as they use the variables. But we also want students to be able to operate on the variables without always having to go to the level of the referent."
However, my doubt is not on what we are doing, or even why we are doing it, but on how we can manipulate this symbol as if it were a referent (as that document puts it). It seems to me a symbol that can be substituted for any elements in a set is different from being an element of said set, so why do we perform the same operations, and use the same logic, on both?
See the post Why is a variable called variable in mathematics.
Variable are used in open formulas:
The details of the semantics of the language dictate "how to read" a formula with free variables.
Usually, we use a "context" [technically called: variable assignment function], i.e. a way to assign a "temporary meaning" to the free variables.
We can compare a free variable to a pronoun of natural language.
To assert "$x$ is Prime" is the same as "it is Prime": its meaning depends on what the context assigns to "it".
In the same way, in roder to read formula $P(x)$, we have to specify an interpretation, e.g. the domain of natural numbers for the quantifiers and the property "to be Prime" for the predicate $P(x)$.
Having done this, the truth value of the formula $P(x)$ and will depend on the "object" we will assign to "it" as reference.
Proof systems for first-order logic have rules for adding and removing the quantifiers.
The first one:
corresponds to the specialization principle : "what holds for all, holds for any".
And the same intuition supports the corresponding elimination rule:
"if something holds for an arbitrary object, then it holds for all objects".
The first rule is quite intuitive, while the second one is a little bit tricky: the crucial point is the clause regarding "the arbitraty object" used to generalize.