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 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 [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. 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 GE-rules from a set of I-rules with results about harmony.

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

Found a mistake? Please highlight the word and press Shift + Enter