Logical harmony, a name coined by

Michael Dummett Sir Michael Anthony Eardley Dummett (27 June 1925 – 27 December 2011) was an English academic described as "among the most significant British philosophers of the last century and a leading campaigner for racial tolerance and equality." He wa ...

, is a supposed constraint on the

rules of inference In the philosophy of logic, a rule of inference, inference rule or transformation rule is a logical form consisting of a function which takes premises, analyzes their syntax, and returns a conclusion (or conclusions). For example, the rule of in ...

that can be used in a given

logical system A formal system is an abstract structure used for inferring theorems from axioms according to a set of rules. These rules, which are used for carrying out the inference of theorems from axioms, are the logical calculus of the formal system. A form ...

Overview

The logician

Gerhard Gentzen Gerhard Karl Erich Gentzen (24 November 1909 – 4 August 1945) was a German mathematician and logician. He made major contributions to the foundations of mathematics, proof theory, especially on natural deduction and sequent calculus. He died o ...

proposed that the meanings of

logical connective In logic, a logical connective (also called a logical operator, sentential connective, or sentential operator) is a logical constant. They can be used to connect logical formulas. For instance in the syntax of propositional logic, the binary co ...

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 or AND may refer to: Logic, grammar, and computing * Conjunction (grammar), connecting two words, phrases, or clauses * Logical conjunction in mathematical logic, notated as "∧", "⋅", "&", or simple juxtaposition * Bitwise AND, a boole ...

'' 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 the Wittgensteinian notion that in many cases we can say, '' meaning is use''. Most contemporary logicians prefer to think that the

introduction rule In logic and proof theory, natural deduction is a kind of proof calculus in which logical reasoning is expressed by inference rules closely related to the "natural" way of reasoning. This contrasts with Hilbert-style systems, which instead use axiom ...

s and the

elimination rule In logic and proof theory, natural deduction is a kind of proof calculus in which logical reasoning is expressed by inference rules closely related to the "natural" way of reasoning. This contrasts with Hilbert-style systems, which instead use axio ...

s for an expression are equally important. In this case, ''and'' is characterized by the following rules: {, border="1" cellpadding="6" cellspacing="0" align="center" , - ! Intro ! colspan="2" , Elim , - , {, border="0" , - , P , , , , , , Q , - , colspan="4" style="border-top:2px solid black;" , , - , colspan="4" align="center" , P and Q , {, border="0" , - , P and Q , - , style="border-top:2px solid black;" , , - , align="center", P , {, border="0" , - , P and Q , - , style="border-top:2px solid black;" , , - , align="center", Q An apparent problem with this was pointed out by

Arthur Prior Arthur Norman Prior (4 December 1914 – 6 October 1969), usually cited as A. N. Prior, was a New Zealand–born logician and philosopher. Prior (1957) founded tense logic, now also known as temporal logic, and made important contribution ...

: 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 Dinsmore Belnap Jr. (; born 1930) is an American logician and philosopher who has made contributions to the philosophy of logic, temporal logic, and structural proof theory. He taught at the University of Pittsburgh from 1963 until his ret ...

, 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 system In mathematical logic, a proof calculus or a proof system is built to prove statements. Overview A proof system includes the components: * Language: The set ''L'' of formulas admitted by the system, for example, propositional logic or first-order ...

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 system In computer programming, a type system is a logical system comprising a set of rules that assigns a property called a type to every "term" (a word, phrase, or other set of symbols). Usually the terms are various constructs of a computer progra ...

s in programming languages.

Semantics Semantics (from grc, σημαντικός ''sēmantikós'', "significant") is the study of reference, meaning, or truth. The term can be used to refer to subfields of several distinct disciplines, including philosophy Philosophy (f ...

of this form has not provided a very great challenge to that sketched in Tarski's

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 deflati ...

, but many philosophers interested in reconstituting the semantics of logic in a way that respects

Ludwig Wittgenstein Ludwig Josef Johann Wittgenstein ( ; ; 26 April 1889 – 29 April 1951) was an Austrian-British philosopher who worked primarily in logic, the philosophy of mathematics, the philosophy of mind, and the philosophy of language. He is considere ...

's ''meaning is use'' have felt that harmony holds the key.

References

, "The runabout inference ticket." ''Analysis'', 21, pp. 38–39, 1960–61. * Nuel D. Belnap Jr., "Tonk, Plonk, and Plink", ''Analysis'', 22, pp. 130–134, 1961–62. *

''The Logical Basis of Metaphysics''
(

Harvard University Press Harvard University Press (HUP) is a publishing house established on January 13, 1913, as a division of Harvard University, and focused on academic publishing. It is a member of the Association of American University Presses. After the retirem ...

, 1991)

External links

harmony
at

Greg Restall Greg Restall (born 11 January 1969) is an Australian philosopher and Professor of Philosophy at the University of St Andrews. He is a fellow of the Australian Academy of the Humanities. Restall is known for his research on logic and theories ...

's Proof and Consequence wiki (archive copy, July 2012) Philosophy of mathematics Logic