# Formal proof involving $\varphi( v_k / v_l )$

I'd like to show that if $\varphi(v_k / v_l )$ and $\varphi(v_l / v_k )$ are admissible then $[\exists v_k \varphi(v_k)] = [\exists v_l \varphi(v_l)]$ where $[\varphi]$ denotes the equivalence class with respect to $\varphi \sim \psi \iff T \vdash \varphi \leftrightarrow \psi$.

Is the following proof correct?

"$\leq$": We want to show $T \vdash \exists v_k \varphi (v_k) \rightarrow \exists v_l \varphi(v_l)$.

We show $T \cup \{ \exists v_k \varphi(v_k) \} \vdash \exists v_l \varphi(v_l)$:

1. $T \cup \{ \exists v_k \varphi (v_k) \} \vdash \exists v_k \varphi (v_k)$

2. $T \cup \{ \exists v_k \varphi (v_k) \} \vdash \exists v_l \varphi (v_l)$ (by substitution)

Then we apply the deduction theorem to get $T \vdash \exists v_k \varphi (v_k) \rightarrow \exists v_l \varphi (v_l)$. So we have $[\exists v_k \varphi (v_k)] \leq [\exists v_l \varphi (v_l)]$.

Then by the same argument, "$\geq$".

The step I am not sure about is the substitution from 1. to 2. but I don't see why I shouldn't be allowed to substitute since the substitution is admissible by assumption.

Edit

We're using first order logic in the course. The axiom we have that is related to substitution is $\varphi(t) \rightarrow \exists x \varphi(x)$ and $\forall x (\varphi(x)\to \psi)\to (\exists x \varphi(x)\to \psi))$

-
It will depend on whether you have that sort of substitution rule in your formal deductive system. Because you have not said which formal system you are using, it is impossible for anyone else to answer this. Another general strategy, depending on your formal system, is to use existential instantiation followed by existential generalization. – Carl Mummert Feb 9 '12 at 14:29
@CarlMummert Thanks, I wasn't aware of this. I added some more information to the question. – Rudy the Reindeer Feb 9 '12 at 16:22
You must have another axiom that allows you to remove an existential quantifier by substituting a term for the variable? These axioms should come in pairs. – Carl Mummert Feb 9 '12 at 18:34
@CarlMummert The only other axiom involving $\exists$ is $\forall x(\varphi(x) \rightarrow \psi) \rightarrow (\exists x \varphi(x) \rightarrow \psi))$. The axioms are listed in this document starting on page 4. – Rudy the Reindeer Feb 9 '12 at 19:17
Yes, that other one is the key. It is the axiom that corresponds to existential instantiation in this author's system. I explained how they are related in my answer. In general, to ask about formal proofs you have to give details about the entire proof system. – Carl Mummert Feb 9 '12 at 20:12

This answer pertains to the system presented here, which is a relatively typical Hilbert-style system.

First, you cannot use a simple substitution. By definition, a substitution only replaces free variables. So if you try to substitute $y$ for $x$ in $(\exists x)\phi(x)$ you get back the same formula $(\exists x)\phi(x)$. This is a very common convention, and is not at all unique to this author.

To prove in this author's particular system that $(\exists x)\phi(x)$ implies $(\exists y)\phi(y)$, where $y$ is admissible for $x$ in $\phi$, you can use rule $L_{15}$ in the following form: $$(\forall x)[\phi(x) \to (\exists y)\phi(y)] \to [(\exists x)\phi(x) \to (\exists y)\phi(y)]$$ This is a correct instance of $L_{15}$ because in $(\exists y)\phi(y)$ all the free occurrences of $x$ in $\phi(x)$ were replaced with $y$, so $x$ is not free in $(\exists y)\phi(y)$. Now the problem is to show that the hypothesis $(\forall x)[\phi(x)\to (\exists y)\phi(y)]$ can be deduced, because then the conclusion $(\exists x)\phi(x) \to (\exists y)\phi(y)$ follows immediately by modus ponens.

To prove $(\forall x)[\phi(x)\to (\exists y)\phi(y)]$, first, use rule $L_{13}$ to obtain $\phi(x) \to (\exists y)\phi(y)$. This is a correct instance of $L_{13}$ because $y$ is admissible for $x$. Now use the generalization rule from page 6 to obtain $(\forall x)[\phi(x)\to (\exists y)\phi(y)]$.

Many proof systems have a separate rule of inference, called existential instantiation, which says that from $(\exists x)\phi(x)$ you can deduce $\phi(z)$ where $z$ is chosen as a new variable that has not yet appeared at all in the proof. In such a system, the deduction would go as follows, in symbolic form: $$(\exists x)\phi(x) \Longrightarrow \phi(z) \Longrightarrow (\exists y)\phi(y)$$ where the second $\Longrightarrow$ uses rule $L_{13}$, which works because $z$ was chosen in such a way to guarantee it was admissible for $x$.

The proof system adopted by this author does not directly admit this rule, but it is straightforward to make it work by Skolemization: add a new constant symbol $z_\phi$ to your language and add a logical axiom $(\forall x)[\phi(x) \to \phi(z_\phi)]$. Thus $z_\phi$ will be an element such that if any element satisfies $\phi$ then $z_\phi$ does. This axiom does not affect the consistency of any theory to which it is added, because any structure for the original theory can be expanded in such a way that the new logical axiom is true, and any structure in which the enlarged system holds automatically satisfies the original system, just by ignoring $z_\phi$. Therefore, using this and the completeness theorems for the original and expanded systems, a sentence in the original language is provable in the original system if and only if it is provable in the expanded system.

Now existential instantiation is an immediate consequence of $L_{15}$ and the new axiom for $z_\phi$ described in the previous paragraph. As a historical note, Hilbert developed a very similar idea which goes by the name $\epsilon$ calculus. What I call $z_\phi$ woulc be called $(\epsilon x)\phi(x)$ in that system.

The way that I look at the proof I described above in the original system is that it is a simulation of existential instantiation that just avoids directly using the rule for $z_\phi$ or the $\epsilon$ operator. The cost of avoiding them is that the other axioms have to be used in less obvious ways. Informally, $$(\forall a)[\phi(a) \to \psi] \to [(\exists x) \phi(x) \to \psi]$$ says that if we can prove $\phi(a) \to \psi$ for a suitable variable $a$, then we could have proved $(\exists x)\phi(x) \to \psi$. So in other words if we want to prove the latter it is enough to pick a suitable $a$ and prove the former. This is analogous to what the existential instantiation rule says: given $(\exists x)\phi(x)$ we should try working with $\phi(a)$ instead.

-
In the 7th paragraph, I should choose $z$ to be admissible for $x$ and $y$. When I edit the answer again, I will make this addition. – Carl Mummert Feb 9 '12 at 20:18
Thank you for this excellent, clear answer! – Rudy the Reindeer Feb 13 '12 at 6:57