Derive the following theorems of first-order predicate calculus in the deductive system $K$.

Question

I am being asked to deduce the following theorems:

For $x_i$ not occuring free in $A$:

• $\vdash(\exists x_i(A\rightarrow B)\rightarrow(A\rightarrow\exists x_i B)),$
• $\vdash ((A\rightarrow\exists x_i B)\rightarrow(\exists x_i(A\rightarrow B)).$

If the only variables occurring free in $\phi$ are $x_i$ and $x_j$ ($i\neq j$):

• $\vdash (\forall x_i\lnot\phi \rightarrow\lnot\forall x_i\phi),$
• $\vdash (\exists x_i\forall x_j\phi \rightarrow\forall x_j\exists x_i\phi).$

Here, the deductive system is $K$, a Hilbert-style system for the first-order language $\mathcal{L}$ with connectives $\lnot, \rightarrow$, with the seven axioms and rules for modus ponens, generalization, and thinning. How do I prove the above statements?

EDIT: Here are the axioms/rules.

1. $(\alpha\rightarrow(\beta\rightarrow\alpha)))$
2. $((\alpha\rightarrow(\beta\rightarrow\gamma))\rightarrow((\alpha\rightarrow\beta)\rightarrow(\alpha\rightarrow\gamma)))$
3. $((\lnot\beta\rightarrow\lnot\alpha)\rightarrow(\alpha\rightarrow\beta))$
4. $(\forall x_i\alpha\rightarrow\alpha[t/x_i])$ where $t$ is free for $x_i$ in $\alpha$
5. $(\forall x_i(\alpha\rightarrow\beta)\rightarrow(\alpha\rightarrow\forall x_i\beta))$, provided that $x_i\notin\text{Free}(\alpha)$
6. $\forall x_i \ x_i\dot{=}x_i$
7. $(x_i\dot{=}x_j\rightarrow(\phi\rightarrow\phi'))$, where $\phi$ is atomic and $\phi'$ is obtained from $\phi$ by replacing some occurrences of $x_i$ in $\phi$ by $x_j$
8. Modus Ponens: From $\alpha$ and $(\alpha\rightarrow\beta)$ infer $\beta$
9. Generalisation: From $\alpha$ infer $\forall x_i\alpha$
10. Thinning: If $\Gamma\vdash\phi$ and $\Gamma\subseteq\Gamma'$ then $\Gamma'\vdash\phi$

Answer 1

Here is a proof for the third theorem: $\forall x \neg \phi(x) \rightarrow \neg \forall x \phi(x)$:

1. $\forall x \neg \phi(x) \rightarrow \neg \phi(a)$ Axiom 4

2. $\forall x \phi(x) \rightarrow \phi(a)$ Axiom 4

3. $\neg \phi(a) \rightarrow \neg \forall x \phi(x)$ Contraposition 2

4. $\forall x \neg \phi(x) \rightarrow \neg \forall x \phi(x)$ Hypothetical Syllogism 1,3

I used Contraposition and Hypothetical Syllogism as propositional logic inference principles rather than theorems. I assume that is ok, and if not, you can always add them as theorems:

$(A \rightarrow B) \rightarrow (\neg B \rightarrow \neg A)$ Contraposition

$(A \rightarrow B) \rightarrow ((B \rightarrow C) \rightarrow (A \rightarrow C))$ Hypothetical Syllogism

So then the above proof would be:

1. $\forall x \neg \phi(x) \rightarrow \neg \phi(a)$ Axiom 4

2. $\forall x \phi(x) \rightarrow \phi(a)$ Axiom 4

3. $(\forall x \phi(x) \rightarrow \phi(a)) \rightarrow (\neg \phi(a) \rightarrow \neg \forall x \phi(x))$ Contraposition

4. $\neg \phi(a) \rightarrow \neg \forall x \phi(x)$ MP 2,3

5. $(\forall x \neg \phi(x) \rightarrow \neg \phi(a)) \rightarrow ((\neg \phi(a) \rightarrow \neg \forall x \phi(x)) \rightarrow (\forall x \neg \phi(x) \rightarrow \neg \forall x \phi(x)))$ Hypothetical Syllogism

6. $(\neg \phi(a) \rightarrow \neg \forall x \phi(x)) \rightarrow (\forall x \neg \phi(x) \rightarrow \neg \forall x \phi(x))$ MP 1,5

7. $\forall x \neg \phi(x) \rightarrow \neg \forall x \phi(x)$ MP 4,6

... but you see what a pain that is, so to keep your proofs manageable and readable I would assume that you already have established those propositional theorems as derived inference principles and stick to the initial proof.

Proofs by contradiction will be useful for some of the other proofs. I will assume that this is defined as follows:

If $\Gamma_1 \cup \{A\} \vdash B$ and $\Gamma_2 \cup \{A\} \vdash \neg B$ then $\Gamma_1 \cup \Gamma_2 \vdash \neg A$

OK, let's do the proof for $\exists x (A \rightarrow B(x)) \rightarrow (A \rightarrow \exists x B(x))$. I'll guide you through the thought process so that hopefully you can do the last two proofs yourself once you get the hang of this:

OK, so to prove $\exists x (A \rightarrow B(x)) \rightarrow (A \rightarrow \exists x B(x))$ we'll show that $\exists x (A \rightarrow B(x)) \vdash (A \rightarrow \exists x B(x))$ so that we can then get the desired theorem using the Deduction Theorem (which says that if $\Gamma \cup \phi \vdash \psi$ then $\Gamma \vdash \phi \rightarrow \psi$).

In fact, since our new goal is $A \rightarrow \exists x B(x)$, which is another conditional, we'll anticipate using the Deduction Theorem here as well, i.e. we're going to show $\{ \exists x (A \rightarrow B(x)), A\}\vdash \exists x B(x)$.

Realizing $\exists x \phi(x)$ is shorthand for $\neg \forall x \neg \phi(x)$, our goal becomes $\{ \neg \forall x \neg (A \rightarrow B(x)), A\}\vdash \neg \forall x \neg B(x)$.

Since our conclusion $\neg \forall x \neg B(x)$ is a negation, we'll set this up as a proof by contradiction, i.e. we want to show that we can get some statement and its negation by starting out with $\{ \neg \forall x \neg (A \rightarrow B(x)), A, \forall x \neg B(x)\}$. And, since we already one negation in this set of statements ($\neg \forall x \neg (A \rightarrow B(x))$), let's try and get the positive of that one, i.e. let's see if we can show: $\{ A, \forall x \neg B(x)\} \vdash \forall x \neg (A \rightarrow B(x))$.

OK, since that new goal is a universal, we'll anticipate the Generalization rule, so we have to show $\{ A, \forall x \neg B(x)\} \vdash \neg (A \rightarrow B(a))$.

Now we have a negation as our goal again, so let's anticipate Proof by Contradiction and show that $\{ A, \forall x \neg B(x), A \rightarrow B(a)\}$ leads to a contradiction.

.. and that is quite straightforward:

1. $\forall x \neg B(x)$ Premise

2. $A$ Premise

3. $A \rightarrow B(a)$ Premise

4. $B(a)$ MP 2,3

5. $\forall x \neg B(x) \rightarrow \neg B(a)$ Axiom 4

6. $\neg B(a)$ MP 1,5

OK, so let's go back in the reverse order in which we set our goals. First, we just showed that:

1. $\{A, A \rightarrow B(a)\} \vdash B(a)$

2. $\{ \forall x \neg B(x)\} \vdash \neg B(a)$

Hence:

3. $\{ \forall x \neg B(x),A\} \vdash \neg (A \rightarrow B(a))$ Proof by Contradiction 1,2

So:

4. $\{ \forall x \neg B(x),A\} \vdash \forall x \neg (A \rightarrow B(x))$ Generalization 3

And since:

5. $\{ \neg \forall x \neg (A \rightarrow B(x)) \} \vdash \neg \forall x \neg (A \rightarrow B(x))$ (trivially true!)

We get:

6. $\{ \neg \forall x \neg (A \rightarrow B(x)), A\}\vdash \neg \forall x \neg B(x)$ Proof by Contradiction 4,5

By definition of $\exists$ this is the same as:

7. $\{ \exists x (A \rightarrow B(x)), A\}\vdash \exists x B(x)$ Definition $\exists$ 6

So by the Deduction Theorem:

8. $\exists x (A \rightarrow B(x)) \vdash (A \rightarrow \exists x B(x))$ Deduction Theorem 7

And applying the Deduction Theorem once more:

9. $\vdash \exists x (A \rightarrow B(x)) \rightarrow (A \rightarrow \exists x B(x))$ Deduction Theorem 8

So, yes, there is a derivation of $\exists x (A \rightarrow B(x)) \rightarrow (A \rightarrow \exists x B(x))$, though notice I didn't write it out. Rather, I gave a proof that there is such a derivation; it is a kind of metaproof. But, I assume this will be perfectly acceptable since, as I already pointed out, the actual derivation itself can be massive.