logicandlanguage.net

It turns out that the usual cast of connectives - ¬, ∨, ∧, → and ↔ - have the following property: if anywhere in a proof there is an application of the introduction rule for a connective, followed immediately by an application of the elimination rule for that same connective which takes the result of the introduction rule as its major premise, then the introduction and elimination pair can be eliminated, leading to a more direct proof of the conclusion.

I should probably track down a presentation of the result, but for now I will give a couple of examples, which should convey the general idea of what this local reduction property amounts to. Suppose we have a proof that contains an instance of ∧-intro, followed immediately by ∧-elim on the result, like this:

P
Q
P ∧ Q (∧-intro)
P (∧-elim)

Then clearly the middle two steps are superflouous. We can obtain a more direct proof of P from the first premise. Here's a slightly less obvious case. Suppose we have a proof that contains an application of ∨-intro, followed by an application of ∨-elim, where the result of the ∨-intro is the major premise in the ∨-elim, e.g.:

¬Q
P
P∨Q (∨-intro_
(new subproof)
P
P
(end of subproof)
(new subproof)
Q
∧
P
(end of subproof)
P (∨-elim)

Again, the conclusion can be reached in a more direct way.

But it seems clear that 'tonk' does not have this local reduction property. Consider my argument

P (our premise)
P tonk Q (by tonk-intro)
Q (by tonk-elim)

which I used to show that 'there is life after death' followed from 'there is life on earth.' This just is an application of tonk-intro followed by tonk-elim. But, intuitively, without this step, the proof would not have been possible at all.

My impression is that discussions of 'tonk' have proceeded without awareness of the local reduction property, an impression that is reinforced by the fact that a google search for "local reduction" and "tonk" returns just a single hit - a multiple-choice geography exam for the Indian Civil Services. A google search for "local reduction" and "deduction" however, returns a host of computer science sites, the first of which reveals that the local reduction property has a twin, the local expansion property. Connectives which have this property can be reintroduced by their introduction rule after an application of the elimination rule. Connectives with the reduction property perserve the soundness of a system (tonk, of course, does not have it and destroys soundness,) while connectives with the expansion property preserve completeness.

It's in the literature, but it's not called the local reduction property. It's called normalisation. A natural deduction proof is normal if it has no so-called critical pairs (*I/*E) pairs, for the connective *. (For a gentle introduction, let me advertise Chapter 2 of Proof and Counterexample which covers normalisation in detail for the implicational fragment of natural deduction. The next chapter says a little (mainly in the exercises) about tonk.

(Am I playing to type?)

Actually, there has been a good deal of discussion of tonk and the "local reduction" property, though not necessarily under the names "tonk" and "local reduction". You should also be aware that this property doesn't hold for classical negation in natural deduction settings. (This part of the argument some people give in support of intuitionistic logic as more natural.) You might want to begin with Dummett's book The Logical Basis of Metaphysics (1991). "Tonk" is discussed (under another name) on p. 209. "Local reduction" is discussed (under the heading of "local peaks") on pp. 248-250. The whole discussion is quite complicated. Earlier work of Dag Prawitz is also relevant (mentioned in Dummett's bibliography). There have been a number of responses. Try the Philosopher's Index (search under Dummett, intuitionistic logic, logical constants...)

I am going to betray my ignorance.

"introduction and elimination rules for a connective give the connective's meaning"

What, may I ask, does that mean? What does it, er, mean, for a connective to have a meaning? Sure, a connective might imply stuff. "tonk" is something I fail to understand.

If P is true, then tonk(P, Q) is true.
If tonk(P, Q) then Q is true.

Can this not be re-written as P -> Q? What is tonk other than another way of expressing "implies"?

You seem to be having logical fits over the fact that you can prove anything with "tonk". I disagree. You can CLAIM anything with "tonk" - but that does not make it true. If I introduce a bad rule into my logical system, then I will not get true deductions out of it.

What is tonk other than a bad logical rule, and what are you really asking when you want to know what a logical connector means?

Surely "introduction and elimination rules for a connective give the connective's meaning" is, at its simplest, a truism. It is like saying "the rules by which we use a word (or symbol)" give its meaning.

I am assuming (possibly mistakenly) that you mean something deeper than this, and want to know something extra about what other meanings can be discovered by thinking about the rules of a connective.

One such meaning you discovered was that some connectives preserve soundness, and some don't, for some systems.

Maybe you will the following paper by A. Avron and I.Lev interesting:
http://antares.math.tau.ac.il/~aa/articles/nmatrices.pdf.

They address the Tonk problem using the tool of non-deterministic matrices.

Greg - yes, you've set a very high standard for yourself; I will be expecting a clarifying book-chapter for everything the computer science department can throw at me. "CS guy" is in fact the computer science department's official liaison with philosophy (cool idea, right?) and has a philosophy undergraduate degree, so there might be some interesting stuff coming this way...

Michael - thank you for the comments and suggestions, especially the tip-off about the links to intuitionism. That's very helpful.

Tennessee - ignorance welcome here, so betray away. That said, I agree with you that the proofs I gave using 'tonk' don't demonstrate the truth of their conclusions, even if the premises are true; they have contradictory conclusions. (Though I've just noticed that your name links to melbournephilosophy.com, so maybe you won't buy that reason for rejecting the truth of the conclusions.)

But (as you may have realised already,) the rules for 'tonk' are not the same as the rules for the conditional. If they were, we would always be able to get P→Q from P (not to be confused with being able to get P→Q from Q, of course.) The elimination rule is different too. One cannot get Q from P→Q alone, one needs P as well.

What does it mean to say that the rules give the meanings of the connectives? Well, that is a good question, worthy of a lot more than I am about to afford it. But here I will just say three things. In connection with natural deduction systems, I think it was Gerhard Gentzen (the inventor of natural deduction) who suggested that we think of the elimination rules in a natural deduction system as giving the meaning of the connectives. But that suggestion is related to an older and more general idea that I associate with Frege, namely that the meaning of an expression is determined by what one commits oneself to when one asserts a sentence containing it. (This is a shamelessly loose expression of something I dimly recall.) And of course, the elimination rules for a connective determine what follows from a sentence containing it (and hence what one is committed to if one asserts it.) This is an interesting and substantive suggestion, though perhaps in need of more clarification. It will be almost impossible to understand, however, from two viewpoints. First, if you assume that all expressions get their meanings by picking out objects and properties in the world ('Fido' means Fido, 'yellow' means yellow...etc) then it seems like a category mistake to say that the meaning of a connective is a rule. The remedy here may be to see that the meanings of words are a pretty diverse bunch of things. 'Fido', I bet, gets its meaning by picking out Fido. But 'hello' doesn't get its meaning by picking something out, and nor (in one sense) do indexicals like 'I' or 'today.' Yet they still have meanings. Alternatively, if you think that every expression gets its meaning by being associated with a rule (e.g. 'bachelor' means unmarried man) and that this rule is the meaning, then it may seem trivial to say that the meaning of a logical connective is the rule governing it. But (thanks largely to Kripke and Scott Soames) I don't think that all expressions work like that. Names, for instance, get their meanings by being associated with objects. Competent speakers don't need to know any rule that picks out the referent of, say, "Ganymede" (the name of one of the moons of Jupiter) and I might not know any rule that will pick it out uniquely. So one thing we would be denying if we asserted that the rules governing a connective are, or give, its meaning, is that connectives are like names in this sense. 'Tonk' causes problems for someone who holds such a view about the meanings of the connectives. One problem is this: if the rules give 'tonk' its meaning, how can they be wrong? But if they are not wrong, how can it be bad to add them to our system? (Which, as you point out, it obviously is.) One interesting question now is, can local reduction, or normalisation, help us to answer that question? (And with that I'm off to read Greg's chapter.)

Hi Anna, thanks for the reference; I'll check it out.

This is sadly off-topic. I really need some magic software that remembers where I posted blog comments. I found this again prompted by Matt Carter who asked me about your blog, and I had clean forgotten. Then I was looking into "tonk" and the whole interesting conversation came flooding back! I think your blog is great, and thoroughly undeserving of my forgetfulness.

If you generate an RSS feed, I could add you to the MelbournePhilosophy daily news page. Let me know.

Hey, welcome back.

There are three feeds for this site (all for the main blog only, there is no comments feed.) My new feedreader (Sage in Firefox) will search the main page and find them automatically, but in case you can't find them, here are the urls:

http://www.logicandlanguage.net/index.rdf (RSS 1.0)
http://www.logicandlanguage.net/atom.xml (XML)
http://www.logicandlanguage.net/index.xml (RSS 2.0)

Let me know if you have any problems with these. I might put this information somewhere more obvious as well.