We introduce a natural deduction calculus for the GodelDummett Logic LC semantically characterized by linearly ordered Kripke models. Our calculus is inspired by an analogous calculus for Intuitionistic logic (IPL) internalizing mechanisms to reduce the proof-search space that has been used to de ne a goal-oriented proof-search procedure for IPL. In this paper we present the calculus for LC and we sketch its soundness and completeness.
Introduction (blocked) or u (unblocked), and #-sequents ) H #. In proof-search, a derivation for an "-sequent is built by trying the bottom-up application of a rule of the calculus to . The label b blocks the applications of some rules, so to reduce the search-space; for instance, if = ) A _ B "l and l = u, then we can bottom-up apply either rule _I0, yielding ) A "u or _I1, yielding ) B "u, and continue bottom-up expansion with the obtained sequents. In contrast, if l = b then the application of rules _I0 and _I1 is blocked, thus the sequent is not provable and one has to backtrack. A formula G is valid in IPL if and only if there exists a derivation D of the sequent ) G "u (with empty context); a crucial point is that D is isomorphic to a derivation in normal form in the standard deduction calculus for IPL.
In this paper we investigate the application of the method to LC; we introduce a natural deduction calculus for LC close to Nbu so that proof-search can be e ciently implemented. The idea is to enhance Nbu by adding a rule to capture the characteristic axiom (A B) _ (B A) of LC. A natural candidate is the rule below, a sort of _E elimination rule where the main premise ) (A B) _ (B A) # has been crossed out, since in LC is redundant:
A
B; ) C "u ) C "u
B
A; ) C "u
Gd
Seemingly, this rule yields a non-e ective proof-search strategy, since the rule
must be applied bottom-up and the formulas A B and B A in the premises
are arbitrary. We can bound proof-search by exploiting [
Goedel-Dummett logic LC
We consider the language based on a denumerable set of propositional variables
V, the connectives ^, _, , and the logical constant ?; :A stands for A ?. By
Sf(G) we denote the set of all subformulas of G (including G itself); Sf!(G) is
the set of C 2 Sf(G) such that C 2 V or C = A B. Let `L G denote that the
formula G is provable in the logic L from the assumptions in . By de nition,
`LC G i gd `IPL G, where gd is the (in nite) set of all the instances of the
axiom-schema (Gd) = (A B) _ (B A) (see e.g. [
B) _ (B
A) j fA; Bg
Sf!(G) g Namely (a simpli ed proof of the theorem is discussed in Appendix A):
gd(G) `IPL G.
tu ) A
B # ) B # ) A _ B # The natural deduction calculi we consider in this section act on sequents of the form ) where , the context, is a nite, possibly empty, multiset of formulas and has the form H # or H "l, with H any formula and l 2 fb; ug. For calculi and derivations we use the de nitions and notations of [14]. In particular, applications of rules of a calculus C are depicted as trees with sequents as nodes. A derivation of C is a tree where every leaf is an axiom sequent, i.e., a sequent obtained by instantiating a zero-premise rule of C. When needed, we write Ctree and C-derivation to emphasize the calculus at hand. A sequent is provable in C, and we write C ` , if there exists a C-derivation with root sequent .
The calculus NLC(G) is displayed in Fig. 1. It consists of introduction (I)
and elimination (E) rules for every logical connective plus the coercion rule (#"),
the ? elimination rule (?E), and assumption introduction rule (Id). The major
formula of an elimination rule is the formula with the characteristic connective
and the major premise is the sequent having the major formula in the
righthand side; e.g., in the rule E the major formula is A B and the major
premise is ) A B #. The calculus NLC(G), parametrized by the goal
formula G to be proved, is a variant of the natural deduction calculus Nbu for
IPL presented in [
) G "u implies `LC G.
In the rest of this section we sketch completeness of NLC(G), i.e., the converse of Th. 2. We provide an example of derivation (another example is at the end of Appendix B).
Example 1. Let G be the formula (p _ q) $ ((p q) q) ^ ((q p) p) (with $ de ned as usual). We prove that G is valid in LC by showing an NLC(G)derivation of ) G "u. tu A = (p q) q
B = (q p) p
C = A ^ B
D = p _ q
D1 D2 D ) A "u D ) B "u
D ) C "u ) D C "u I2 ^I
p ) D $ C "u
D3 q; C ) D "u q
C ) D "u ) C D "u
D4 p; C ) D "u
I2 ^I
Gd Below we detail the NLC(G)-derivations D1 and D3 (D2 and D4 are similar). p q; D ) D # p p
Id
p q; D ) q # q; D ) q "u #" D ) A "u
I2 q; D ) p q #
Id _E1 p p q; C ) C # q; C ) (p q)
Id q # p; p q; C ) p
q # p; p p; p p
p; p Id p; p q; C ) q # q; C ) q "b #" q; C ) p q "b q; C ) p # q; C ) p "b #"
Id I2 E ^E0 p p p q; C ) q # q; C ) q "b #" q; C ) D "u _I1 3 Actually, one could introduce _ as a de ned operator and drop out its I/E-rules. Nbu = NLC(G) n fGd; _E0; _E1g [ f_Eg NLC (G) = NLC(G) n fGdg [ fGd g
NLC_(G) = NLC (G) [ f_Eg ) A _ B # A;
) D "u B; ) D "u
Let us assume `LC G. By Th. 1, it holds that gd(G) `IPL G; by Th. 3, there exists an Nbu-derivation D of the sequent gd(G) ) G "u. We show that D can be turned into an NLC(G)-derivation of ) G "u. The translation requires some non-trivial steps; to handily describe them, we introduce the auxiliary calculi NLC (G) and NLC_(G) (see Fig. 2). We point out that NLC (G) is obtained by replacing in NLC(G) the rule Gd with the more liberal rule Gd ; NLC_(G) is obtained by adding the rule _E to NLC (G). Let Sf (G) = Sf(G) [ f A
B j fA; Bg
Sf!(G) or A _ B 2 Sf(G) g NLC_(G) enjoys the following extended version of subformula property: Theorem 4. Let D be an NLC_(G)-derivation of a sequent occurring in D. Then:
Given h 2 fb; ug, by h we denote the partial function mapping an NLC_(G)tsreeqeueTntwith)roCo"ths.eWquheennt de)neCd,"l h(l(T2)fibs;oubgt)atinoeadnbNypLoCss_i(bGly)-cthraeengwinitghsroomoet of the labels l in the bottom part of T with h. The de nition of h(T ) is displayed in Fig. 3. The following properties can be easily checked: (P1) if D is an NLC_(G)-derivation of ) C "l, then
derivation of ) C "u. (P2) if D is an NLC (G)-derivation of ) C "l and h 2 fb; ug, then an NLC (G)-derivation of ) C "h. u(D) is an NLC_(G)
h(D) is ) A ^ B "l
T1 ) B "l ) A
T2 A;
B;
T1 Let T be an NLC_(G)-tree with root sequent C; ) . By C (T ) we denote the NLC_(G)-tree obtained by deleting an occurrence of C from the left contexts of the sequents in T , with some caution with rule I1. Formally: 0
C;
) C C; C
T1 ) B "l T1 C; One can easily check that the map C is well-de ned (note that in its de nition the map h is only used with h set to u). We remark that, if D is an NLC (G)derivation, the tree C (D) might not be an NLC_(G)-derivation. For inst_ance, lreetpluasceadssbuymtehtehoapteDn lceoanftain)s aCle#a.fWeC c=anCp;rov)etCha#t,: with C 62 ; then, C is
+ Let T be an NLC (G)-tree with root sequent ) and C a formula. By C (D) we denote the NLC (G)-tree with root sequent C; ) obtained by adding an occurrence of C to the left contexts of T , with some caution with rule I2, namely: + C
A;
T1 ) B "u ) A
T1 B; T1 ) D "u B
) D "l ) "
Tn l
R
A;
C;
C; 1
C; GdAC = C; ) " l(T1) It is easy to check that if D is an NLC (G)-derivation of ) , then itsheancoNmLpCosi(tGe)m-daeprivaC+t1ion of C; C+n )(nam(seeley,(wPe2)a)d.dFoarll th=e ffoCrm1; u:l:a:s; Cinng, + C (D)
+ is ).
Lemma 2. NLC_(G) ` ) H "u implies NLC (G) ` ) H "u.
Proof. Let D be an NLC_(G)-derivation of ) H "u. We show that we can eliminate all the applications of rule _E. Let us consider a subderivation D0 of D of the form
D0 ) A _ B #
A;
D1 ) D "u ) D "u
B;
D2 ) D "u _E
A 62 ; B 62 where D0, D1 and D2 do not contain applications of _E, hence D0, D1 and D2 are NLC (G)-derivations. We show that we can replace D0 with an NLC (G)derivation G of ) D "u. Let us assume B A 2 and let us consider the NLC (G)-tree A(D1) having root sequent ) D "u. Note that A(D1) might contain open leaves of the form A = ; ) A #. We can replace A with the NLC (G)-derivation ; + (D0) ) A _ B #
A = ; ; ) B ) A #
A #
Id _E0 After such replacements, we get an NLC (G)-derivation G of ) D "u. The case A B 2 is symmetric. Finally, let us assume A B 62 and B A 62 . Proceeding as in the previous cases, starting from the NLC (G)-tree siA+milBar(lyB,(frDo2m)) wB+e cAa(n bAu(iDld1)a)nwNe LcCan (bGu)i-ldderNivLatCion(GE)1-doefriAvatioBn; E2 )of DB"u; A; ) D "u. We can replace D0 with the NLC (G)-derivation
A
B;
E1 Note that the displayed application of rule Gd is sound since ) A _ B # occurs in D hence, by Theorem 4(iii), A _ B 2 Sf(G). By repeatedly applying such replacements, we cross out all the applications of _E and we eventually get an NLC (G)-derivation of ) H "u. tu
By applying standard permutation steps, consisting in moving down the applications of Gd , so that the conclusion can be labelled by u, we get: Lemma 3. NLC (G) ` ) G "u implies NLC(G) `
To conclude, in this short paper we present the calculus NLC(G) and we
show that it is sound and complete for LC. We plan to design a proof-search
strategy for NLC(G), similar to the one developed for Nbu in [
Logica, 60(1):67{106, 1998. 13. W. Sieg and S. Cittadini. Normal natural deduction proofs (in non-classical logics). In D. Hutter and W. Stephan, editors, Mechanizing Mathematical Reasoning, volume 2605 of LNCS, pages 169{191. Springer, 2005. 14. A.S. Troelstra and H. Schwichtenberg. Basic Proof Theory, volume 43 of Cambridge Tracts in Theoretical Computer Science. Camb. Univ. Press, 2ed edition, 2000.
Kripke semantics and proof of Theorem 1
In this section we provide a semantic proof of Theorem 1 inspired from [
A ^ B i K; A and K; B; A _ B i K; A or K; B; A B i , for every 2 W such that , K; 1 A or K;
B.
Let be a set of formulas. By K; we mean that K;
A 2 . A formula A is valid in a model K i K; A for every
well-known that (see e.g. [
We introduce a ltration technique on Kripke models based on quotientation
[
G G i , for every A 2 Sf!(G), K; i G and G .
A implies K;
A; Note that implies G , while the converse might not hold. We point out that G is an equivalence relation on W ; by [ ] we denote the G-equivalence class containing . The quotient model K=G = hW 0; 0; 0; V 0i is de ned as follows: { W 0 is the set of equivalence classes generated by { [ ] 0 [ ] i G ; { V 0([ ]) = V ( ) \ Sf!(G).
G and 0 = [ ]; One can easily check that K=G is a well-de ned Kripke model. In particular: 0 is the minimum element of K=G and [ ] 0 [ ] implies V ([ ]) V ([ ]). In the next lemma we prove that quotientation with respect to G preserves the forcing of subformulas of G; moreover if all the formulas in gd(G) are valid in K, then K=G is linear.
Lemma 4. Let K = hW; ; ; V i be a Kripke model and let G be a formula. (i) For every (ii) If K;
2 W and C 2 Sf(G), K; C i gd(G), then K=G is a linear model.
K=G; [ ]
C.
Proof. Let K=G = hW 0; 0; 0; V 0i. The proof of (i) goes by induction on the structure of C. We only discuss the case C = A B the other being trivial. Let K; 1 A B. Then, there exists 2 W such that , K; A and K; 1 B. By induction hypothesis, K0; [ ] A and K0; [ ] 1 B. Since , we get [ ] 0 [ ], and this proves that K0; [ ] 1 A B. Conversely, let K0; [ ] 1 A B. Then, there exists 2 W such that [ ] 0 [ ], K0; [ ] A and K0; [ ] 1 B. By induction hypothesis, we get K; A and K; 1 B, which implies K; 1 A B. Since A B 2 Sf!(G) and G , we conclude K; 1 A B.
(ii) Let K; gd(G) and let us assume, by absurd, that K0 is not a linear model. Then, there exist two worlds and of K such that [ ]6 0[ ] and [ ]6 0[ ], namely 6 G and 6 G . This implies that there is A 2 Sf!(G) such that K; A and K; 1 A and B 2 Sf!(G) such that K; B and K; 1 B. It follows that K; 1 D, where D = (A B)_(B A). This yields a contradiction, since D 2 gd(G) and K; gd(G); we conclude that K0 is linear. tu Given a logic L, by j=L A we mean that A is a logical consequence of namely: for every L-model K and every world of K, if K; then K; in L,
A.
Lemma 5. j=LC G i
gd(G) j=IPL G.
Proof. Let us assume 6j=LCG. Then, there exists a linear Kripke model K and a world in K such that K; 1 G. Since all the formulas in gd(G) are valid in K, we conclude gd(G)6j=IPLG. Conversely, let us assume, gd(G)6j=IPLG. Then, there exists a Kripke model K and a world in K such that K; gd(G) and K; 1 G. By Lemma 4, K=G is an LC-model (Point (ii)) such that K=G; [ ] 1 G (Point (i)), and this implies 6j=LCG. tu
By Lemma 5 and the fact that logical consequence relation j=L and provability relations `L coincide, with L 2 fIPL; LCg, Theorem 1 follows. B
Proof of the main results of Section 3 Given a formula G, the set Sf+(G) of strictly positive subformulas of G (see [14]) is the smallest set of formulas such that: - G 2 Sf+(G); - A B 2 Sf+(G), with 2 f^; _g, implies A 2 Sf+(G) and B 2 Sf+(G); - A B 2 Sf+(G) implies B 2 Sf+(G).
Given a multiset of formulas , the set Sf+( ) is the union of the sets Sf +(G), for every G 2 . By induction on the depth of NLC_(G)-derivations, one can easily prove that: Lemma 6. NLC_(G) `
) C # implies C 2 Sf+( ). ) G "u and let ) tu be Proof. By induction on the depth of = ) , namely the distance between and the root sequent r = ) G "u of D. In the base case = r and points (i) and (ii) trivially hold. Let 6= r. Then, is the assumption of the application aofssau mruelethRatof 0NsLaCtis_(eGs);pboiynts0 (wi)e{(diiein).otWe ethperoccoenecdlubsiyona ocfaRse. aBnyalIyHsi,swoencRan, only detailing some signi cant cases.
R = #" R = ?E
=
By IH, Sf (G), hence (i) holds. Since NLC_(G) ` , by Lemma 6 we get ? 2 Sf+( ). It follows that ? 2 Sf (G), and this proves (iii).
R = ^I
R = ^Ek = By IH, Sf (G), hence (i) holds. Since NLC_(G) ` , by Lemma 6 we get A0 ^ A1 2 Sf+( ). It follows that A0 ^ A1 2 Sf (G), hence (iii) holds.
R =
E 1 = ) A
B # 0 = ) B # = By IH, Sf (G), hence (i) holds. Since NLC_(G) ` 1, by Lemma 6 we get A B 2 Sf+( ), hence A B 2 Sf (G). This implies that A B 2 Sf(G) or fA; Bg Sf!(G) or A _ B 2 Sf(G). In either case A 2 Sf(G), hence (ii) holds.
R =
I2
= A; 0 =
The following lemma states a su cient condition to guarantee that is an NLC_(G)-derivation: C (D) Lemma A.1. Let D be an NLC_(G)-derivation of C; ) and let us assume that D does not contain applications of rule Id with main formula C. Then,
C (D) is an NLC_(G)-derivation of ) .
Proof. By induction on the depth of D. Note that, in the base case, D only consists of the sequent C; ) A # and, by hypothesis, A 6= C, hence A 2 . This implies that C (D) = ) A # is an NLC_(G)-derivation. tu
Proof. Let D be an Nbu-derivation of gd(G) ) G "u; note that D is an NLC_(G)-derivation as well. We can eliminate from D all the applications of rule Id having main formulas in gd(G) as follows. Let = ) C # be the conclusion of an application of rule Id with C 2 gd(G), and let us assume C = (A B) _ (B A) where fA; Bg Sf!(G). Then, must be the major premise of an application of rule _E with conclusion 0 = ) D "u. Let D0 be the subderivation of D with root sequent 0 de ned as: = ) C #
Id
A
B; 0 =
D1 ) D "u ) D "u
D2 B
A; We can replace D0 with the NLC_(G)-derivation
D1 A
B;
We conclude this section with a further example of NLC(G)-derivation. Example 2. Let G = :p _ ::p; an NLC(G)-derivation of G is (recall that :A stands for A ?): ::p p; ::p p; ::p ::p
D1 :p ) ? # :p ) ? " I2 :p ) :p "b :p ) :p _ ::p "u _I0 b ?E :p; :p :p; :p :p
D2 ::p ) ? # ::p ) ? " I2 ::p ) ::p "b ::p ) :p _ ::p "u _I1
Gd b ?E :p ) :p _ ::p "u and D2 is similar.
p; A ) :p#
:p; p; A ) p# Id :p; p; A ) :p# Id :p; p; A ) p"b :p; p; A ) ?# :p; p; A ) ?"u ?E p; A ) ::p"b EI2 pp;;AA))pp"#b I#d"