Q: On Soundness proof in Tourlakis 2003

Question

In p.59 of Lectures in Logic and Set Theory, Tourlakis proves the inductive step for the E-introduction rule of Soundness.

He uses a proof by contradiction stating that $B'[x \leftarrow \bar i] \implies C'$ interprets as false. But since it's an instance of $B \implies C$, it must interpret as true by IH s- thus contradiction.

But what if $x$ is not a free variable in $B$? Wouldn't the substitution $B'[x \leftarrow \bar i]$ output an entirely new wff that cannot be an instance of $B$?

My understanding of $B'$ is that it's a valid instance for any free variable substitution (into imported constant), so is non-free variable substitutions safe?

Answer 1

We want to prove the soundness of the $\exists$-introduction rule [page 36] :

from $B \to C$, derive $(\exists x) B \to C$, provided that $x$ is not free in $C$.

The question is :

But what if $x$ is not a free variable in $B$ ? Wouldn't the substitution $B′[x ← \overline i]$ output an entirely new wff that cannot be an instance of $B$ ?

If $x$ is not free in $B$, either $x$ is not present in the formula or $B$ is $((∃y)B')$ and $y = x$.

In the second case [see page 33] we have that $B[x \leftarrow t]$ is $B$ itself.

In both cases, there is no $x$ free to be "filled" with $\overline i$ and we have that : $B[x \leftarrow \overline i]$ is $B$ itself.

Thus, the assumption $((∃x)B)^{\mathfrak I} =$ t amounts to $B^{\mathfrak I}=$ t.

See Def.I.5.6 [page 55] : (4) If $A$ is $(∃x)B$, then $A^{\mathfrak I} =$ t iff $(B [x ← \overline i])^{\mathfrak I} =$ t for some $i ∈ M$.

---

Why we need the proviso : $x$ not free in $C$ ? In order to ensure the soundness of the rule.

Recall that [page 56] soundness means : "all the theorems of the theory are logically implied by the nonlogical axioms. Clearly then, all [logical] theorems are universally valid."

Consider now the arithmetical formula $(x=0) \to (x=0)$; it is a tautology and thus it is universally valid.

If we apply the $\exists$-introduction rule to it (forgetting of the proviso) we get : $\exists x (x=0) \to (x=0)$, which is clearly not $\mathbb N$-valid.

---

---

New details about the proof.

We have to read carefully the proof page 59. It is a proof by contradicition, i.e. it assumes that the premise $B \to C$ of the rule is true and that the conclusion $\exists x B \to C$ is false.

First observation : we have to assume that $x$ occurs free in $B$, otherwise the syntactically correct formula $\exists x B$ will be equivalento to to $B$ and the proof is trivial.

Second observation : the proof does not preclude that there are other free variables in $B \to C$; this is the reason why the author speaks of "instances". But, again, we can forgive this point and consider for simplicity only $x$.

Now, back to the proof : to say that the conclusion of the rule is false amounts to saying that $\exists x B$ is true and $C$ is false.

In turn, $\exists x B$ is true when we have that $B[i]^{\mathfrak I}$ is true, for some $i \in M$.

Thus (with the above simplification) we have that :

$B[i]^{\mathfrak I}$ is true and $C$ is false, and thus $(B \to C)[i]^{\mathfrak I}$ is false.

This last step is licensed precisely because $x$ is not free in $C$, and thus we can "move" the "$i$-instance" from $B$ alone to the formula $B \to C$.

Now the final step : why the fact that $(B \to C)[i]^{\mathfrak I}$ is false contradicts the assumption of the proof that $B \to C$ is true ?

We have to step back to the semantical specifications [page 55] : for a formula whatever (not necessarily closed) :

we say that $A$ is valid in $\mathfrak M$ (or that $\mathfrak M$ is a model of A) iff for all $\mathfrak M$-instances $A'$ of $A$ it is the case that $A^{\mathfrak I} = \text t$.

But $(B \to C)[i]^{\mathfrak I}$ is an $\mathfrak M$-instance of $B \to C$ and we have assumed that $B \to C$ is true : contradiction !

See also counter-example above.