I-Style Natural Deduction System

The I-style natural deduction systems for K, D, and T include all inference rules of the classical natural deduction system. However, any rules involving boxes (i.e., the iteration rule and the /3 introduction rules) refer only to the type 1 boxes. Thus, we must develop some rules for type 2 boxes. The following is a complete list of the common rules for 1-style natural deduction K, D, and T systems:

1. Type 2 box creation rule: if a wff 7r(c) (resp. 7r÷(c)) occurs in the course of a deduction, a type 2 box with label c (resp. c ÷) may be created. The created box is at the same nest level as the occurrence of ~ ( c ) (resp. 7r+(c)), and 7r0(c) (resp. ~-~(c)) is put at the first line of the box.

2. Iteration rules for type 2 boxes: If B is a type 2 box with label c (c+), and S is the set of all wffs that occur above B and have the same nest level as B. Then any member of K÷(S, 1 - c)(K(S, 1 - c)) may be repeated directly inside B.

350 Churn Jung Liau and Bertrand I-Peng Lin

1. Iteration rule: in a deduction, if f and box B are at the same nest level and f occurs above B, then f may be repeated directly inside the box B.

2. Contradiction rules:

3. Elimination rules:

a elimination rules:

AE: f a g g f

- n ~ E :

f

~ f g

J_ -7 T

~ f f fl elimination rules:

VE: . ~ f -~g f V g f V g

g f

g g

V E : - ~ ( f v g ) ~ DE: - ~ ( f 3 g )

-~f f

~ g ~ g

~ A E : f g

- - ( f A g ) - . ( f A g )

~ g - ~ f

D E :

f ~ g

f D g f D g

g ~ f

4. Introduction rules:

a introduction rules:

A I : f g f a g

-~ v I : _~f ~ ~I: f

-~g -~g

- ~ ( f V g ) --7(fDg)

-.-71: f - 7 - ~ f

Figure 3. Natural deduction system for classical logic.

Proof Methods for Reasoning

/3 introduction rules (assumption discharging rules):

f v g f v g

-~ AI:

-~(f A g)

f D g f z g ~ f

Figure

3--Continued

-~(f ^ g) 351

3. Contradiction return rule: if I is derived in a type 2 box, the box may be closed off, and _1_ is returned outside.

