# The GE-rule for Implication and the Type-Theoretic Dependent Product Type

The present author commented [3] that the general (aka “flattened” [29]) 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 [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 dependently-typed context

*A type, B(x ) type* [*x* : *A*],

the generalisation (in which *ap*2*( f, a)* is often just written as *f a* or *( f a)*):

__ __ __f ____:____ ____Π____(____A____ ____,____ ____B____ ____) ____a ____: ____A____ __

*ap*2*( 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____ __

*ap*3*( f, a, c)* : *C* ⊃ *GE*

with semantics *ap*3*(λ(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____ ____(λ(____?____))____ __

*ap*3*( 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 [30]. 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 [15].

# 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 [13], 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. T*I* 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 GE-rules from a set of I-rules with results about harmony.

- [1] “Transfer” premises in the terminology of [13]