Logical harmony, a name coined by Michael Dummett, is a property on the rules of inference that a given logical system can satisfy.
Overview The logician Gerhard Gentzen proposed that the meanings of logical connectives does not need to be defined by a world outside of logic, but could be given by the rules for using them within logic itself. For example, if one believes that the sky is blue and one also believes that grass is green, then one can introduce the connective and as follows: The sky is blue AND grass is green. Gentzen's idea was that such rules give meaning to one's words, or at least to logical connectives. The idea has also been associated with the Wittgensteinian notion that in many cases we can say, meaning is use. It is also called inferential role semantics, or inferentialism. In a natural deduction system, each logical connectives has two types of rules: the introduction rules and the elimination rules. In this case, and is introduced and eliminated by the following rules: P Q P ∧ Q , P ∧ Q P , P ∧ Q Q {\displaystyle {\frac {P\quad Q}{P\land Q}},\quad {\frac {P\land Q}{P}},\quad {\frac {P\land Q}{Q}}} An apparent problem with this was pointed out by Arthur Prior: Why can't we have an expression (call it "tonk") whose introduction rule is that of OR (from "p" to "p tonk q") but whose elimination rule is that of AND (from "p tonk q" to "q")? This lets us deduce anything at all from any starting point. Prior suggested that this meant that inferential rules could not determine meaning, i.e. inferentialism is false. Nuel Belnap responded that introduction and elimination rules can constitute meaning, provided that the rules must meet certain constraints, such as not allowing us to deduce any new truths in the old vocabulary. The concept of harmony formalizes this. The introduction and elimination rules of a logical connective are in harmony if in any proof, maximal formulas can be eliminated by normalizing the proof. A maximal formula is a formula that is introduced, then eliminated later. The idea is that such maximal formulas behave similarly to lemmas, and while they can make the proof easier to write and shorter, are not strictly necessary. A normalized proof ought to only introduce logical connectives, and never eliminate them. The deeper reason for such a demand is that, ideally, the introduction rules for a connective describes the conditions that can justify the connective. For example, A ∧ B {\displaystyle A\land B} is justified given a proof of A {\displaystyle A} and a proof of B {\displaystyle B} . On the other side, the elimination rules for a connective describes the conditions that the connective can justify. For example, a proof of A ∧ B {\displaystyle A\land B} justifies A {\displaystyle A} and also justifies B {\displaystyle B} . The idea of harmony is that what a connective justifies should be exactly the same as what justifies that connective. This is the main idea of Prawitz's "Inversion Principle". The application of harmony to mathematical logic may be considered a special case of the philosophical concept. It makes sense to talk of harmony with respect to not only inferential systems, but also conceptual systems in human cognition, and to type systems in programming languages. Semantics of this form has not provided a very great challenge to that sketched in Tarski's semantic theory of truth, but many philosophers interested in reconstituting the semantics of logic in a way that respects Ludwig Wittgenstein's meaning is use have felt that harmony holds the key.
References
External links harmony at Greg Restall's Proof and Consequence wiki (archive copy, July 2012)
