Formula term-substitution in first order logic

Question

Let $F_u(s)$ denote the first order sentence with the term $s$ substituted for all instances of $u$ (where $u$ is any free variable). There is an exercise that asks me to define $F_u(s)$ for all possible formulas $F$ and then prove that $F_u(s)$ is a formula.

My book defines that if $F$ is a formula then let $(Qx)F_u(x)$ be a formula where $x$ is a bound variable and $u$ is any free variable of the language.

With the induction hypothesis that $G_u(s)$ is a formula for some formula $G$. (I have skipped the base case of the atomic formulas) I have defined $F_u(s) : = ((Qx)G_u(s))_v(x)$ iff $F := (Qx)G_v(x) $ where $u$ and $v$ in general are any free variable but could be the same variable and $Q$ is any quantifier). This can be proved a formula by straightforward application of the IH and the definition 'if $F$ is a formula then $(Qx)F_u(x)$ is a formula'.

However, I am in a debate with someone who thinks this it should be $F_u(s) : = ((Qx)G_v(x))_u(s)$. But, I don't see how my definition is wrong.

Answer 1

In predicate logic, substitution is defined in the obvious way for atomic formulas: $P(t_1,\ldots, t_n)[s/x] := P(t_1[s/x],\ldots, t_n[st/x])$, and we extend it naturally to manage formulas with connectives.

The only "tricky" case is that of quantifiers:

$(∀y \varphi)[s/x] := ∀yϕ[s/x] \text { when } x \ne y \text { and } ∀yϕ \text { when } x = y$,

and similar of $\exists$.

In plain terms: if $F:=∀xG$, then the result of replacing free occurrences of $u$ with $s$ left the formula $F$ unchanged when $u$ is $x$.

---

Now, going back to your notation, we start with a formula $G$ with $v$ free. Then we quantify it to get $F := \forall x G_v(x)$ where we have replaced every occurrence of $v$ with $x$ [sylly example: $G := (v>0)$ and $F := \forall x (x > 0)$].

Now we want to apply the substitution: $s$ in place of $u$, and we have the two cases above: if $s$ is $x$, no substitution at all.

If $s \ne x$, then we have simply to replace $u$ with $s$ in $G_v(x)$ [silly example again: $G := (v+u>0)$ and $F := \forall x (x+u > 0)$; then: $F_u(s) := \forall x (x+s > 0)$].

If you adopt the convention that terms and bound variables are disjoint collections, the case $s=x$ cannot occur, and thus:

if $F := (Qx)G_v(x)$, then $F_u(s) := [(Qx)G_v(x)]_u(s) := (Qx)[G_u(s)]_v(x)$.

---

Regarding now the induction proof, we know that $G_u(s)$ is a formula by IH and we have reduced the case $F_u(s)$ to that of $[G_u(s)]_v(x)$.

But $G$ is a formula of lower complexity with respect to $F$ [removing the quantifier, we have to restore the original free variable $v$] and thus the IH applies: $G_u(s)$ is a formula.

Using again the example above with: $G:=(v+u>0)$ and $F:=∀x(x+u>0)$, we have that $F_u(s)$ is $\forall x [(v+u>0)_u(s)]_v(x)$ and the substitution $(v+u>0)_u(s) := (v+s>0)$ is correct by IH.

---

---

The feature of using two sorts of variables: $x,y,z$ for bound variables and $a,b,c$ for free ones (called: parameters), is common to the"tradition of Proof Theory; see G.Gentzen (1936), English transl.page 70.

How are they managed? We can see the rules for quantifiers in Natural Deduction:

$(\forall \text I) \ \ \text {If } \Gamma \varphi[x/a], \text { then } \Gamma \forall x \varphi$

where $\varphi [x/a]$ denotes the operation of substitution, that is, of replacing all free occurrences of $x$ in $\varphi$ with a parameter $a$.

Thus, when we remove a quantifier we have to replace the bound variable $x$ occurring in the scope of the quantifier with a (free) parameter $a$, provided that $a$ is new (i.e. it does not occur in the formula).

This means that, with e.g. $F := (∀x)(x=u)$, the removal of the quantifier must produce $(v=u)$ and not $(u=u)$, because in the second case the re-introduction of the quantifier will produce $G := (∀x)(x=x)$, which is not the same as $F$.

Answer 2

Actually, $(Qx)[G_\mu(s)]_\nu(x)$ is not well defined (where $\mu$ and $\nu$ are any free variable). For example, Let $s:=v$, $G:= P(v) $ , $H:= P(u) $ and $F:= (\forall x) P(x) $. Note that $F \approx (\forall x) G_v(x) \approx (\forall x) H_u(x)$. Then

(1) $F_u(s) \approx ((Qx)G_v(x))_u(s) \approx ((Qx)G_u(s))_v(x) \approx ((Qx) P(v) )_v(x) \approx (Qx) P(x) $ .

(2) $F_u(s) \approx ((Qx)H_u(x))_u(s) \approx ((Qx)H_u(s))_u(x) \approx ((Qx) P(v))_u(x) \approx (Qx) P(v) $.

So the definition $F:=(Qx)G_\nu(x)$ iff $F_\mu(s) := (Qx)[G_\mu(s)]_\nu(x)$ is not well defined.

Instead define $F:=(Qx)G_\nu(x)$ iff $F_\mu(s) := (Qx)[G_\nu(x)]_\mu(s)$.

We will also use: (3) that for any forumla $G$, then $(Qx)G_\nu(x)$ is also a formula.

Now to prove $F_\mu(s)$ is a formula. (Parentheses will be dropped for readability).

I will leave out the base case proof for the atomic formulas. Define the length of a formula to be the total number connectives (including $\lnot$) and quantifier symbols. Now assume that for all formulas of length $n$ that the operation $_\mu (s)$ (for any free variable $\mu$ and any term $s$) applied to that formula yields a formula. Let $G$ be a formula of length $n$.

Note that $G_ \nu (x) \approx G_ \nu (\gamma) _\gamma (x) $ for any free variable $\gamma$. Therefore we have $(Qx)G_ \nu (x) _ \mu(s) \approx (Qx)G_ \nu (\gamma) _\gamma (x)_ \mu(s)$. Now put the extra constraint that $\gamma \not \in FV(s), FV(G)$ and $\gamma \not \approx \mu$ and $\gamma \not \approx \nu$ (we can always find such a $\gamma$ since there are infinitely many free variables).

Because of the conditions on $\gamma$ we now have $(Qx)G_ \nu (\gamma) _\gamma (x)_ \mu(s) \approx (Qx)G_ \nu (\gamma) _\mu (s)_ \gamma(x)$. $G_ \nu (\gamma)$ is a formula from the IH. Also, it is a formula of length $n$ since no new connectives or quantifiers were added. Therefore we can apply the IH again to get that $G_ \nu (\gamma) _\mu (s)$ is a formula. Then from (3) $(Qx)G_ \nu (\gamma) _\mu (s) _\gamma(x)$ is a formula which implies $(Qx)G_ \nu (x) _ \mu(s)$ is a formula.