Home Philosophy Advances in Proof-Theoretic Semantics

## The Problem of HarmonyIn the proof-theoretic semantics of logical constants, harmony is a, or perhaps the, crucial concept. If we work in a natural-deduction framework, harmony is a property that introduction and elimination rules for a logical constant are expected to satisfy with respect to each other in order to be appropriate. Harmony guarantees that we do not gain anything when applying an introduction rule followed by an elimination rule, but also, conversely, that from the result of applying elimination rules we can, by applying introduction rules, recover what we started with. The notion of harmony or 'consonance' was introduced by Dummett ([13], pp. 396–397).3 However, it is not absolutely clear how to define harmony. Various competing understandings are to be found in the literature. We identify a particular path that has not yet been explored, and we call this path 'intensional' or 'strong' harmony. The need to consider such a notion on the background of the discussion, initiated by Prawitz [45], on the identity of proofs, in particular in the context of Kosta Došen's work (see Došen [6, 8, 9], Došen and Petric´ [12]), was raised by Luca Tranchini.4 As the background to this issue we first present two conceptions of harmony, which are not reliant on the notion of identity of proofs. ## Harmony Based on Generalised RulesAccording to Gentzen “the introductions represent so-to-speak the 'definitions' of the corresponding signs” whereas the eliminations are “consequences” thereof, which should be demonstrated to be “unique functions of the introduction inferences on the basis of certain requirements” (Gentzen [25], p. 189). If we take this as our characterisation of harmony, we must specify a function There have been various proposals to formulate elimination rules in a uniform way with respect to given introduction rules, in particular those by von Kutschera [36], Prawitz [47] and Schroeder-Heister [53]. At least implicitly, they all intend to capture the notion of harmony. Read [51, 52] has proposed to speak of 'general-elimination harmony'. Formulated as a principle, we could say: Given a set Consequently the generalised elimination rules
the canonical elimination rule takes the form [
The exact specification of what the While the standard approaches use introduction rules as their starting point, it is possible in principle, and in fact not difficult, to develop a corresponding approach based on elimination rules. Given a set of elimination rules
then the canonical introduction rule takes the form [
Here the conclusions of the elimination rules become premisses of the canonical introduction rules. Again, the exact specification of used. For example, if, for the four-place connective ∧ →, the set ∧→ the three elimination rules
6In this section, we do not distinguish between schematic letters for formulas and propositional variables, as we are also considering propositional quantification. Therefore, in a rule schema such as we would define [
∧→ In Schroeder-Heister [63] functions |

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

Related topics |

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