Free variables in definitions

Question

Consider the epsilon delta definition of the limit below, as it is usually stated:

the limit of f as f approaches a is L if and only if, for all ε > 0, there is a δ > 0 such that for all x, 0 < |x - a| < δ implies |f(x) - L| < ε.

In this form, before the "if and only if", f(x), L, and a are not bound and therefore x, L and a must be considered free in the formula as a whole.

Question 1. Is it considered good practice, in logic, to specify formulas containing free variables? If so, what are the semantics of free variables in formulas containing them?

Question 2. When proving that a function has a limit, we replace f(x), L and a with terms (e.g. L = 0, f(x) = x^2, a = 0). What logical rule of inference allows us to do this? If there is no such rule of inference, then the above definition would have to be considered shorthand for something like

for all f, L and a, the limit of f as f approaches a is L if and only if, for all ε > 0, there is a δ > 0 such that for all x, 0 < |x - a| < δ implies |f(x) - L| < ε.

Then, we could use universal specification to replace f, L and a with specific functions or constants. But that leads to question 3.

Question 3. To what extent can we treat function symbols (e.g. f), as variables? Can we quantify function symbols?

Answer 1

I'm not sure how to answer your second question, but I think I can manage the other two.

Answer 1. A formula with free variables is typically written as something resembling $\varphi(v_1,\ldots,v_n)$ where $v_1,\ldots,v_n$ are the free variables and the bound variables are not among $v_1,\ldots,v_n$. When written this way, $\varphi(v_1,\ldots,v_n)$ does not have a truth value; but if $\mathcal M$ is a model and $a_1,\ldots,a_n \in |\mathcal M|$ as elements, then either $ \mathcal M \models \varphi(a_1,\ldots,a_n)$ or $\mathcal M \models \neg \varphi(a_1,\ldots,a_n)$. (I'm assuming this is the sort of answer you're looking for when you're asking about semantics.)

Answer 3. You can quantify over function symbols, but then you would be leaving first-order logic and venturing into second-order logic. (Note that if you want to quantify over a symbol $f$, then $f$ should not be in your language $\mathcal L$ because then it would have a fixed interpretation in any $\mathcal L$-structure.) In first-order logic, quantifiers operate on individual elements in the a model, but second-order logic allows for quantification over sets. For example, $\forall x \exists y (y>x)$ is a first order statement that we could interpret in $\mathbb N$ with $x,y \in \mathbb N$. However,

$$\forall X((0 \in X \wedge (n \in X \rightarrow n+1 \in X)) \rightarrow \forall n(n \in X)$$

uses a sort for $X \in P(\mathbb N)$, making it second-order.

The reason you can't quantify over function symbols in first-order logic is because they implicitly represent sets. A formula $\varphi(v_1,\ldots,v_n):=\exists f \psi(f,v_1,\ldots,v_n)$ where we try to quantify over functions may be interpreted as follows: if $\mathcal M$ is an $\mathcal L$-structure and $a_1,\ldots,a_n \in |\mathcal M|$, then $\mathcal M \models \varphi(a_1,\ldots,a_n)$ if there is some expansion $\mathcal M^*$ to the language $\mathcal L \cup \{f\}$ in which $\mathcal M^* \models \theta(a_1,\ldots,a_n)$ where $\theta(\bar v)$ is the formula we get from $\psi(f,\bar v)$ by interpreting $f$ as function symbol instead of a variable. The reason this entails quantifying over a set is because $f$ is essentially a subset of $|\mathcal M|^2$ that is explicitly represented when we move up to $\mathcal M^*$.

Answer 2

Question 1. I can give you this hint : S.C.Kleene, Mathematical Logic (1967, Dover reprint), pag.207 :

in taking Axiom 14 [i.e. first-order Peano's Axiom : $a'= b' \rightarrow a = b$ (where $a'$ is the successor of $a$)] for elementary number theory, we intend to assume that, for every pair of natural numbers $a$ and $b$, if $a+1 = b+1$, then $a = b$. So Axiom 14 is to be regarded as synonymous with its closure $\forall a \forall b (a'= b' \rightarrow a = b)$.

So we can say that in common mathematical practice, free variables are implicitly universally quantified.

Question 2. The logical rules involved with the universal quantifier are :

$\forall xA(x) \vdash A(t)$ (in Natural Deduction : $\forall$-elimination)

if $\vdash A(x)$ then $\vdash \forall xA(x)$ (in Natural Deduction : $\forall$-introduction)

In other words, $\forall$-elimination allows you to derive, form a universally quantified theorem, an instance of it [i.e.to derive from $\forall a \forall b (a'= b' \rightarrow a = b)$ its instance $\forall a (a'= 0' \rightarrow a = 0)$, where $0'$ is the successor of $=$, i.e. $1$]

$\forall$-intro license the derivation of a universally quantified formula from a "generic" instance of it.

Question 3 Rif. to Maxwell's answer.

In general, in order to "formalize" your calculus theorem regarding limits, you must use a formal language and, in order to prove it, you need axioms.

Case 1. If your language is first-order language and you states axiom for real numbers (in technical words, the axioms for a complete ordered field) your universe of dicourse is made of the set $\mathbb R$ of real numbers only. So you cannot speak of functions from $\mathbb R$ to $\mathbb R$.

Case 2. Many-sorted language assume a universe of discourse "partitioned" in many non-overlapping domains; e.g. a domani for (real) numbers and a domain for functions. The formulae must be rewritten using to predicates: $N$umber(x) and $F$unction(x), like :

$\forall f \forall \epsilon ( F(f) \land N(\epsilon) \land (\epsilon > 0) \rightarrow .....$

Case 3. Move to second-order language.

Case 4. Use set theory, like ZFC. This a a first-order theory that's able to "speak of" every mathematical object, because all of them (numbers, functions, etc.) can be defined as suitable sets. Of course, you need set's axioms.

Answer 3

There is a standard convention that free variables not explicitly introduced are universally quantified.

Indeed, this is actually true of the usual formal rules of the first-order predicate calculus: the way to deduce statements of the form $\forall x. \phi$ is to deduce (from various axioms and modus ponens) $\phi$, a formula with a free variable $x$, and then apply the generalisation rule, which says that if none of the hypotheses of the theory used to deduce $\phi$ had $x$ as a free variable, then you may bind $x$ in a universal quantifier.

This sounds weird at first, but it's actually pretty easy and sensible to work with. In particular, if you are trying to prove tautologies, you are working from the empty theory, so the precondition is trivially satisfied. What's then going on is that if you have any free variables, you must have introduced them "freshly" yourself, you must therefore know nothing about them, and hence any argument that works for them will work for anything in their place. So typically working from an empty theory you can introduce and discard universal quantifiers at the top level however and whenever you wish. On the contrary, if your ambient theory contained something like $x > 2$, then certainly statements you proved about $x$ would not be able to be generalised.

Answer 4

I posted a similar question here: http://www.reddit.com/r/math/comments/1sxj6h/logic_free_variables/.

After discussing the question there, and thinking about it myself, I concluded the following. To quote myself:

My main question was question 2, with questions 1 and 3 aiming to answer it. As time has passed, I've thought of a clearer way of stating it:

How do we know that

for all ε > 0, there is a δ > 0 such that for all x, 0 < |x - a| < δ implies |f(x) - L| < ε.

is satisfied by

for all ε > 0, there is a δ > 0 such that for all x, 0 < |x - 0| < 1 implies |3 - 3| < ε

?

After thinking about it, I think you would need the following set of assumptions: f(x) = 3, δ = 1, a = 0. You could then derive the following in succession.

f(x) = 3, δ = 1, and a = 0 implies that for all ε > 0, there is a δ > 0 such that for all x, 0 < |x - a| < δ implies |f(x) - L| < ε

f(x) = 3, δ = 1, and a = 0 implies that the limit as x approaches a of f(x) is L

f(x) = 3, δ = 1, and a = 0 implies that the limit as x approaches 0 of 3 is 3

To answer my question 1, I found the following: http://math.andrej.com/2012/12/25/free-variables-are-not-implicitly-universally-quantified/

To answer question 3, I found out from the reddit discussion, and the other answers here that I would have to work in second order logic, because to quantify a function is to quantify a set of ordered pairs.