Confusion concerning a theorem *about* propositional logic 
The first theorem is called a “derived rule” (of inference) because it involves a hypothesis, $T$, which can be any axiom or previous theorem. Such a derived rule of inference is a theorem about rather than in the implicational calculus, but it provides a recipe to shorten subsequent proofs. Specifically, theorem 1.12 shows a derivation of $S\implies T$ from $T$ and axiom $P1$...
1.12 Theorem (derived rule): For each well-formed formula $S$ and for each theorem $T$, the implication $S\implies T$ is a theorem: $P1,\,T\vdash S\implies T$.
proof:
\begin{align*}
&\vdash T\text{ hypothesis}\\
&\vdash T\implies(S\implies T)\text{ axiom P1}\\
&\vdash S\implies T\text{ detachment}
\end{align*}

i am not sure I understand how this is a theorem about the implicational calculus, and what that would mean exactly. aren't theorems things that we derive using the implicational calculus itself (so how can they be about it)?
as per my understanding, a rule of inference tells us that when we have theorems of a specific form we can infer another theorem, which we would call a conclusion. comparing this derived rule of inference to usual ones, it seems to me that the difference is that we now have a well formed formula that we don't suppose is a theorem in the equation.
would this be the reason why the stated theorem is about, not in, the implicational calculus? if yes, why would this make the theorem about the calculus? especially since, as i said bove, we are using an axiom and a rule of inference of the calculus to prove it.
 A: "as per my understanding, a rule of inference tells us that when we have theorems of a specific form we can infer another theorem, which we would call a conclusion. comparing this derived rule of inference to usual ones, it seems to me that the difference is that we now have a well formed formula that we don't suppose is a theorem in the equation."
The hypothesis and the sequent (right hand side of the $\vdash$) both get used to refer to well-formed formulas which are not supposed as theorems, usually at least.  Note, I don't think 'S⟹T' is a well-formed formula of your calculus, I would guess it's '(S⟹T)', though it could also be '(S)⟹(T)' similar to the pattern in Kleene (Introduction to Metamathematics) or Stoll's book (Set Theory and Logic).
However, if something is true for well-formed formulas which may not be theorems, then it is also true for theorems.  Falsity implies truth, and truth implies true.  So, the meta-theorem does tell you something about theorems in the calculus, insofar it can be said to 'tell' anything.  Here it implies that for any theorem T in the calculus, (S⟹T) is also true, no matter whether S is a theorem or not.
To perhaps try to put that into your notation scheme, it might look something like this:
{ P1 , ($\vdash$T) } ⊢ [ S ⟹ ($\vdash$T) ].
Also, if anyone were to ask us "how many theorems are there in propositional calculus?"  We could easily and conclusively respond that there is no possible limit that we can write.  Even if infinity isn't a valid concept, anytime someone presented us with a theorem, we could respond that well 'S' could be a theorem too. But, 'S' is completely arbitrary and not fixed by any of the premises.  So, there's always a way to produce more theorems even if infinity does not exist... unless we run out of physical material to do so.
I can't say this answers all of your questions, but perhaps it's at least something.
