# Help me prove this principle with other Hilbert system principles

I have two choices:

1.to show that this principle is correct with other Hilbert system principles the first order $\forall x(A \to B(x)) \to (A \to \forall x B(x))$ (original screenshot)

OR 2. to show that this principle is independent of other of this system principles

I must not use the deduction theorem

($x$ is NOT free variable of $A$)

Thanks

• Welcome to Math.SE! I converted your screenshot to $\TeX$. Please do it yourself next time. Here is a tutorial. – Ayman Hourieh Jan 4 '14 at 11:25
• thanks if you can please help me solve it. – SRah Jan 4 '14 at 11:29

Usually, we would use the following deduction :

1) $\forall x (A \rightarrow Bx)$ --- Assumption

2) $\vdash \forall x (A \rightarrow Bx) \rightarrow (\forall x A \rightarrow \forall x Bx)$ --- Axiom Q6

3) $\forall x A \rightarrow \forall x Bx$ --- from 1&2 by MP

4) $\vdash A \rightarrow \forall x A$ --- Axiom Q7 ($x \notin Free(A)$)

5) $A \rightarrow \forall x Bx$ --- form 4&3 by TAUT

so : $\forall x (A \rightarrow Bx) \vdash ( A \rightarrow \forall x Bx )$

But we cannot add the final step to obtain :

$\vdash \forall x (A \rightarrow Bx) \rightarrow ( A \rightarrow \forall x Bx )$

without the Deduction Theorem.

In order to get the desired result without the DT we can "mimick" the steps used into the proof of DT, in order to transform the deduction of :

$( A \rightarrow \forall x Bx )$ from : $\forall x (A \rightarrow Bx)$

into a deduction of :

$\forall x (A \rightarrow Bx) \rightarrow ( A \rightarrow \forall x Bx )$

Enderton's textbook (A Mathematical Introduction to Logic : 2nd ed, 2001) use the same set of axioms (and only MP) ; so you can use the proof of DT at page 119.

I have tried to write it.

We need three Tautologies :

A) $[P \rightarrow (Q \rightarrow R)] \rightarrow [ P \rightarrow ( (S \rightarrow Q) \rightarrow (S \rightarrow R) ) ]$

B) $(P \rightarrow Q) \rightarrow [P \rightarrow (Q \rightarrow R)] \rightarrow (P \rightarrow R) ]$

C) $P \rightarrow (Q \rightarrow P)$

Now with the deduction :

1) $\vdash \forall x (A \rightarrow Bx) \rightarrow (\forall x A \rightarrow \forall x Bx)$ --- Axiom Q6

2) $\vdash A \rightarrow \forall x A$ --- Axiom Q7 ($x \notin Free(A)$)

3) $\vdash (A \rightarrow \forall x A) \rightarrow [\forall x (A \rightarrow Bx) \rightarrow (A \rightarrow \forall x A) ]$ --- TAUT C

4) $\vdash \forall x (A \rightarrow Bx) \rightarrow (A \rightarrow \forall x A)$ --- from 2 & 3 by MP

5) $\vdash \forall x (A \rightarrow Bx) \rightarrow [(A \rightarrow \forall xA) \rightarrow (A \rightarrow \forall x Bx) ]$ --- from TAUT A & 1 by MP

6) $\vdash \forall x (A \rightarrow Bx) \rightarrow ( A \rightarrow \forall x Bx )$ --- from TAUT B & 4 & 5 by MP.