Proving a bi-conditional predicate calculus formulae

Question

Prove the following:

∀x(C → D(x)) ↔ (C →∀xD(x))

I am looking at the axioms I can use under hilberts deductive system as well as the Generalization rule but I can't find an axiom that supports the biconditional connective. any help?

Answer 1

We have to prove that, if $x$ does not occur free in $C$, then

$\vdash (C → ∀xD(x)) ↔ ∀x(C → D(x))$.

---

---

A) To prove :

$\vdash (C → ∀xD(x)) → ∀x(C → D(x))$.

1) $C → ∀xD(x)$ --- assumed

2) $C$ --- assumed

3) $∀xD(x)$ --- from 1) and 2) by modus ponens

4) $D(x)$ --- from 3) and Axiom.1 : $∀x \alpha → \alpha _t^x$, by mp

5) $C → D(x)$ --- from 2) and 4) by Deduction Th

6) $∀x(C → D(x))$ --- from 5) by Generalization Th : $x$ is not free in assumption 1)

7) $(C → ∀xD(x)) \rightarrow ∀x(C → D(x))$ --- from 1) and 6) by Deduction Th

---

B) To prove :

$\vdash ∀x(C → D(x)) → (C → ∀xD(x))$.

1) $∀x(C → D(x))$ --- assumed

2) $C$ --- assumed

3) $C → D(x)$ --- from 1) and Axiom.1 by mp

4) $D(x)$ --- from 2) and 3) by mp

5) $∀x D(x)$ --- from 4) by Generalization Th : $x$ is not free in assumptions 1) and 2)

6) $C → ∀x D(x)$ --- from 2) and 5) by Deduction Th

7) $∀x(C → D(x)) → (C → ∀x D(x))$ --- from 1) and 6) by Deduction Th

---

The theorem follows from A) and B) by tautological implication :

$\alpha \rightarrow \beta, \beta \rightarrow \alpha \vDash \alpha \leftrightarrow \beta$