Is the Deduction Theorem a metametatheorem or a metatheorem?

Question

I am talking about a Hilbert style system for Propositional Calculus. The only axioms and rule of inference that I can use are,

$\color{crimson}{\text{Axiom 1.}}\ P\to (Q\to P)$

$\color{crimson}{\text{Axiom 2.}}\ (S\to (P\to Q))\to((S\to P)\to (S\to Q))$

$\color{crimson}{\text{Axiom 3.}}\ (\neg Q\to\neg P)\to(P\to Q)$

$\color{crimson}{\text{Rule of Inference.}}$ Modus Ponens.

My main question is regarding the Deduction Theorem for this system. Before stating my question, let me first state the Deduction Theorem for the sake of completeness of this post.

Deduction Theorem. Let $\Delta$ be a set of formulas. If $\Delta\cup\{S\}\vdash T$ then $\Delta\vdash S\to T$.

Here symbols have usual meaning (if clarification is needed then please let me know via comment(s)).

The main question I have is,

Is the Deduction Theorem a meta-theorem or a meta-meta theorem?

Due to the occurrence of $\vdash$ in the statement of Deduction Theorem and since $\vdash$ is not in the alphabet of Propositional Calculus (for example, see here) the statement for Deduction Theorem can't be a statement of the object language. In logic text books (at least the ones I have seen) the theorem is characterized as a metatheorem.

However, from the statement of the theorem it seems to me that the theorem is talking (roughly) about a property of $\vdash$. Since the theorem talks about a property of $\vdash$, I thought that the Deduction theorem is probably a metametatheorem. My questions are,

1. Is the Deduction Theorem a metametatheorem?
2. In which language is the proof of the Deduction Theorem being carried out (i.e., in the metalanguage or in the metametalanguage)?
3. Is it possible to state an prove the deduction theorem in a language which is not a Natural Language (like English)?

---

Edit: See this comment for further clarification of the motivation for asking this question.

Answer 1

The symbol $\vdash$ is being used in your statement of the deduction as a shorthand notation; $\Delta \vdash A$ means "the formula $A$ is derivable from the set of formulas $\Delta$". The statement does not talk about $\vdash$, it just uses it. So the deduction theorem is a metatheorem rather than a metametathorem and its proof is (in typical textbooks) carried out in a metalanguage comprising a mixture of natural language and symbols like $\vdash$, $\cup$, $\{$ and $\}$ etc.

It would be possible to state and prove the deduction theorem in a formal language like the language of set theory or in the language of a typical automated proof assistant.

Answer 2

Your statement of The Deduction Theorem is a bit imprecise. It doesn't actually say, parenthesizing the implication as needed, that "Let Δ be a set of formulas. If Δ∪{S}⊢T then Δ⊢(S→T)." If it did, then for all uses of $\vdash$ we would have that. But, there exist some logical systems where that doesn't hold, such as Lukasiewicz's three-valued logic. It sometimes isn't even stated in classical logic, such as in Frege's work or gets relegated to an appendix such as in Arthur Prior's book Formal Logic. The Deduction Theorem as you used it says:

"Let Δ be a set of formulas. If Δ∪{S} ⊢$_{(1, 2, 3)}$ T then Δ ⊢$_{(1, 2, 3)}$ (S→T)."

So, I don't think that The Deduction Theorem talks about a property of $\vdash$. It talks about a property of the deductive system at hand. The "if-then" statement is the property. That implies The Deduction Theorem as a meta-theorem of that deductive system.