# Need Help undertanding part of Substitution Theorem for Well-Formed Formulas

Okay so just for reference I'm reading the proof of the Substitution Theorem for Well-Formed Formulas on proof wiki, link below.

https://proofwiki.org/wiki/Substitution_Theorem_for_Well-Formed_Formulas

Everything makes sense except for case involving the quantified expression.

let:

B,A be wff's

q be a quantifier ( either ∃ or ∀)

y,x be variables

t a term

C[t\x] be the substitution instance of the wff C, substituting t for x.

Now let A be a wff such that, A = qyB

In the proof, when the case for the quantified formula is handled, it is assumed that t is free for x in A, there are two cases in which this can happen. one of the cases is that x does not occur free in A.

my question:

if x does not occur free in A, then does that not just mean that x does not occur free in B or that x = y ? I don't understand why the proof jumps to A[t/x] = A.

I understand that by definition if x = y then A[t/x] = A, so does that mean that somehow x is made to occur free in B?

Any help is welcome, I don't know much on this subject I've only read random free textbooks on the web on foundations of first order logic.

• If formula A is like $\exists y B$, to say that term $t$ is free for $x$ in $A$ means that $t$ has no $y$ inside; if so, when we replace $t$ in place of $x$ into $A$ [i.e. $\exists y B$] the (obviously) free occurrence of $y$ in $t$ will be "captured" by the $\exists y$ quantifier. Jul 19, 2022 at 6:46
• Thus, to say that $t$ is free for $x$ in $A$ means two cases: (i) there is no $x$ free in $A$: trivial case that means that $A[t/x]=A$ i.e. no substitution at all. And (ii) $y$ does not occur in $t$, in which case we can freely proceed with the substitution $A[t/x]=\exists y B [t/x]$. Jul 19, 2022 at 6:47

It is nice that the ProofWiki offers the details of a proof which are not mentioned in the source book of the article, Kenneth Kunen's Foundations of Mathematics. The proof can be presented as follows:

The inductive hypothesis is

$$\mathrm{val}_{\mathfrak{A}}\,\phi(x\gets\tau)[\sigma] = \mathrm{val}_{\mathfrak{A}}\,\phi[\sigma + x/a]\mathrm{\text{ where }}\mathrm{val}_{\mathfrak{A}}\,\tau[\sigma] = a$$

The task is to show that this is true for any formula $$\phi$$ whatever form it has. At present, we shall work out the quantified case.

It should be remarked that $$\tau[\sigma] = a$$ does not necessarily imply that $$\sigma$$ assigns $$a$$ to a variable $$\tau$$, for $$\tau$$ may be a compound term built up from a function. To illustrate briefly, suppose we work with an algebraic structure; $$\tau$$ can be $$2x$$ and $$\sigma$$ assigns $$a/2$$ to $$x$$ and $$\tau$$ takes the value $$a$$.

Let us comprehend clearly what the hypothesis tells:

• $$\mathfrak{A}$$ is a structure for a first-order language $$\mathcal{L}$$.
• $$\phi(x\gets\tau)$$ is the formula obtained by replacing all free occurrences of $$x$$ by $$\tau$$.
• $$\sigma$$ is a semantic assignment and $$\sigma + (x/a)$$ is the assignment just the same as $$\sigma$$ for all variables except for the variable $$x$$ that is assigned to $$a$$.

To make the discussion concrete, let us consider a formula $$\phi$$ which has the form $$\exists y\psi$$ (the same argument can be followed for the case of universal quantification). Thus, inductive hypothesis can be used on $$\psi$$ as well:

$$\mathrm{val}_{\mathfrak{A}}\,\psi(x\gets\tau)[\sigma] = \mathrm{val}_{\mathfrak{A}}\,\psi[\sigma + x/a]$$

where $$\mathrm{val}_{\mathfrak{A}}\,\tau[\sigma] = a$$.

$$\tau$$ is a term free for the variable $$x$$, so it is legitimate to replace $$x$$ with $$\tau$$. Since $$\tau$$ is free for $$x$$,

• either: $$x$$ is bound in $$\phi$$,
• or: $$y$$ does not occur in $$\tau$$, otherwise it would get captured by $$\exists y$$.

In the former case, $$x$$ is, so to say, a dummy variable (one could use any other variable) and the value assigned by $$\sigma$$ does not make difference. Thus, we do not need the inductive hypothesis to get the result. Hence,

$$\phi(x\gets\tau) =\phi$$

Notice that, in the notation of the present context, a parenthesised variable is adjoined to the formula name if the variable we deal with is free. Here, $$\phi$$ by itself may still be an open formula having, say, a variable $$z$$ free, but we restrict the present discourse to the variable $$x$$.

In the latter case (where $$y\neq x$$ clearly), we have by the definition of existential quantification (indicated by an underbraced $$\exists$$):

$$\mathrm{val}_{\mathfrak{A}}\,\phi(x)[\sigma] = \mathrm{val}_{\mathfrak{A}}\,\psi(x)[\underbrace{\sigma + y/b}_{\exists}]$$

and

$$(*)\;\mathrm{val}_{\mathfrak{A}}\,\phi(x\gets\tau)[\sigma] = \mathrm{val}_{\mathfrak{A}}\,\psi(x\gets\tau)[\sigma + y/b] = \mathrm{val}_{\mathfrak{A}}\,\psi(x\gets\tau)[\sigma']$$

where $$b$$ ranges over the universe of $$\mathfrak{A}$$ to instantiate $$y$$ and $$\sigma$$' is another assignment that is equal to $$\sigma + y/b$$.

Since $$y$$ does not occur in $$\tau$$, what $$\sigma$$ assigns to $$y$$ does not interfere with the value of $$\tau$$ (indicated by an underbraced $$\sigma$$'):

$$\mathrm{val}_{\mathfrak{A}}\,(\tau)[\underbrace{\sigma + y/b}_{\sigma'}] = \mathrm{val}_{\mathfrak{A}}\,(\tau)[\sigma] = a$$

Hence, the assignments $$\sigma$$ and $$\sigma$$' does not differ as regards the assignment of $$\tau$$. On this basis, we apply the induction hypothesis with $$\psi$$ and $$\sigma$$':

$$\mathrm{val}_{\mathfrak{A}}\,\psi(x\gets\tau)[\sigma'] = \mathrm{val}_{\mathfrak{A}}\,\psi[\underbrace{\sigma + y/b}_{\sigma'} + x/a]$$

Referring to (*), we can write

$$(\dagger)\;\mathrm{val}_{\mathfrak{A}}\,\phi(x\gets\tau)[\sigma] = \mathrm{val}_{\mathfrak{A}}\,\psi[\underbrace{\sigma + y/b}_{\sigma'} + x/a]$$

and

$$(\ddagger)\;\mathrm{val}_{\mathfrak{A}}\,\psi[\underbrace{\sigma + y/b}_{\exists} + x/a] = \mathrm{val}_{\mathfrak{A}}\,\phi[\sigma + x/a]$$

From $$(\dagger)$$ and $$(\ddagger)$$, we infer the result. The double use $$\sigma$$' (i.e., $$\sigma + y/b$$) indicated by the underbraces can be pointed as the key idea.

It may be more beneficial to study the website together with Kunen's book of which a preprint copy is freely available on the Web.