Harmony principle (logic)

from Wikipedia, the free encyclopedia

The principle of harmony (Engl. Principle of harmony ) is a metalogical principle for calculi of natural deduction requested the introduction and elimination rules for logical operators that in "harmony" should be located, that is, roughly speaking, that the elimination rule for a given Operator does not allow the transition to logically stronger statements than is covered by the introductory rule. The term was coined by Michael Dummett ; the idea that there must be a principle of harmony, however, was already anticipated by Gerhard Gentzen .

Prehistory: Prior's challenge to proof-theoretical semantics

In 1934, Gentzen proposed semantically characterizing the logical operators by specifying a pair of introduction and elimination rules for each operator. The introductory rule specifies the conditions under which a statement may be inferred that contains the operator in question as the main operator; the elimination rule indicates what can be inferred from such a statement. For example, the rules for conjunction in a calculus of natural inference are as follows:

The conjunction “A and B” can be inferred from two statements A and B (rule of the introduction of the conjunction).
Example: From the statements “Skolem was Norwegian” (A) and “Skolem was a logician” (B) it can be concluded: “Skolem was a Norwegian and a logician” (A ∧ B).
Every single conjunct, i.e. both A and B, can be deduced from a conjunction “A and B” (rule of eliminating the conjunctions).
Example: From “Skolem was a Norwegian and a logician” (A ∧ B) it can be concluded: “Skolem was a Norwegian” (A) - and also “Skolem was a logician” (B).

Gentzen and, following him, the representatives of the proof-theoretic semantics assume that these rules indicate the meaning of the logical operators. Arthur Prior pointed out a possible problem with this assumption in his essay "The runabout inference ticket": What prevents us from introducing a junctor "tonk" whose introductory rule corresponds to that of the adjunct introduction (from A follows A tonk B), but whose elimination rule corresponds to the conjunctival elimination (from A tonk B follows A)? This would allow any statement to be derived from any given premises and lead to a trivialization of logic:

At first glance, this is a very strong argument against the idea that the rules of usage determine the meaning of a term. In his contribution to the debate sparked by Prior, JT Stevenson drew the lesson from this that the meaning of the logical operators must already be established before inference rules are given, and that the inference rules are based on this predefined meaning (e.g. by truth tables ) to orient.

The harmony principle as a solution

Gentzen himself had already seen the need for harmony between the rules of introduction and rules of elimination:

The introductions represent, so to speak, the “definitions” of the characters in question, and the eliminations are ultimately only consequences of what can be expressed as follows: When eliminating a character, the formula in question, the outermost character of which is involved here, may only "To be used as what it means by virtue of the introduction of this mark". […] By specifying these ideas, it should be possible to prove the elimination conclusions on the basis of certain requirements as unambiguous functions of the associated introduction conclusions.

The approach suggested by Gentzen amounts to considering the introductory rules as semantically primary and deriving the elimination rules from them; The inversion principle (see below) provides one possibility for this. Belnap and Dummett, on the other hand, propose the definition- theoretical requirement for conservatism or non-creativity as a more precise specification of the harmony requirement .

Non-creativity

Nuel Belnap argued in his reply to Prior that, without prejudice to the fact that rules determine the meaning of an expression, not just any (pairs of) rules are suitable. The rules of introduction and elimination must be harmonious, and Belnap explains this as follows: The rules for a new operator must not allow the derivation of statements that do not contain the newly introduced expression and were previously not derivable. The operator tonk violates this requirement in an obvious way.

The idea that in this sense there must be a harmony between the truth and assertability conditions of a statement and its consequences was extended by Michael Dummett to non-logical vocabulary:

A simple case would be that of a pejorative term, eg ' Boche '. The condition for applying the term to someone is that he is of German nationality; the consequences of its application are that it is barbarous and more prone to cruelty than other Europeans. [...] The addition of the term 'Boche' to a language which did not previously contain it would produce a non-conservative extension, ie one in which certain other statements which did not contain the term were inferable from other statements not containing it which were not previously inferable.

The corollary sequence “Fritz is German; so Fritz is a Boche; So Fritz is cruel ”shows that the introduction of the expression 'Boche' represents a non-conservative language extension: The statement“ Fritz is cruel ”would not be inferred from the statement“ Fritz is German ”without the intermediate step about“ Fritz is a Boche ” . However, it is questionable whether non-conservatism is a problem with non-logical vocabulary. The demand for non-creativity for every newly introduced expression would amount to a ban on real language extensions, which is not plausible for natural languages.

Inversion principle

Following the work of Paul Lorenzen , Dag Prawitz proposed to explicate harmony by resorting to the so-called inversion principle: there must be a symmetry between rules of introduction and rules of elimination in such a way that the content of a conclusion reached by applying an elimination rule to a premise P. may not go beyond what was already contained in the premises from which P was inferred by means of the associated introductory rule. For example, if A ∧ BA inferred, this is permissible because A ∧ B is (typically) obtained by applying the introduction of the conjuncture to the premises A and B. The proof for a conclusion obtained by means of the elimination rule is thus already contained in the proof for its premises if the main premise has been inferred by means of the corresponding introductory rule. The term inversion principle is intended to make it clear that an application of an elimination rule only reverses what has been achieved by the associated introduction rule.

Harmony in terms of logical strength

Neil Tennant suggested the following harmony criterion in Natural Logic :

Introduction and elimination rules for a logical operator λ must be formulated so that a sentence with λ dominant expresses the strongest proposition which can be inferred from the stated premises when the conditions for λ-introduction are satisfied; while it expresses the weakest proposition possible under the conditions described by λ-elimination.

How the various criteria for harmony relate to one another (e.g. whether they can be traced back to one another) has not yet been clarified.

literature

Reprinted in: Karel Berka , Lothar Kreiser (eds.): Logic texts . Annotated selection on the history of modern logic , Berlin: Akademie-Verlag, 4th edition 1986.
Online version of the University of Göttingen: Part 1 and Part 2

Web links

Individual evidence

  1. ↑ Gentzen, "Investigations into Logical Inference".
  2. ^ Stevenson, "Roundabout the Runabout Inference Ticket".
  3. ^ Gentzen, "Investigations into logical reasoning", p. 189.
  4. ^ Belnap, "Tonk, Plonk and Plink", p. 131ff.
  5. ↑ See Brandom, Making it Explicit , p. 125.
  6. ^ Dummett, Frege: Philosophy of Language , p. 454.
  7. ^ Brandom, Making it Explicit , p. 127.
  8. ^ Prawitz, Natural Deduction .
  9. ↑ Lorenzen, "Constructive Justification of Mathematics".
  10. ↑ Lorenzen, Introduction to Operational Logic and Mathematics .
  11. ^ Tennant, Natural Logic , p. 74; quoted Tennant, "Inferentialism, Logicism, Harmony, and a Counterpoint," p. 19.
  12. ^ Tennant, "Inferentialism, Logicism, Harmony, and a Counterpoint," p. 15.