Home Philosophy Advances in Proof-Theoretic Semantics

## GE Harmony: A Counter-ExampleFrancez and the present author [8]16 developed these ideas (looking also at the analogues of universal and existential quantification) by defining the notion of “GEharmony” (E-rules are GE-rules obtained according to a formal procedure, of which parts are as described above) and showing that it implied “local intrinsic harmony” (local soundness, i.e. reductions, and local completeness, as illustrated above for ). The classification in [8] corresponds roughly but not exactly to the different possibilities enumerated above (1 Let us now consider a combination of such ideas, e.g. two I-rules each of which discharges an assumption, e.g. the pair [ .
B [B. ].
BWhat is/are the appropriate GE-rule(s)? It/they might be just [ .
but that only captures, as it were, the first of the two I-rules (and implies that
[ .
16Written in 2007–9, several years before publication. but then these two need to be combined somehow. If into a single rule,it would be something like [ . [ .
which is weird; with only the second and last of these premisses, already for two GE-rules or just one. A similar example was given in 1968 by von Kutschera [38, p. 15], with two I-rules for an operator but the flattened E-rule failing to capture the definition adequately. ## Another [Counter-]ExampleFollowing Zucker and Tragesser's [42, p. 506], Olkhovikov and Schroeder-Heister [21] have given as a simpler example the ternary constant with two introduction rules: [ .
and the “obvious” GE rule thereby justified is: .
.
which is clearly wrong, there being nothing to distinguish it from |

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

Related topics |

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