Home Philosophy Advances in ProofTheoretic Semantics


Several IRulesWhere a logical constant (such as ∨) is introduced by several alternative ^{[1]} rules, one can formulate an appropriate GErule as having several minor14 premisses, one for each of the Irules, 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 Irules is to ensure that “the GErule” has n minor premisses. This works well for ⊥, with no Irules: the ⊥E rule, as in [9, 24], has no minor premises^{[2]}. IRule Has Several PremissesNow there are two possibilities following the general idea that the conclusion of a GErule is arbitrary. Let us consider the intuitionistic constant ∧ (with its only Irule 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 GErules: [ A. ] . A B C C ∧GE1 [B. ] . A B C C ∧GE2 and it is routine to show that the ordinary GErule for ∧ is derivable in a system including these two rules, and viceversa. 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 IRule Discharges Some AssumptionsNatural deduction's main feature is that assumptions can be discharged, as illustrated by the Irule for ⊃ and the Erule for ∨. This raises difficulties for the construction of the appropriate GErules: 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” GErule 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 Irule, namely [ A. ] . [B. ] . B A A ≡ B ≡ I According to our methodology, we have two possibilities for the GErule; 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 viceversa. The alternative is to have two GErules, along the lines discussed above for ∧, and these are clearly [B. ] . A B A C C ≡ E1 [ A. ] . A B B C C ≡ E2 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 ≡ E1, 1 A ≡ E2, 3 A ≡ B ≡ I, 2, 4 We are thus committed in general to the use of the second rather than the first possibility of GErules—the use of two such rules rather than one—when there are two premisses in an Irule. 
CONTENTS 

Related topics 