Does it make sense to substitute a value in for bound variables?

Question

Consider the identity $$ \forall x \left(\cos^2x+\sin^2x=1\right) \, . $$ Instructors will often illustrate such identities by giving examples. It is common to hear a statement such as

Let $x=\pi/3$. Then the identity states that $\cos^2(\pi/3)+\sin^2(\pi/3)=1$.

However, does it really make sense to say 'let $x=\pi/3$' if $x$ is a bound variable? After all, it wouldn't make sense to write $$ \arcsin(x)=\int_{0}^{x}\frac{1}{\sqrt{1-t^2}} \, dt $$ and then say 'let $t=1/2$', since the integral operator binds the variable $t$.

Moreover, it is clear that this identity also implies that $$ \forall (2x) \left(\cos^2(2x)+\sin^2(2x)=1\right) \, . $$ However, here it wouldn't make sense to 'let $x=2x$' and then proceed. How would such issues would be addressed in mathematical logic? In particular, is the idea of substituting a particular number in for a bound variable well-founded? And if not, how does one justify that the identity $$ \forall x \left(\cos^2x+\sin^2x=1\right) $$ implies both $$ \cos^2(\pi/3)+\sin^2(\pi/3)=1 $$ and $$ \forall (2x) \left(\cos^2(2x)+\sin^2(2x)=1\right) \, ? $$

Answer 1

Whether or not it makes sense does not really depend on some general property of 'bound variables.' It depends on the particular examples.

In the first example, there is a rule that says that from $∀ x. P$ we may deduce $P[x := T]$ for every term $T$ that $x$ may be instantiated to. This is a property/the meaning of the universal quantifier in logic.

In the second example, integration is an operation on functions. The expression $$\frac{1}{\sqrt{1 - t^2}} dt$$ is meant to denote the function of $t$ that the integral is operating on (at least, in the usual explanation of integrals). Substituting for $t$ (eliminating the $dt$) just gets you the value of said function at the point you're substituting in, which may have little to do with the integral.

As was mentioned in the other answer, quantifiers in logic generally bind variables, not arbitrary expressions, so $∀(2x) ...$ is not well-formed, unless $2x$ is meant to be a variable name.

In lambda calculus $λ x. E$ binds the variable $x$ in $E$. The lambda expression denotes a function $f$, and substitution for $x$ in $E$ again gives (an expression for) the value.

The existential quantifier in logic $∃ x. P$ binds the variable $x$ in $P$. Substituting for $x$ in $P$ gives a proposition that can be used to deduce the existential statement. I.E. from $P[x := T]$ we may deduce $∃ x. P$, which is the opposite of the universal quantifier.

So, hopefully it's clear, you can substitute for bound variables if you want, but the relationship between the substituted expression and the quantified expression depends on the quantifier/binder.

Answer 2

Your sentence

Moreover, it is clear that this identity also implies that $$ \forall (2x) \left(\cos^2(2x)+\sin^2(2x)=1\right) $$

is not true. The reason being that

$$ \forall (2x) \left(\cos^2(2x)+\sin^2(2x)=1\right) $$ is not a well-formed first-order logic formula. You use quantifiers on variables. Not on function symbols using variables.