Home Philosophy Advances in ProofTheoretic Semantics
The GErule for Implication and the TypeTheoretic Dependent Product TypeThe present author commented [3] that the general (aka “flattened” [29]) Erule for implication didn't look promising because it didn't generalise to type theory. Here (after 27 years) are the details of this problem: Recall [15] that in the dependentlytyped context A type, B(x ) type [x : A], the rule [z : I:(.A, B)] . [x : A, y : B(x )] . . p : I:( A , B ) C (z ) type c (x , y ) : C ((x , y )) spli t ( p, c) : C( p) I: E with6 semantics spli t ((a, b), c) → c(a, b) is a generalisation of the rule [x : A,. y : B] . p : A × B C type c (x , y ) : C spli t ( p, c) : C ×E . Now, ordinary (but with witnesses) Modus Ponens f : A ⊃ B a : A fa : B ⊃ E has, in the dependentlytyped context A type, B(x ) type [x : A], the generalisation (in which ap2( f, a) is often just written as f a or ( f a)): f : Π(A , B ) a : A ap2( f, a) : B(a) Π E (with Π( A, B) written as A ⊃ B whenever B(x ) is independent of x ); but the “flattened” GE rule [y :. B] . f : A ⊃ B a : A C type c ( y ) : C ap3( f, a, c) : C ⊃ GE with semantics ap3(λ(g), a, c) → c(g(a)) doesn't appear to generalise: [z : Π (.A, B)] . [y : B(a)] . . f : Π(A , B ) a : A C (z ) type c ( y ) : C (λ(?)) ap3( f, a, c) : C( f ) in which, note the questionmark—what should go there? In the context y : B(a), the only ingredient is y, which won't do—it has the wrong type. Addition of an assumption such as x : A (and making c depend on it, as in c(x , y)) doesn't help. 6The notation c is used to abbreviate λxy.c(x , y). Similar abbreviations are used below. c(a, b) is then just c applied to a and then to b. One solution is the system of higherlevel rules of SchroederHeister [30]. Our own preference, to be advocated after a closer look at flattened GErules, is for implication (and universal quantification) to be taken as primitive, with Modus Ponens and the Π E rule taken as their elimination rules, with justifications as in [15]. GERules in GeneralThe widespread idea that the “grounds for asserting a proposition” collectively form some kind of structure which can be used to construct the assumptions in the minor premiss(es) of a GErule is attractive, as illustrated by the idea that, where two formulae A, B are used as the grounds for asserting A ∧ B, one may make the pair A, B the assumptions of the minor premiss of ∧GE . An example of this is LópezEscobar's [13], which gives Irules and then GErules for implication and disjunction, with the observation [13, p. 417] that: Had the corresponding Irule had three “options with say 2, 3 and 5 premises respectively, then there would have been 2 × 3 × 5 Erules corresponding to that logical atom. Also had there been an indirect premise, say ∇D/E, in one of the options then it would contribute a minor premise with conclusion E and a transfer premise with discharged sentence D to the appropriate Erule. In practice, there is an explosion of possibilities, which we analyse in order as follows: 1. a logical constant, such as ⊥, ∧, ∨, ≡ or ⊕ (exclusive or), can be introduced by zero or more rules; 2. each of these rules can have zero or more premisses, e.g. TI has zero, ⊃ I and each ∨Ii have one, ∧I has two; 3. each such premiss may discharge zero or more assumptions (as in ⊃ I ); 4. each such premiss may abstract over one or more variables, as in ∀I ; 5. and a premiss may take a term as a parameter (as in ∃I ). It is not suggested that this list is exhaustive: conventions such as those of substructural logic about avoiding multiple or vacuous discharge will extend it, as would recursion; but it is long enough to illustrate the explosion. The paper [8] attempted ^{[1]} to deal with all these possibilities and carry out a programme of mechanically generating GErules from a set of Irules with results about harmony.

< Prev  CONTENTS  Next > 

Related topics 