The introduction rule for implication

Question

The introduction rule for implication says that you can prove a statement of the form $P \implies Q$ by assuming $P$ and deducing $Q$. (Btw. I don't know why it's called an introduction rule - you don't introduce the implication, you eliminate it.)

My question is: can the introduction rule for implication be proven? If yes, how?

Answer 1

Named "introduction rule for implication", it's just what it says, it's the syntactical rule for which we introduce the symbol $\implies$ to signify that actually assuming $P$ one can deduce $Q$.

If you instead name it "deduction theorem" (DT, it's actually a metatheorem) you can follow the proof in wikipedia, on how to convert a proof using DT to a proof that doesn't use DT, provided your logic system has other axioms, of course). Thus, you see that DT is no necessary for the whole deduction process, so it is a theorem, and not an axiom.

Answer 2

When are you entitled to assert a conditional $P \to Q$? Precisely when, given $P$ as an assumption, you are in a position to assert $Q$. The natural deduction rule "conditional proof" or "$\to$-introduction" encapsulates that fundamental assumption about the meaning of the conditional. It's an introduction rule because it tells you that when you can argue from $A$ to $C$ you are entitled to discharge the assumption and deduce a proposition $A \to C$ whose main connective is the conditional, thereby introducing a conditional where there wasn't one before.

And the "modus ponens" or "$\to$-elimination" rule is in harmony with introduction rule. For if someone asserts $P \to Q$ they represent themselves as being in a position, given the assumption $P$ to infer $Q$. So if you tell them the assumption $P$ is indeed true, they are committed to $Q$.

You need, contra @rewritten, to clearly distinguish the introduction rule proper (which belongs to a collection of introduction and elimination rules constituting a natural deduction system, for arguing inside a deductive system) from the deduction theorem (which is a meta-theorem which looks at an axiomatic system from outside and says "if there is such-and-such axiomatic proof, then there will also be an axiomatic proof related so-and-so").