While making a list of the rules of inference for my math students, I came across this list on Wikipedia:

enter image description here

I noticed a pattern: for every introduction rule, there seems to be an elimination rule, and vice versa. For example, corresponding to conjunction introduction is conjunction elimination, and corresponding to disjunction introduction is disjunction elimination.

I wondered if Modus Ponens, which asserts ((P⇒Q)∧P)⇒Q, followed this pattern. I noticed its Wikipedia article referred to Modus Ponens as "implication elimination", so I wondered if there existed another tautology or theorem known as implication introduction. Although no page exists on Wikipedia for "implication introduction", a Google search returned this statement, formulated in sequent notation as

(P ⊢ Q) ⊢ (P ⇒ Q)

It's a curious statement, as once written in tautological form, it seems to say that (P⇒Q)⇒(P⇒Q).

Have I correctly translated the statement from sequent notation to tautological form? If so, the resulting theorem, (P⇒Q)⇒(P⇒Q), seems quite trivial to me. Certainly it is true; just like implication elimination can be proved using a truth table to show ((P⇒Q)∧P)⇒Q is a tautology, you can also verify using a truth table that (P⇒Q)⇒(P⇒Q) is a tautology. However I must be missing what makes this statement interesting, as it seems as trivial to me as saying A⇒A.

Perhaps I've mistranslated the statement from sequent notation to tautological form. The webpage mixes two different symbols for implication. The definition of "implication" ⇒ which I learned is the unique truth-functional connective characterized by its Boolean (or truth table) values. That is, ⇒ is the unique function that maps P and Q to (1,0,1,1):

enter image description here

Since this definition of ⇒ is unique, what would the other implication symbol mean as a truth-functional connective? Would it have a different truth table? And, when I translated the inference rule from sequent notation to tautological form, was it correct to replace all instances of ⊢ with ⇒?

Finally, I'm curious why implication introduction isn't listed with the other rules of inference in the Wikipedia table. Is there something fundamentally different about this result, perhaps its use of the turnstile implication, that makes this theorem of a fundamentally different sort than the others? Thanks for your thoughts!

  • See Natural Deduction for the source of the simmetrical formulation of introduction and elimination rules. Commented Feb 2, 2017 at 20:08
  • The introduction rule is from Γ, A ⊢ B to Γ ⊢ A→B, where ⊢ means "logically derives", see sequent calculus notation. If you want complete symmetry between introduction and elimination rules though then classical logic does not have it, symmetric sequent calculus gives intuitionistic logic.
    – Conifold
    Commented Feb 2, 2017 at 23:28
  • Thanks, @Conifold ! As a follow-up, does the turnstile symbol ⊢ here have the same meaning as the entailment symbol ⊨ or are they used differently? philosophy.stackexchange.com/questions/12816/… Commented Feb 3, 2017 at 0:56
  • They are often used interchangeably but when distinguished ⊨ is semantic ("truth table") consequence , and ⊢ is deductive (proof-theoretic) consequence. The difference depends on subtle issues about "true but unprovable" statements. In sequent calculus deductive consequence is more natural.
    – Conifold
    Commented Feb 3, 2017 at 1:47
  • An implication introduction in "tautological form" must be Q⇒(P⇒Q). Commented Feb 3, 2017 at 7:14

2 Answers 2


The two different symbols on the page you link to are indeed different. The first is the turnstile symbol Ⱶ which may be read as 'proves', while the arrow → is material implication. These are very different. Material implication is a symbol in the object language defined by the truth table that you give, i.e. T/F/T/T. Turnstile is a symbol in the metalanguage that can be read as P proves Q, or Q is a theorem on P.

The rule of conditional introduction can be understood as meaning that if Q is a theorem on P, then P → Q is a theorem. More generally, it might be written like this: if Γ is a set of propositions, then from Γ,P Ⱶ Q, one can deduce Γ Ⱶ P → Q. If Γ together with P proves Q, then Γ proves that P materially implies Q. This is called the deduction theorem.

In natural deduction, we can use the rule of conditional proof to the same effect. You may assume any P you like, proceed to prove Q from it, then discharge the assumption to introduce the material implication P → Q.

