# The introduction rule for implication

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?

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$.
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$.