Deduction Theorem - Interpretation In the book "A tour through mathematical logic" - by Robert S. Wolf, the deduction theorem is specified as follows:
If T $\cup$ {P} $\vdash$ Q, then T $\vdash$ (P $\to$ Q)
Where T is a first-order theory and P & Q are some formulae, in the language of this first-order theory. Then, is the following interpretation, of the deduction-theorem, correct?

If Q is derivable/provable from T $\cup$ {P}, then one can say that -
if P is derivable from T (i.e. P is a theorem of T) then Q is also
derivable from T.

Also, does this interpretation capture the essence of the deduction theorem?
PS: another question titled Deduction Theorem - Intuition, seems to focus primarily on the syntactic aspects of the theorem and predicate calculus in general - rather than on its semantics.
 A: 
is the following interpretation, of the deduction-theorem, correct?

No. What you write is

If $T \cup \{P\} \vdash Q$, then if $T \vdash P$, then $T \vdash Q$.

This is the same as saying

(1) If $T \cup \{P\} \vdash Q$, then $T \nvdash P$ or $T \vdash Q$.

But this is not equivalent to

(2) If $T \cup \{P\} \vdash Q$, then $T \vdash P \to Q$.

It may be the case that $P$ is not provable, but $P \to Q$ isn't either. Then "$T \nvdash P$ or $T \vdash Q$" holds, but "$T \vdash P \to Q$" does not. So (1) $\not \Rightarrow$ (2).
This is what is meant in the comments by "trivialization": "if $T \vdash P$ then $T \vdash Q$" (= what you wrote) becomes trivially true if $T \nvdash P$, i.e. if $P$ is unprovable. But "$T \vdash P \to Q$" (= what the deduction theorem states) does not: Just because we can't prove $P$ doesn't mean we can prove $P\to Q$ -- as you observed. Hence why "$T \vdash P \to Q$" is a stronger claim that "If $T \vdash P$ then $T \vdash Q$".

The essence of the deduction theorem is that you can "flip-flop" between having a theorem dependent on an open assumption and proving a conditional statement:
If there is a proof of $Q$ which is still dependent on the assumption $P$, then there will be a proof in the theory of the statement $P \to Q$. This is the immediate effect of the conditional proof technique (see p. 14).
And for the converse direction of the deduction theorem, if you can prove $P \to Q$, then you will be able to prove $Q$ under the assumption that $P$. This is a consequence of the modus ponens rule of inference (see p. 13).
The two directions combined, the deduction theorem simply justifies what we mean by having a proof of "$\to$".

You are completely right in pointing out that the central notion of a formal system is that of proof rather than truth. But do keep in mind that we're normally interested in designing a "useful" proof system that is "in line" with the notion of truth: A statement should be provable in a theory exactly when it is true in all models of the theory. After all, the point of a proof system is to have a mechanical device to rigorously prove statements we consider true. So while the notion of a proof of $\to$ is formulated in terms of rules of inference, the way these rules are used does reflect the truth table for $\to$: A proof system should be (and as for the proof system presented in Wolf's book, is) sound w.r.t. the semantics: What can be proved is true (according to the truth table definitions) in all structures; the system (hopefully) doesn't prove random nonesense.
