# Several I-Rules

Where a logical constant (such as ∨) is introduced by several alternative ^{[1]} rules, one can formulate an appropriate GE-rule as having several minor14 premisses, one for each of the I-rules, giving a case analysis. This is very familiar from the case of ∨and the usual ∨*E* rule:

[ *A*. ]

. [*B*. ]

.

__ __ __A____ ____∨____ ____B C C____ __

*C*

so an appropriate generalisation for *n* ≥ 0 alternative I-rules is to ensure that “the GE-rule” has *n* minor premisses. This works well for ⊥, with no I-rules: the ⊥*E* -rule,

as in [9, 24], has no minor premises^{[2]}.

# I-Rule Has Several Premisses

Now there are two possibilities following the general idea that the conclusion of a GE-rule is arbitrary. Let us consider the intuitionistic constant ∧ (with its only I-rule

having two premisses) as an example. The first possibility is as illustrated earlier: the rule

[ *A,*. *B*]

.

__ __ __A____ ____∧____ ____B C____ __

.

The second is to have two GE-rules:

[ *A*. ]

.

__ __ __A__ __B C __

*C* ∧*GE*1 [*B*. ]

.

__ __ __A__ __B C __

*C* ∧*GE*2

and it is routine to show that the ordinary GE-rule for ∧ is derivable in a system

including these two rules, and vice-versa. Tradition goes for the first possibility;

examples below show however that this doesn't always work and that the second may be required.

# Premiss of I-Rule Discharges Some Assumptions

Natural deduction's main feature is that assumptions can be discharged, as illustrated by the I-rule for ⊃ and the E-rule for ∨. This raises difficulties for the construction of

the appropriate GE-rules: Prawitz [26] got it wrong (corrected in [27]), SchroederHeister [30] gave an answer in the form of a system of rules of higher level, allowing discharge not just of assumptions but of rules (which may themselves discharge

…)—but, although much cited, use of this system seems to be modest. As already discussed, an alternative was mentioned (disparagingly) in [3] and (independently)

adopted more widely by others [13, 36, 39], the “flattened” GE-rule for ⊃ being

[*B*. ]

.

__ __ __A__ __B A C __

*C* ⊃ *GE*

Let us now consider the position where two premisses discharge an assumption (just one each is enough): consider the logical constant ≡ with one I-rule, namely

[ *A*. ]

. [*B*. ]

.

__ ____B A __

*A* ≡ *B* ≡ *I*

According to our methodology, we have two possibilities for the GE-rule; first, have the minor premiss of the rule with two assumptions *B, A* being discharged and some device to ensure that there are other premisses with *A* and *B* as conclusions. There seems to be no way of doing this coherently, i.e. with *A* somehow tied to the discharge of *B* and vice-versa. The alternative is to have *two* GE-rules, along the lines discussed

above for ∧, and these are clearly

[*B*. ]

.

__ __ __A__ __B A C __

*C* ≡ *E*1 [ *A*. ]

.

__ __ __A__ __B B C __

*C* ≡ *E*2

by means of which it is clear that, from the assumption of *A* ≡ *B*, one can construct a proof of *A* ≡ *B* using the introduction rule as the last step, implying the “local

completeness” of this set of rules in a sense explored by Pfenning and Davies [22]:

*A* ≡ *B* [ *A*]2 [*B*. ]1

.

*B A* ≡ *B* [*B*]4 [ *A*. ]3

.

*A*

*B* ≡ *E*1, 1 *A* ≡ *E*2, 3

*A* ≡ *B* ≡ *I,* 2, 4

We are thus committed in general to the use of the second rather than the first possibility of GE-rules—the use of two such rules rather than one—when there are two premisses in an I-rule.