logicandlanguage.net

« Gödel in the New Yorker | Main | How to put proof trees in weblog entries »

March 23, 2005

Normalisation/local reduction (Ch2 of Proof & Counterexample)

In a previous post I discussed A.N. Prior's 'tonk' connective and local reduction, and lots of smart people left comments, or discussed the issue on their own blogs. Greg Restall, in particular, pointed me to chapter two of the proof theory book he is writing. Greg's book project is likely to be particularly interesting to e-philosophers (that's you), because he is posting it online as a Wiki as he writes it, and inviting participation and comments.

Anyway, I have now read chapter two, and I thought I would write a little about what I have learned, as a follow-up to the Tonk post, and perhaps as a prelude to some more philosophical posts on 'tonk', the truth predicate and meaning.

1. First of all, I have been reminded of the tree method of writing natural deduction proofs, which I haven't really thought about since I first read Gentzen. Simple tree diagrams are pretty easy to read. Here is one:

The formula on the bottom line is our conclusion, any formula which does not have a horizontal line above it is a premise. The line above a formula tells us how it was derived; when we want to derive something from (say) two formulas, we draw a single horizontal line under them both and write the derived formula under that line. In the simple tree above, C is the conclusion, A→(B→C) and A, and B are all premises, and B→C is an intermediate step, derived from A→(B→C) and A using the rule of [→E]. Here is a simple proof in which premises get discharged:

In this case we have assumed A at the beginning, then discharged it using [→I] on the second line. We indicate that a premise has been discharged by drawing a line above it and writing the number of the step where it was discharged next to that line (number assignment is arbitrary; it is just a way of matching up discharged premises with the places where they were discharged. The orderly-minded will, no doubt, wish to start at 1 and move up through the natural numbers, and the rest of us should refrain from alarming our readers by following suit.) Finally we use [→I] again to get the conclusion A→(A→A). It's worth noting here that in this case we have 'discharged' a premise we never assumed. Some logics take a dim view of this kind of thing, as we shall see...but first, a less simple example of a proof, for you to look on in awe:

2. Different logics have different policies about what kinds of premise-discharging are allowed. At the most liberal end, we have standard logics (including classical logic.) They are liberal in two degrees; they allow vacuous premise discharges (as in the last step of the second proof above) and they allow more than one premise to be discharged at once, like in the last line of this proof:

If we allow more than one premise to be discharged at once, but do not allow vacuous discharging, then the result is a relevant logic. The second proof above is thus not relevantly acceptable, since it uses vacuous discharge in the last step. If we allow neither vacuous discharge nor duplicate discharge, the result is a linear logic (important to computer scientists, I believe) and if we allow vacuous but not duplicate discharging, the resulting logic is affine. Affine logics include, but are not exhausted by, intuitionistic logics.

We are dealing with logics quite generally here, independently of questions about which is the "one true logic," so we want to be able to talk sensibly about all of them. If we are going to talk about logics which do not allow multiple discharges, it is no use thinking of the premises, or premises and assumptions in force at any particular step, as a set. These logics care about whether there are two occurrences, or merely one occurrence, of A in the premises and assumptions, but the set {A, A, B, C} is the same set as {A, B, C}. So we think of our premises as forming a multiset, which is a bit like a set, except that elements can be members more than once, so that "A, A, B, C" is a different multiset from "A, B, C" (disappointingly, multisets don't come with any cool bracket notation, we just write them out as lists in quotation marks.)

In this chapter we are restricted to logics with just two rules: [→I] and [→E]. This is because Greg is attempting to keep his treatment of normalisation simple (he believes that the basic idea is simple and that you shouldn't have to be a mathematician to grasp it.) Check out his introduction for more about the goals of the book.

3. Methodology: in a sense, it is easy to demonstrate that there is a proof of some formula or argument; we just exhibit the proof. Without resorting to model theory, it is trickier to show that there is no proof of something. It turns out that one way to do it is to show that there is no normal proof from the premises to the conclusion, since i) it is often easier to show that there is no normal proof than it is to show directly that there is no proof at all and ii) it turns out that if there is a proof, there is a normal proof. The climax of the chapter is the proof of that last conditional. I am not going to go through the proofs here - this is just an explanation and summary of the results. There are two main results, the subformula theorem, and the normalisation theorem.

5. Normal Proofs: a proof is normal iff the concluding formula A→B of an [→I] step is not at the same time the major premise of an [→E] step.

In the schematic proof on the left below, the formula A→B is both the conclusion of an [→I]-step and the major premise of a [→E]-step. For now I will call such pairs "non-normal pairs" (Greg calls them critical pairs, but from the discussion with Aaron Stump on the website (scroll down to see it) it seems as if he no longer likes this terminology.) We can take non-normal pairs out by rewriting the proof as in the schematic proof on the right:

When we generalise the definition of "normal proof" to cover the other connectives, it seems that the 'tonk' proof that I was interested in here is bound to count as non-normal:

6. The Subformula Theorem: normal proofs satisfy the Subformula Theorem: if π is a normal proof from premises X to conclusion A, every formula in π is in sf(X,A), where sf(X,A) is the set of subformulas of X and A. Non-normal proofs do not, in general, satisfy the subformula theorem, as this example shows:

Here the formula A→A is a subformula of neither the premise, nor the conclusion. Clearly the inference with 'tonk' would not satisfy a generalised version of the subformula theorem either, since it contains formulas which are not in sf(P, Q), namely 'P tonk Q.'

And, finally

7. The Normalisation Theorem: if there is a proof π from X to A, there is a normal proof π' from X' to A.

• If π is linear, so is π' and X=X'.
• If π is affine, so is π' and X' is a submultiset of X.
• If π is relevant, then so is π', and X' is a modest super-multiset of X containing more repeats.
• If π is standard, then so is π', and X' is a variant of X found by possibly deleting some elements from X and duplicating others.

X' is a submultiset of X iff whenever a is an n-fold member of X, a is an m-fold member of X for m less than or equal to n. (m may be zero.)

e.g. "A,A,B,C" is a submultiset of "A,A,B,B,C,D"

X' is a modest supermultiset of X if whenever a is an n-fold member of X for some n>0, then a is an m-fold member of of X' for some m greater than or equal to n and whenever a is a member of X' to some non-zero degree, it is also a member of X.

e.g. "A,A,A,B,C" is a modest super multiset of "A,B,C"

The normalisation theorem turns out to be easy to prove in the linear and affine cases (where there are no duplicate discharges), and a bit harder to prove in general. The basic idea in the easy case is that you take the non-normal proof, and remove the non-normal pairs one at a time, using the method outlined in 5 above. Proofs have a finite length, and the proof gets shorter each time a pair is removed, so eventually there will be no more pairs to remove. The result is a normal proof.

But if we allow duplicate discharges, as we do in standard and relevant logics, the proof might not get smaller when we remove a non-normal pair, since we may be writing the proof of A many times, in place of every time we assumed A. In these cases, how can we know that the process of normalisation will come to an end?

Complexity: the complexity of a formula is the number of connectives it contains.

(In order to make the following definition readable on the web, sequences are written within parentheses (curved brackets.) This is not the correct notation and I am looking for a better alternative.)

Non-Normality: the measure of non-normality of a proof is a sequence (c1, c2,..., cn) of numbers such that ci is the number of critical pairs of formulas of complexity i. The sequence for a proof stops at the last non-zero value. Sequences are ordered with their last number as most significant, that is (c1,...cn) > (d1,...dm) iff n>m, or if n=m, when cn>dn, or if cn=dn, when (c1,...cn-1) > ( d1,...dn-1).

Lemma - Non Normality reduction: given a proof π with some critical pair π reduces to π' with a lower measure of non-normality.

So even though you might not have fewer non-normal pairs, when you take one of them out, you will have a proof with a lower non-normality measure. Keep going, and eventually the process will return a normal proof. Thus every proof can be transformed into a normal proof.

Caveat: as the detail of the normalisation theorem makes clear, except in the linear case, the normal proof will not necessarily proceed from the same multiset of premises as the original.

Posted by logican at March 23, 2005 03:22 PM

Trackback Pings

The trackback address for this entry is:
http://www.logicandlanguage.net/trakbak.cgi/16

Listed below are links to weblogs that reference Normalisation/local reduction (Ch2 of Proof & Counterexample):

» Intelim Rules for Truth and Names from Opiniatrety
(If you didn't fall asleep during the post title, I'm taking that as license to be as technical as I wanna be.) Gillian Russell considers the possibility that the truth predicate is like 'tonk' in that introducing it into the... [Read More]

Tracked on April 5, 2005 04:37 PM

Comments

Posted by: Nick Smith at March 26, 2005 04:58 AM

Posted by: Gillian Russell at March 26, 2005 11:57 AM

Post a comment

Name:

Email Address:

URL:
Remember Me? YesNo

Comments: (you may use HTML tags for style)