Logical harmony
Encyclopedia
Logical harmony, a name coined by Sir Michael Dummett, is a supposed constraint on the rules of inference that can be used in a given logical system.
The logician Gerhard Gentzen
proposed that the meanings of logical connective
s could be given by the rules for introducing them into discourse. 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 having rules like this is what gives meaning to one's words, or at least to certain words. The idea has also been associated with Wittgenstein's dictum that in many cases we can say, the meaning is the use. Most contemporary logicians prefer to think that the introduction rules and the elimination rules for an expression are equally important. In this case, and is characterized by the following rules:
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. He was answered by Nuel Belnap
, that even though introduction and elimination rules can constitute meaning, not just any pair of such rules will determine a meaningful expression – they must meet certain constraints, such as not allowing us to deduce any new truths in the old vocabulary. These constraints are what Dummett was referring to.
Harmony, then, refers to certain constraints that a proof theory must let hold between introduction and elimination rules for it to be meaningful, or in other words, for its inference rules to be meaning-constituting.
The application of harmony to logic may be considered a special case; 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.
The logician Gerhard Gentzen
Gerhard Gentzen
Gerhard Karl Erich Gentzen was a German mathematician and logician. He had his major contributions in the foundations of mathematics, proof theory, especially on natural deduction and sequent calculus...
proposed that the meanings of logical connective
Connective
Connective may be referring to:* Bains::connective* Logical connective* Connective tissue* Discourse connective, in linguistics, a word or phrase like "therefore" or "in other words"....
s could be given by the rules for introducing them into discourse. 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
Logical conjunction
In logic and mathematics, a two-place logical operator and, also known as logical conjunction, results in true if both of its operands are true, otherwise the value of false....
as follows: The sky is blue AND grass is green. Gentzen's idea was that having rules like this is what gives meaning to one's words, or at least to certain words. The idea has also been associated with Wittgenstein's dictum that in many cases we can say, the meaning is the use. Most contemporary logicians prefer to think that the introduction rules and the elimination rules for an expression are equally important. In this case, and is characterized by the following rules:
| Intro: | | Elim: | |
|---|---|---|
| p q | p and q | p and q |
| ------- | ------- | ------- |
| p and q | p | q |
An apparent problem with this was pointed out by Arthur Prior
Arthur Prior
Arthur Norman Prior was a noted logician and philosopher. Prior founded tense logic, now also known as temporal logic, and made important contributions to intensional logic, particularly in Prior .-Biography:Prior was entirely educated in New Zealand, where he was fortunate to have come under the...
: 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. He was answered by Nuel Belnap
Nuel Belnap
Nuel D. Belnap, Jr. is an American logician and philosopher who has made many important contributions to the philosophy of logic, temporal logic, and structural proof theory. He has taught at the University of Pittsburgh since 1961; before that he was at Yale University. His best known work is...
, that even though introduction and elimination rules can constitute meaning, not just any pair of such rules will determine a meaningful expression – they must meet certain constraints, such as not allowing us to deduce any new truths in the old vocabulary. These constraints are what Dummett was referring to.
Harmony, then, refers to certain constraints that a proof theory must let hold between introduction and elimination rules for it to be meaningful, or in other words, for its inference rules to be meaning-constituting.
The application of harmony to logic may be considered a special case; 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
Semantic theory of truth
A semantic theory of truth is a theory of truth in the philosophy of language which holds that truth is a property of sentences.-Origin:The semantic conception of truth, which is related in different ways to both the correspondence and deflationary conceptions, is due to work published by Polish...
, but many philosophers interested in reconstituting the semantics of logic in a way that respects Ludwig Wittgenstein
Ludwig Wittgenstein
Ludwig Josef Johann Wittgenstein was an Austrian philosopher who worked primarily in logic, the philosophy of mathematics, the philosophy of mind, and the philosophy of language. He was professor in philosophy at the University of Cambridge from 1939 until 1947...
's meaning is use have felt that harmony holds the key.
External links
- Harmony at Greg Restall's Proof and Consequence wiki