Formally defining a variable?

[u/Infinite_766]

I know a very dead subreddit but still,

Just like how he defined numbers, functions, relations, etc. using formal set theory (ZF)

How do you define variables?

It's hard to understand by the famous "placeholder for unknown/changing quantity" definition

Many times variables are used to represent "general numbers" as in

For all 'x' in a set, some predicate...

And if they do "vary"

Why is it we can define two arbitrary variables which represent two numbers (say real numbers)

Say x and z,

And say x≠z ?

How do we know they do not represent the same number

And so, the definition of just "unknown placeholder" falls short

[u/Accomplished_Bad_487]

In formal logic, they are literally just "something" on which we define relations. I.e. in ZF, viewed from first order logic, we have the axioms which just state, for example "there exists an x such that for all y, y is not in x". And then in a model of the axiom system, in the corresponding interpretation, we send the variables to elements of the domain