Home Philosophy Advances in Proof-Theoretic Semantics

## Towards a Definition of Strong HarmonyFor simplicity, take the notion of reductive harmony mentioned in Sect. 3.2. Given introduction rules What we would like to achieve, in any case, is that the canonical eliminations for given introductions are in strong harmony with the introductions, and similarly that the canonical introductions for given eliminations are in strong harmony with the eliminations. The second case is trivial, as the premisses of the canonical introduction are exactly the conclusions of the eliminations. For example, if for the connective ↔ the elimination rules
1 ↔ p 2 p 1
are assumed to be given, then its canonical introduction rule has the form
Both the elimination meaning ↔
the first case, where the canonical eliminations are given by the general elimination rules, the situation is more problematic. Consider disjunction with the rules [
Here the introduction meaning of they are not isomorphic. There are proofs
∀
of ∀ ∀ the identity proof ∀ ∀ is also eliminated due to its definability in IPC2). To accommodate this objection, we consider the example of the trivial connective + with the introduction and elimination rules
+
Here the elimination rule is the canonical one according to the general-elimination schema. In order to demonstrate strong harmony, we would have to establish the isomorphism of be related to the fact that for the second-order translations of propositional formulas, we do not have
ination. We have a problem in the case of the connective +, which has the introduction meaning alternative elimination rule is derivable, namely the rule
In fact, this sort of elimination rule is available for all connectives with only a single introduction rule. We call it the 'direct' as opposed to the 'indirect' elimination rule. For example, the connective &⊃ with the introduction rule [
has as its direct elimination rules
If we require that the canonical elimination rules always be direct where possible, that is, whenever there is not more than one introduction rule, and indirect only if there are multiple introduction rules, then the problem of reduction to IPC2 seems to disappear. In the direct case of a single introduction rule, the elimination meaning is trivially identical to the introduction meaning. In the indirect case, they now become trivially identical again. This is because disjunction, which is used to express the introduction meaning for multiple introduction rules, is translated into disjunctionfree second-order logic in a way that makes its introduction meaning identical to its elimination meaning. This second proposal would require the revision of basic tenets of proof-theoretic semantics, because ever since the work of von Kutschera [36], Prawitz [47] and Schroeder-Heister [53] on general constants, and since the work on general elimination rules, especially for implication, by Tennant [69, 70], López-Escobar [37] and von Plato [43],12 the idea of the indirect elimination rules as the basic form of elimination rules for 12For a discussion see Schroeder-Heister [65]. rules. If we consider conjunction with ∧
then ∧ [
whereas ∧ |

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

Related topics |

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