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

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.


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").

  • $\begingroup$ Plainly, yes. Upvoted. $\endgroup$ – rewritten Dec 6 '13 at 20:59

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.