Home Philosophy Advances in Proof-Theoretic Semantics
The GE-rule for Implication and the Type-Theoretic Dependent Product Type
The present author commented  that the general (aka “flattened” ) E-rule 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  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 dependently-typed 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 question-mark—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 higher-level rules of Schroeder-Heister . Our own preference, to be advocated after a closer look at flattened GE-rules, 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 .
GE-Rules in General
The wide-spread 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 GE-rule 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ópez-Escobar's , which gives I-rules and then GE-rules for implication and disjunction, with the observation [13, p. 417] that: Had the corresponding I-rule had three “options with say 2, 3 and 5 premises respectively, then there would have been 2 × 3 × 5 E-rules 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 E-rule.
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  attempted  to deal with all these possibilities and carry out a programme of mechanically generating GE-rules from a set of I-rules with results about harmony.
|< Prev||CONTENTS||Next >|