4. Contradiction rules: our additional contradiction rules with respec- tively the premises -1 [0If, -1 (0>f, [1] +f, and (1 } +f are included.

Furthermore, we have special rules for the system D and T. The special rule for T is directly presented in Figure 4. The special rule for D is as follows: one may create a type 2 box labeled with 1 at any point of the deduction. For convenience, the first line of the so-created box is q-.

Schematically, these rules are presented in Figure 4.

The definition of deduction, proof, and global assumption rule is almost same as that for classical logic. However, we require a proof that is a deduction in which all boxes (type 1 or 2) have been closed. We use B ~-L' f to denote that f has a proof in the I-style system for L under the global assumption rule with set B. It is easy to construct the completeness of the I-style systems, so we consider it first.

THEOREM 5.1

Let B be a finite set of wffs and f be a wff. Then B ~L f implies B ~--L' f

Proof First, let F = S u b ( B U { f } , and O = { S c F I B ~ L ,

ASP_I_}.

We will verify that O is a B-compatible L-consistency property. Then, if B ~L' f, then { ~ f} ~ O. Otherwise, B ~-L' -~ f D _L, and by D E and the reverse rule, we have B ~-L' f after all. Thus, by model existence theorem

B ~ L f .

To verify that 0 is a B-compatible L-consistency property, we go through the following steps. First, the verification of conditions (a) and

352 Churn Jung Liau and Bertrand I-Peng Lin

1. Creation rules:

2. Iteration rules:

3. Return rule:

,r(c)(c > O)

,rr+(c)

C+: ~

f ~ K+(S, 1 - c ) ( c > O) f ~ K ( s , 1 - c)

C+:

4. Additional contradiction rules:

-~[0]f g 5. Special rules for T:

6. Special rule for D:

.1_

~ ( O ) f [ l ] + f (1)+f

g g g

v(c)(c > O) v+(c)

,-'o(C) ~,~-(c)

Figure 4. The I-style natural deduction rules for systems K, D, T.

Proof Methods for Reasoning 353

Furthermore, O is B-compatible because of the global assumption rule.

[]

354 Chum Jung Liau and Bertrand I-Peng Lin The soundness of I-style systems is intuitively obvious. However, to construct the formal result, we need some more definitions.

DEFINnnON 5.1 Given an 1-style deduction for the wff f under the global assumption B. We can define the set of assumptions alive at line n, A(n), for each line of the deduction as follows:

(i) A(O) = 0 .

(ii) if line n is a member of B or comes from a earlier lines by one of the iteration, contradiction, aI, aE, or BE rules, then A(n) = A(n - 1).

(iii) I f part of the proof looks like

( n ) 5 (n + 1)f2

(re)f3 (m + 1)f4

where (n) represents that the line number is n, then A(n + 1) = A(n) tO {f2} a n d A ( m + 1) = A(n).

(iv) if part of the proof looks like

(n)f~

c: (c+:) (n + 1)f2

(m)f3 (m + 1)f4 thenA(n + 1) = fDandA(m + 1) = A(n).

Note that in each box of a deduction, there are two kinds of assumptions alive. The first one is that induced by the creation of a type 1 box, and the second one is those imported from the outside. According to the definition above, when we enter a type 1 box, the two kinds of assumptions are both included in the set of alive assumptions. However, when we enter a type 2 box, all assumptions outside it are forgotten. Thus, the alive assumption set in fact depends on the world in which we are doing deduction.

Proof Methods for Reasoning 355 Furthermore, if line (n) and line (m) are at the same nest level, then A(n) = A ( m ) according to the definition.

In what follows, let L = K, D, or T, and B be a finite set of wffs which is used as the global assumption set of our deduction process.

LEMMA 5.3 (conditional validity lemma) Let P be a proof in 1-style natural deduction system with B as the global assumption set, and M = (W, R, TA) be a finite model in L such that ~M B. Then for each w E W, we have w ~ /x A(n) D f f o r any line (n)foccurring in P but not inside any type 2 boxes.

Proof We prove the lemma line by line through P inductively.

Induction basis: assume the first line of P is (1)f. Then it must be the cases that f ~ B or f is an assumption. If f ~ B , then w ~ M f since ~M B, so the result follows since A(1) = Q. If f is an assumption, then it is the first line of the outermost type 1 box, and by definition A(1) = {f}, so the result holds.

Induction step: assume that for all lines whose number k :g n and not inside any type 2 boxes, we have w ~M /x A ( k ) ~ f. To prove the result holds for line (n). Since line (n) is not in any type 2 box, there are four cases to be considered as follows:

1. if line ( n ) f is derived by one of the a introduction rules, a elimina- tion rules, /3 elimination rules, contradiction rules, type 1 iteration rule, or special rules for T from some premise lines ( m l ) f l and (m2)f2 (if the rule is one-premise rule, then only (m l) is needed), then by definition, A ( m i) c_ A(n)(i = 1, 2) where the containment is proper in the case of iteration rule. Since (n) is not inside any type 2 boxes, and (ml), (m 2) are either at the same nest level as (n) or is outside the type 1 box containing (n), then (ml), (m 2) are not inside any type 2 boxes, either. Thus, the induction hypothesis implies w k ~ / x A ( m i) 3 f i for i = 1,2, and this in turn implies w ~M A A (n) 3 f / for i = 1, 2. Now, we can check all the above-mentioned rules to see that w ~M f l /x f2 D f , so the result follows.

2. If ( n ) f is the first item of a type 1 box as follows:

( n - 1 ) f '

then A(n) = A(n - 1) U {f}, so w ~M /x A(n) Df.

356 Chum Jung Liau and Bertrand I-Peng Lin 3. if ( n ) f is derived by the /3 introduction (i.e. assumption discharging)

rules as follows:

(k + 1)f2

.

(n - 1)f3 ( n ) f

then by induction hypothesis, w ~M ^ A ( n ) ^ f2 ~ f3 since A ( n - 1) = A ( k + 1) = A ( k ) U {7"2} = A ( n ) u {f2}. Note that these equa- tions are derived from the facts that (k) and (n) are at the same nest level, and (k + 1) is the first line of a type 1 box while (n - 1) is the last line of the same box. Thus, w ~M A A ( n ) ~ (-~ f2 V f3). This implies the result since all assumption discharging rules have the form so that f = -~ f2 v f3 is valid in classical logic.

if (n) I is returned from a type 2 box as follows: (the c + case is similar)

(i)~r(c)

c: (k + 1)Tr0(c)

(n - 1) ± (n) &

Note that the last line of a type 2 box must be ± since the only return rule for it is the contradiction return rule. We will show that w g:M /x A(k).

This in turn implies w ~M A A ( n ) D _1_ since A ( k ) = A ( n ) . Assume w ~M A A(k), and let the type 2 box under consideration be B. Then by induction hypothesis, we have w ~M A A ( k ) ~ w(c) since (i) and (k) are at the same nest level. Thus w ~M 7r(c). Since M is a finite model, we can find a world w' such that R(w, w') > c and w' ~ ar0(c). This also implies w' ~M A A ( k + 1) ~ zr0(c). Now, we can consider the box B as an inde- pendent deduction process except that the type 2 iteration rules may import wffs into it. Thus, we can restart the proof of the lemma from the first line of B recursively to prove that w' ~M A A ( j ) ~ f for each line ( j ) f in B but not inside any other type 2 boxes except those lines imported

Proof Methods for Reasoning 357 by the type 2 iteration rules. However, if line ( j ) f is imported from the outside of B, then f ~ K+(S, 1 - c), where S is the set of all wffs above B and at the same nest level as it. Since w ~M A A ( k ) and all wffs in S are at the same nest level as line (k), we have w ~M S by induction hypothe- sis. This in turn implies w' ~M f. Thus w' ~M A A ( j ) 3 f for each line ( j ) f in B but not inside any other type 2 boxes. In particular, w' ~M /x A ( n - 1) ~ 1 . However, A(n - 1) ---A(k + 1) = • since all assumption introduced in B have been discharged before line (n - 1), so w' ~M ± 4 This is a contradiction, thus the assumption that w ~M /x A ( k ) is false.

That is, w ~M A A(k). []

According to the lemma, we can construct the soundness result.

THEOREM 5.2 Let B be a set of wffs and f be a wff. Then B ~-i2 f implies

B ~ L f .

Proof By the preceding lemma, in particular, consider the last line of the proof. Assume ( n ) f is the last line of the proof B ~-L' f , since in a natural deduction proof for the I-style system, all boxes have been closed, line (n) does not occur in any type 2 boxes, and since all assumptions have be en discharged, A ( n ) = Q, we have B ~VL f by the preceding Lemma.

Then the desired result follows from Corollary 3.1. []