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.