The standard deduction theorem or introduction rule for implication, for classical logic is also valid/or intuitiouistic logic, but just as with predicate logic, other rules of inference have to be restricted if the theorem is ~o ho14 for weaker impli. cational logics.
In this paper we look in 4etail. at special cases of the Gen~zen rule for ~ and show that various subsets of these in effect constitute deduction theorems determining all the theorems o~ many well known as well as no~ well known impliea~ional logics. In parti~ cular systems of rules are given which are equivalent to the relevance logics E_.,R_~, T, P-W and P-W-I.
Several weak implicational logics were examined by :~r in [8], some of these were represented in terms of n set of unary rules of inference and others by means cf constrhetlcnS which could, as was shown in [2], be represented in terms of restrictions of the Gentzen rules. ~r constructions nnd the rules of [2] in fact provided deduction theorems for these systems. Here using some extensions of these rules we look at n l~rge number of further systems.
The
Rules. ule 2~e B .Rule C~ t~e D~ t~ule Ek~ ~ule G~ The rules of [2], slightly gener~lised, ~re as follows.