As to logical constants having corresponding introduction and elimination rules, this is no accident. In the Fitch system, the logical constants are specified by these rules. The idea of harmonious introduction and elimination rules was introduced by Gerhard Gentzen and taken up by various others. The idea is that the corresponding I and E rules should be 'inverses' of one another, in order to ensure that they don't have unruly consequences. In a famous paper back in 1960, Arthur Prior ("The Runabout Inference Ticket" Analysis 21: 38-9) showed that defining logical constants without restrictions could allow you to prove anything.

This inverse relationship between the I and E rules is called logical harmony. Michael Dummett argued that classical logic has no harmonious way of defining the rules for negation, while intuitionistic logic does, though this has been disputed. If you would like to follow up with some more information about logical harmony, these papers might be useful:

Steinberger, F. (2011) “What harmony could and could not be”. Australasian Journal of Philosophy 89: 617-639. Rumfitt, Ian (2016) “Against Harmony”. Forthcoming in Robert Hale, Crispin Wright, and Alexander Miller, eds., The Blackwell Companion to the Philosophy of Language, 2nd edition. Oxford: Blackwell.

I believe both papers can be found on philpapers.org.

  • Thanks very much for the explanation! So if I understand this (please correct me if I'm wrong), because the sequent "→I" (implication introduction) involves symbols (namely, the turnstile ⊢) from the meta language, therefore →I can't be formulated in terms of a theorem/tautology in the mathematical object language? Is that right? Commented Feb 3, 2017 at 0:59
  • And so it would seem like there is NO implication introduction result that's provable within the object language like all the other introduction/elimination results, correct? And therefore, we would say there's no "harmonious" way of defining I/E rules for implication, since →E is provable in the object language but →I isn't, is this correct? Commented Feb 3, 2017 at 0:59
  • The I and E rules for material implication are commonly taken to be harmonious, though I agree with you that the I rule is an oddity, because it refers to the meta-linguistic entailment operator, while other I rules do not. Having said that, harmony is arguably too strong a criterion to deal with Prior's runabout inference problem. All we need is that a logical constant behaves in such a way as to be conservative with respect to what it implies. The Ian Rumfitt paper I mentioned in the reply is good on this point.
    – Bumble
    Commented Feb 3, 2017 at 10:54

What might be thought of as implication introduction, →I, is sometimes called conditional proof or CP.

The basic strategy is to assume the antecedent and derive the consequent. Once the consequent is derived, the assumption can be discharged. Here's an example:

{1}      1.   (P ∨ Q) → R                 Prem.
{2}      2.   P                           Assum.
{2}      3.   P ∨ Q                       2 ∨I (rh)
{1,2}    4.   R                           1,3 MP
{1}      5.   P → R                       2,4 CP

The antecedent is assumed on line 2, and the consequent is derived on line 4. This meets the conditions for → Introduction or CP on line 5.

With this particular system of proof, dependency numbers are listed on the left. Wherever the number {2} appears, that means that the corresponding line number depends on the assumption made in line 2. Notice that once the implication is introduced, the dependency number for the assumption is discharged. You can see that the conclusion is based only on {1}, which is the premise.

The other symbol:

The Wikipedia article reads:

The modus ponens rule may be written in sequent notation:

P → Q, P ⊢ Q

where ⊢ is a metalogical symbol meaning that Q is a syntactic consequence of P → Q and P in some logical system;

The other symbol is a turnstile and functions in a way analogous to the implication symbol, but it belongs to a separate system of logic, or metalogic. The turnstile indicates that an indicated argument is sound, and since it functions like implication, all the premises of an argument along with the conclusion can be rewritten using normal logical notation to form a tautology.

As I mentioned in my comment, the relation expressed by((A & (A → B)) → B) is the principle governing both introduction and elimination, so the same truth table is valid for both.

  • Thanks very much for your answer. It does leave a couple of my questions still unanswered, though... For instance, how would one write this implication introduction as a theorem / tautology? Would the statement be formulated as (P⇒Q)⇒(P⇒Q)? I want to be able to prove the result; up until now I've been able to prove all the other rules of inference by truth table. Commented Feb 2, 2017 at 19:52
  • The relation expressed by the tautology (A & (A → B) → B) is the principle governing both introduction and elimination, so the same truth table is valid for both. I edited my answer to address your question about the other implication symbol, which is a turnstile and indicates the soundness of the argument in metalogic.
    – user3017
    Commented Feb 2, 2017 at 20:35

You must log in to answer this question.

Not the answer you're looking for? Browse other questions tagged .