Home Philosophy Advances in ProofTheoretic Semantics


GE Harmony: A CounterExampleFrancez 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” (Erules are GErules 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 ... 5): “noncombining” (zero or one premiss[es]) or “combining” (more than one premiss) corresponds to possibility 2; “hypothetical” (a premiss with assumptions discharge) or “categorical” (no such discharge) corresponds to possibility 3; “parametrized” (a premiss depends on a free variable) corresponds roughly to a mixture of 4 and 5; “conditional” (e.g. there is a freshness condition) corresponds roughly to 4. Let us now consider a combination of such ideas, e.g. two Irules each of which discharges an assumption, e.g. the pair [ A. ] . B A O B [B. ] . A A O B What is/are the appropriate GErule(s)? It/they might be just [B. ] . A O B A C C but that only captures, as it were, the first of the two Irules (and implies that ( AOB) ⊃ ( A ⊃ B), surely not what should be the case); so we have to try also [ A. ] . A O B B C C 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 [B. ] . [ A. ] . A O B A C B C C which is weird; with only the second and last of these premisses, already C can be deduced. The meaning of A O B is thus surely not being captured, whether we go for two GErules or just one. A similar example was given in 1968 by von Kutschera [38, p. 15], with two Irules for an operator F based on the informal definition F ( A, B, C) ≡ ( A ⊃ B)∨(C ⊃ B) but the flattened Erule failing to capture the definition adequately. Another [Counter]ExampleFollowing Zucker and Tragesser's [42, p. 506], Olkhovikov and SchroederHeister [21] have given as a simpler example the ternary constant with two introduction rules: [ A. ] . B ( A, B, C) I1 C ( A, B, C) I2 and the “obvious” GE rule thereby justified is: ( A, B, C) A [B. ] . D [C. ] . D D GE which is clearly wrong, there being nothing to distinguish it from ( A, C, B). Their main point is to show by a semantic argument that there is no nonobvious GE rule for , thus defending the “idea of higherlevel rules” [30]. 
< Prev  CONTENTS  Next > 

Related topics 