Are there inference rules for introducing and elimination implication `->` in the antecedent (the part on the left of `|-`)?

Question

Deductive theorem says that P, Q |- S, if and only if P |- (Q->S). I found that the deductive theorem is inference rules for introducing and elimination implication -> in the succedent (the part on the right of |-).

Are there inference rules for introducing and elimination implication -> in the antecedent (the part on the left of |-)?

• If ... |- ..., where ... on the left hand side doesn't include implication, then ..., (Q->S) |- ....

• If ..., (Q->S) |- ..., then ... |- ..., where ... on the left hand side doesn't include implication.

Thanks.

Answer 1

There is a very natural way of doing so assuming the classical sequent calculus. We have (L ->):

Given

Γ⊢Δ,A

and

B,Γ⊢Δ

deduce

A→B,Γ⊢Δ

The classical sequent Gamma|- Delta can be interpreted as "All of Gamma make at least one of Delta true". Under this interpretation we have the following justification of this rule: Given all of Gamma, we have at least one of Delta or A is true. if one of Delta, we are done. If A, use A-> B to conclude that B is true, and use the second assumption to conclude that one of Delta is true. There is however no "elimination" rule for the left hand side since we do not eliminate connectives in the sequent calclus (by design).

How does this look when we go back to a hilbert style calculi? Since |- typically is used as shorthand in the metalanguage to say there exists a proof, trivially we can derive rules with say, weakening or MP. But we would not call them intro or elimination rules.