What is the formal definition of a variable?

Solution 1:

A variable is a carrier for something--i.e. it represents something. We usually define a variable to belong to a set, for instance $x\in\mathbb{R}$ means that when we see the variable $x$, it represents some value from the real numbers. Most things involving variables imply first order logic--it's just we don't normally think of it that way.

As an example solve each of the following two equations (for x, a real number): $x^2 = -1$ and $x^2 = 1$. When we ask you to solve an equation the very first thing you might do is check whether or not there is a solution--this is a first order formula: $\exists x \in \mathbb{R} : x^2 = -1$ which is read: "there exists a value from the set of real numbers, which we call $x$, such that the square of this value, $x$, is negative one." If this expression is true, then we may be able to find the value or values of real numbers that make this true (theoretically we can always find the value, if it exists, but it, or they, may be very difficult to find).

So for the first equation, there does not exist a real value such that its square is negative one and thus this equation has no solutions. However, for the second equation, there are real values whose square gives positive one and we can find those values. We say that $x = 1$ or $x = -1$. What we are really saying is that $1$ and $-1$ are the two existent real numbers whose value squared gives positive one (the two real values that make the boolean expression $x^2 = 1$ true). The $x$ is just a convenient way to put a "place-holder" while we still do not know the particular values we intend for $x$ to represent.

edit: More rigorous Definition of a Variable

Essentially a variable is a symbol, which can be anything--including symbols for sets, functions, operators, etc.! A Signature defines the set of symbols in a language, $s_\text{func}$ and $s_\text{rel}$, and some properties of those symbols. The set $s_\text{func}$ consists of symbols which represent functions (which includes variables and constants like $x$ and $1$, respectively). The set $s_\text{rel}$ defines relational operators such as $=$, $\leq$, $\geq$, etc. The final piece of the signature is a set of functions, $ar$, each of which assigns an arity for a particular symbol. An arrity of $n$ means this symbol requires $n$ inputs (so something like $+$, defining addition, would have arrity $2$ since it requires two inputs, e.g. $a + b$).

As an example, I may have $S: \langle \{2, 3, 5,x, +, - \}, \{=\}, ar\rangle$. Each of the constants has arity $0$ (which is defined in $ar$) which means that its interpretation will be a single value from a domain. The variable $x$, is actually a function of arity $1$! It requires at least one input value to be interpreted. Even if $x$ represents a vector value, it still requires only a single input which is a single value from domain set $\mathbb{D}^n$ (where $n$ would be the arity of the vector). The two symbols $+$ and $-$ have arity $2$--they each require two inputs and again those inputs could be vector values. Finally $=$ (a relational symbol) is also of arrity $2$--it requires two values to make a comparison.

The interpretation of the symbols defines what they actually mean. So for instance the interpretation of $x$ above would be a function which maps $\{2, 3, 5\} \mapsto \{2, 3, 5\}$ such that each element is mapped to itself (i.e. $x(2) = 2$, $x(3) = 3$ and $x(5) = 5$). The constants just represent particular values from the set of $\mathbb{I}$. The plus and minus symbols define functions which map $\mathbb{I}\times\mathbb{I} \mapsto \mathbb{I}$ and so on. So I can use this above signature to solve an equation:

$$ x + 3 = 5 \\ x = 5 - 3 = 2 \\ x = 2 $$

All of the symbols I used in solving that equation are defined by the signature above and a proper interpretation (which I partially explained--although certainly not formally).

Solution 2:

You can see Categorial grammar and, in detail : Sara Negri & Jan von Plato, Structural Proof Theory (2001), Appendix A.2 : CATEGORIAL GRAMMAR FOR LOGICAL LANGUAGES [page 221].

In propositional logic, no structure at all is given to atomic propositions, but these are introduced just as pure parameters $P, Q, R$,..., with the categorizations

$P : Prop, Q : Prop, R : Prop$, ...

Connectives are functions for forming new propositions out of given ones. We have the constant function $\bot$, called falsity, for which we simply write $\bot : Prop$.

Next we have negation, with the categorization :

$Not: (Prop)Prop$.

And so on ...

We can put predicate logic into [this] framework [...] if we assume for simplicity that we deal with just one domain $\mathcal D$. The objects, individual constants, are denoted by $a, b, c$,.... Instead of the propositional constants $P, Q, R$,..., atomic propositions can be values of propositional functions over $\mathcal D$, thus categorized as $P : (\mathcal D)Prop, Q : (\mathcal D)(\mathcal D)Prop$, and so on. Next we have individual variables $x, y, z$ , . . . taking values in $\mathcal D$. Following the usual custom, we permit free variables in propositions. Propositions with free variables are understood as propositions under assumptions, say, if $A : (\mathcal D)Prop$, then $A(x) : Prop$ under the assumption $x : \mathcal D$. Terms $t,u,v$,... are either individual parameters or variables. The language of predicate logic is obtained by adding to propositional logic the quantifiers Every and Some, with the categorizations

$Every : ((\mathcal D)Prop)Prop$

$Some : ((\mathcal D)Prop)Prop$.

These are relative to a given domain $\mathcal D$. Thus, for each domain $\mathcal D$, a quantifier over that domain is a function that takes as argument a one-place propositional function $A : (\mathcal D)Prop$ and gives as value a proposition, here either $Every(A)$ or $Some(A)$.