 Home Philosophy Advances in Proof-Theoretic Semantics

# Several I-Rules

Where a logical constant (such as ∨) is introduced by several alternative  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.

# 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

CGE1 [B. ]

.

A B C

CGE2

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  got it wrong (corrected in ), SchroederHeister  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  and (independently)

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

[B. ]

.

A B A C

CGE

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

ABI

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

CE1 [ A. ]

.

A B B C

CE2

by means of which it is clear that, from the assumption of AB, one can construct a proof of AB 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 :

AB [ A]2 [B. ]1

.

B AB [B]4 [ A. ]3

.

A

BE1, 1 AE2, 3

ABI, 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.

•  López-Escobar  calls these “options”
•  López-Escobar  does it differently. Found a mistake? Please highlight the word and press Shift + Enter Related topics