Implication Introduction formulated as a theorem?

Question

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

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):

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!

Answer 1

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.

Answer 2

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.