Jtdylktuy

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?

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.