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!