Home Philosophy Advances in Proof-Theoretic Semantics

## In Other WordsThe “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 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.) tion rules (e.g. generalisations [ . [ .
More precisely, we note that with an introduction rule given in 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 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. |

< Prev | CONTENTS | Next > |
---|

Related topics |

Academic library - free online college e textbooks - info{at}ebrary.net - © 2014 - 2020