0

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

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

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

Thanks.

0

0

Browse other questions tagged .