0
$\begingroup$

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.

$\endgroup$
2
  • $\begingroup$ 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. $\endgroup$ Jul 19, 2022 at 6:46
  • $\begingroup$ 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]$. $\endgroup$ Jul 19, 2022 at 6:47

1 Answer 1

0
$\begingroup$

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.

$\endgroup$

You must log in to answer this question.

Not the answer you're looking for? Browse other questions tagged .