Is the Deduction Theorem a metametatheorem or a metatheorem?

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.

• See Deduction theorem : "In mathematical logic, the deduction theorem is a metatheorem of propositional and first-order logic. It is a formalization of the common proof technique in which an implication A → B is proved by assuming A and then deriving B from this assumption conjoined with known results. The deduction theorem explains why proofs of conditional sentences in mathematics are logically correct." – Mauro ALLEGRANZA Jun 17 '18 at 16:22
• Compare with Sequent calculus where $\vdash$ is part of the language. – Mauro ALLEGRANZA Jun 17 '18 at 16:32
• We have a mathematical object : propositional calculus (axioms, rules, derivations - compare with real numbers)) and we have a theory studying the properties of that "object" : propositional logic (compare with real analysis). Unfortunately, we are used to call the end-formula of a derivation in the calculus : a theorem. Thus, the result proved by usually math reasoning in the theory (prop logic) about the math object (prop calculus) are called : meta-theorems. End of the story. – Mauro ALLEGRANZA Jun 18 '18 at 6:03
• Prop calculus is a formal system based on a formal language i.e. a set of strings of symbols. Sets a mathematical objects. – Mauro ALLEGRANZA Jun 18 '18 at 7:04
• Mathematical logic (or any mathematical analysis of formal languages) cannot start without some way of talking about the sequences of symbols that constitute the statements in the formal language. – Rob Arthan Jun 18 '18 at 21:13

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.

• It is true that " $\Delta \vdash A$ means "the formula $A$ is derivable from the set of formulas $\Delta$". But I took the Deduction theorem to be stating a property about $\vdash$ in the following rough sense: one can 'switch' $P$ from the LHS of $\vdash$ to the RHS of $\vdash$. This seemed to me to require the existence of the metametalanguage. – user 170039 Jun 18 '18 at 3:20
• @user170039 As Rob says, there's no talk about $\vdash$ in the statement of it. So, I don't see how the statement of The Deduction Theorem, when a theorem, ends up in the metametalanguage. Now, the proof of the Deduction Theorem, that seems like it usually happens in the metametalanguage. – Doug Spoonwood Jun 18 '18 at 4:10
• @DougSpoonwood: From the point of view provided in the answer, I agree that the statement of DT doesn't talk about $\vdash$ but just uses it. However, I was trying to read the DT as a theorem in the following manner: $${\color{red}{\vdash}}\Delta\cup\{P\}\vdash Q\implies \Delta\vdash P\to Q$$ where ${\color{red}{\vdash}}$ was assumed to be signify "the formula $\Delta\cup\{P\}\vdash Q\implies \Delta\vdash P\to Q$ is a theorem", in an analogous way of reading $\vdash P\to P$, say. – user 170039 Jun 18 '18 at 4:56

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.

• In any case, I was only claiming that DT in the context of my question was intended to be interpreted as I have done here. – user 170039 Jun 18 '18 at 13:43
• @user170039 Alright, what is the axiomatic and rule basis for your use of the red $\vdash$? If you don't have such, I'm not sure that (((Δ∪{P})⊢Q)⟹(Δ⊢(P→Q))) is a theorem, even if semantically it makes sense. – Doug Spoonwood Jun 18 '18 at 14:01
• If you don't mind then can we continue this discussion in this room? – user 170039 Jun 18 '18 at 14:20