No deduction, no arrow

Explain this idea: "If you've got no deduction theorem, then you might as well be implication-free."

Here’s the gist in plain terms:

• The deduction theorem is the bridge between reasoning with assumptions and using → inside formulas. It says: if from Γ together with A you can prove B (Γ, A ⊢ B), then you can prove the implication inside the system (Γ ⊢ A → B). In other words, “assuming A, B follows” can be internalized as the single formula A → B.

• So, in logics where a good deduction theorem holds, the connective → earns its keep: it represents the underlying consequence relation ⊢. Proof steps that temporarily assume A can be packaged up as the statement A → B.

• If your system doesn’t have a (usable) deduction theorem, → no longer tracks provability from assumptions. You might still have a symbol called “→”, but it doesn’t internalize your consequence relation. Then implication loses its chief proof-theoretic role; it’s just another connective with some axioms, not the stand-in for “from A, infer B”.

That’s what the quip means by: “no deduction theorem ⇒ might as well be implication-free.” If → can’t encode entailment, you could drop it and work directly with the turnstile (sequents, Γ ⊢ B), or redesign your system so that whatever conditional you keep really does satisfy a deduction-style rule (e.g., by giving → an introduction/elimination rule or ensuring it’s the right adjoint to ∧ in the algebraic/structural sense).

A slightly more technical snapshot

• With DT: A → B is the internalization of entailment: A ⊢ B ⇔ ⊢ A → B (relative to Γ if present).
• Without DT: there’s no such equivalence, so → doesn’t mirror ⊢. Proof theory then usually takes ⊢ (or sequents) as primitive, or replaces → with a conditional that restores the adjunction: Γ, A ⊢ B iff Γ ⊢ A → B.

So the slogan is a design principle: if your implication can’t internalize consequence (no deduction theorem), using it is mostly decorative; organize the system around ⊢ instead, or fix → so it earns its place.