The “flattening” methodology when either the constant being defined has several introduction rules or one or more of such rules have several premisses can lead

1. to a number (>1) of GE rules, none of which on its own suffices, and

2. to a “disharmonious mess”, i.e. a failure to capture the correct meaning.

Already there are enough problems, before we start considering the cases where the premiss abstracts over several variables, instantiates a variable as a term or recurses on the constant being defined.

The solution of Schroeder-Heister [30] is to allow rules to discharge rules. We prefer, however, to propose instead that one should adopt the standard solution from (e.g.) Coq [1]: to reject the idea that the rule for handling implication (and other situations where assumptions are discharged) be treated as illustrated above and instead to take implication (and its generalisation, universal quantification), together with an inductive definition mechanism, as primitive, with traditional “special” elimina-

tion rules (e.g. Modus Ponens) but to allow GE rules elsewhere (e.g. for ∧ and its

generalisations I: and ∃). This deals with ≡; likewise, it deals with O as if it were

[ A ⊃. B]

. [B ⊃. A]

.

AOB C C

C .

More precisely, we note that with an introduction rule given in Coq by the inductive definition

Inductive and (A B : Prop) : Prop := and_I : A -> B -> (and A B).

we obtain as a theorem

Theorem and_elim : forall A B C : Prop, (and A B) -> (A -> B -> C) -> C.

and similarly for O we have the inductive definition

Inductive odot (A B : Prop) : Prop :=

| odot_I_1 : (A -> B) -> (odot A B)

| odot_I_2 : (B -> A) -> (odot A B).

and we can obtain as a theorem

Theorem odot_elim : forall A B C : Prop,

(odot A B) -> ((A -> B) -> C) -> ((B -> A) -> C) -> C.

Not only can we obtain such theorems, but Coq will calculate them (and several variants) from the definitions automatically. Further details of this approach can be found in [23]. For example, existential quantification can be defined thus (we give also the obtained theorem representing the elimination rule):

Inductive ex (X:Type) (B : X -> Prop) : Prop := ex_intro : forall (w:X), B w -> ex X B.

Theorem ex_elim : forall X : Type, B : X -> Prop,

C : Prop, (ex X B) -> (forall (x:X) (B x -> C)) -> C.

Short shrift is given to •:

Inductive bullet : Prop :=

bullet_I : ( (bullet -> False) -> bullet).

Error: Non strictly positive occurrence of"bullet" in "(bullet -> False) -> bullet"

This pushes the problem (of constructing and justifying elimination rules given a set of introduction rules, and establishing properties like harmony, local completeness and stability) elsewhere: into the same problem for a mechanism of inductive definitions and for the rules regarded as primitive: introduction and (non-general) elimination rules for implication and universal quantification. Apart from the issue of stability, we regard the latter as unproblematic, and the former as relatively straightforward (once we can base the syntax on implication and universal quantification).

To a large extent this approach may be regarded as just expressing first-order connectives using second-order logic, and not very different from Schroeder-Heister's higher-level rules. The important point is that there are difficulties (we think unsurmountable) with trying to do it all without such higher-order mechanisms.

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