Existence Introduction on Kleene's Introduction to Metamathematics

Question

Existence introduction in Kleene's IM is stated as $A(t) \vdash \exists x A(x)$. The way the notation $A(t)$ in introduced by Kleene (page 78), make me think that all occurrences (instances) of t in $A(t)$ must be substituted by $x$. However, this is not the case, as explained here.

Is this fact explained or explicitly used anywhere on Kleene's IM? If it's a yes, could you point me in the right direction? Thanks

Answer 1

The notation for substitution as used in the existential introduction rule is defined on p. 78:

If substitution is to be performed for $x$, we first introduce a composite notation such as "$A(x)$" for the substituend [...]. The result of substituting $t$ for $x$ in $A(x)$ is then written $A(t)$.

The existential introduction rule can then be defined in terms of ordinary substitution, namely in terms of the substitution going the other way round: In $A(t) \vdash \exists x A(x)$, $A(t)$ is the result of replacing every free occurrence of $x$ in $A(x)$ with $t$.

There may be other occurrences of $t$ in $A(t)$ that are not the result of substitutions for $x$, which is why if one explains the replacement the other way round (as in the answer to the post linked), not all occurrences of $t$ need to be replaced by $x$. And note that that partial replacement of $x$ for $t$ is not substitution, since 1. $t$ can be a constant but only variables can undergo substitution, and 2. substitution always replaces all occurrences.

Answer 2

On page 80, Kleene says that $A(b)$ is the result of substituting $b$ for all free occurrences of $x$ in $A(x)$. Here, $b$ is supposed to be some constant, but it is clear that when you consider any variable-free term $t$, the same idea holds holds: $A(t)$ is the result of substituting $t$ for every free occurrence of $x$ in $A(x)$

OK, so why does this allow one to go from, say, $s(a)=s(a)$ to $\exists x \ x =s(a)$?

Well, in this example, the term $t$ is $s(a)$, and $A(x)$ is $x=s(a)$. And, if you substitute $s(a)$ for every free $x$ in this $A(x)$, you do indeed get $s(a)=s(a)$, which is $A(t)$.

So, the whole 'trick' to understand the formal rule is to not think of the Existential Introduction rule as substituting $x$ for $t$, but as substituting $t$ for $x$.

Of course, in practice, you do think of it as substituting $x$ for $t$ .... and that's ok, as long as you understand that you don't have to substitute all $t$'s with $x$'s. You can, as in the above example, substitute just some of the $t$'s ... and if you really wanted to, you could even decide to not do any substitutions at all. Indeed, from $s(a) =s(a)$ you could infer $\exists x \ s(a) = s(a)$ using Existential Introduction: it still follows the rule!