Proof-search in Hilbert calculi

Abstract

It is well-known [7] that the standard formalizations of classical and intuitionistic logic based on Hilbert calculi, sequent calculi and natural deduction are equivalent. In spite of this, proof-search has been mainly developed around the notion of sequent calculi almost neglecting the cases of natural deduction and Hilbert calculi. This is primarily motivated by the fact that the latters lack the \deep symmetries" of sequent calculi which can be immediately exploited to control and reduce the search space (see, e.g., [2,3,6] for an accurate discussion). However, as we have shown in [3], in the case of natural deduction it is possible to design proof-search procedures with structural properties and complexity comparable with those based on sequent calculi. In this paper we begin an analogous investigation concerning Hilbert calculi. In particular, we consider the f!; :g-fragment of the Hilbert calculus for Classical Propositional Logic de ned in [5] and we describe a terminating proof-search procedure for it. We consider the propositional language L of Classical Propositional Logic (CPL) based on a denumerable set of propositional variables V and the connectives ! and :. The logical connectives ^ and _ can be introduced by setting A ^ B = :(A ! :B) and A _ B = :A ! B. A literal is a formula of the form p or :p with p 2 V; the set of literals is denoted by Lit. We call Hc the Hilbert calculus for CPL introduced by Kleene in [5]. Logical axioms of Hc are:

-

(Ax1) (Ax2) (Ax3) (Ax4)

A ! (B ! A) (A ! B) ! ((A ! (B ! C)) ! (A ! C)) (A ! B) ! ((A ! :B) ! :A) ::A ! A The only rule of Hc is MP (Modus Ponens ): from A ! B and A infer B. Let be a set of formulas and A a formula. A deduction of A from assumptions is a nite sequence of formulas hA1; : : : ; Ani such that An = A and, for every Ai in the sequence, one of the following conditions holds: (a) Ai 2 (namely, Ai is an assumption); (b) Ai is an instance of a logical axiom; (c) Ai is obtained by applying MP to Aj and Ak, with j < i and k < i. ( 1 ) DMP(A ! B; A) : A ! B; A ` B; ( 2 ) D::E(A) : ::A ` A; ( 3 ) DEF(A; B) : A; :A ` B; ( 4 ) DEF!(A; K) : :A ! K; :A ! :K ` A; ( 5 ) DEF!:(A; K) : A ! K; A ! :K ` :A. tu By D : ` A we mean that D is a deduction of A from assumptions . By Fm(D) we denote the set of formulas occurring in the sequence D. In the following proposition we introduce some deductions: Proposition 1. For every formula A, B and K, the following deductions can be constructed: Let D and E be two deductions, where E = hA1; : : : ; Ani. The concatenation of D and E, denoted by D E, is de ned as follows: { let E0 be obtained by removing from E the formulas Aj such that 1 j < n and Aj is in D; then, D E is the concatenation of the sequences D and E0. One can easily check that: Lemma 1. Let D : ` A and E : ` B. Then, D E : [ ( n Fm(D)) ` B and Fm(D E) = Fm(D) [ Fm(E). tu A distinguishing feature of Hilbert calculi is that there are no rules to close assumptions. Thus, to prove the Deduction Lemma we have to rearrange a deduction D of A; ` B, as shown in next lemma.

Lemma 2 (Deduction Lemma). Let D : A; ` B. Then, there exists a deduction EDL(D) : ` A ! B such that, for every C 2 Fm(D), A ! C 2 Fm(EDL(D)). tu

In the next lemma we introduce the deductions E:E(D) and EI:(D). Lemma 3.

(i) Let D : :A;

E:E(D) : (ii) Let D : A;

EI:(D) :

` K such that :K 2 Fm(D). Then, there exists a deduction ` A.

` K such that :K 2 Fm(D). Then, there exists a deduction ` :A.

Proof. We prove Point (i). By the Deduction Lemma, there exists a deduction EDL(D) : ` :A ! K such that :A ! :K 2 Fm(D). Let us consider the derivation DEF!(A; K) : :A ! K; :A ! :K ` A de ned in Proposition 1.( 4 ). We can set E:E(D) = EDL(D) DEF!(A; K) which, by Lemma 1, is a deduction of ` A. The de nition of the deduction EI:(D) of Point (ii) is similar using DEF!:(A; K) instead of DEF!(A; K). tu

A (classical) interpretation I is a subset of V; the validity of a formula A in I, denoted by I j= A, is de ned as usual. Given a set of formulas , I is a model of , denoted by I j= , i I j= C, for every C 2 . A set of literals is consistent if it does not contain a complementary pair of literals fp; :pg. Given a consistent set of literals , the interpretation \ V is a model of .

The procedure Hp

We present the procedure Hp to search for a deduction in Hc. Let be a set of formulas, let A be a formula or the special symbol ?. We de ne the procedure Hp satisfying the following properties: (H1) If A 2 L, Hp( ; A) returns either a deduction D :

[ f:Ag. (H2) Hp( ; ?) returns either a deduction D : or a model of .

` A or a model of ` K such that :K 2 Fm(D) In Proposition 2 we prove that Hp is correct, namely, properties (H1) and (H2) hold. The procedure is presented in Fig. 1. In the presentation of Hp, we use a high-level formalism, discarding inessential details. The computation of Hp( ; A) is de ned by cases on and A. The rst case among ( 1 ){(9) matching the values of and A is executed; if none of the conditions in ( 1 ){(9) holds, case (10) is performed. We implicitly assume that the recursive calls are correct.

The rest of this section is devoted to the proof of correctness of Hp. Given a formula A, we denote by V(A) the set of propositional variables occurring in A and by jAj the number of symbols occurring in A. Given a nite set of formulas, we set:

V( ) = [ V(A) A2 j j = X jAj

A2

Lit( ) = \ Lit Let 1 and 2 be two nite sets of formulas and let A1 and A2 be either formulas or ?. We de ne the ordering relation ( 1; A1) ( 2; A2) i the following conditions hold (where j?j = 1): ( 1 ) V( 1 [ fA1g) V( 2 [ fA2g); ( 2 ) either Lit( 1 ) ) Lit( 2 ) or Lit( 1 ) = Lit( 2 ) and j 1j + jA1j < j 2j + jA2j. One can easily prove that is well-founded, namely: every -chain of the form ( 2; A2) ( 1; A1) ( 0; A0) has nite length. Indeed, by Point ( 1 ) of the de nition of , along a -chain no new propositional variable is added, hence we cannot apply Point ( 2 ) in nitely many times. In particular, the length of every chain starting with ( ; A) (and hence the number of nested recursive calls of Hp) is bounded by O(j j + jAj).

Proposition 2 (Correctness of Hp). The procedure Hp is correct. Proof. Let us consider the call Hp( ; A). We have to prove that Hp( ; A) satis es properties (H1) and (H2). One can easily check that every recursive call Hp( 0; A0) performed in the computation of Hp( ; A) satis es ( 0; A0) ( ; A). In particular, note that no new variables are added, hence V( 0 [ fA0g) V( [ fAg); moreover, literals are never deleted from the set of assumptions, hence Lit( 0) Lit( ). Since the relation is well-founded, we can assume by ( 1 ) If A is an instance of a logical axiom or A 2 .

Return the deduction only consisting of A. ( 2 ) If there exists B such that fB; :Bg .

If A = ?, return the deduction h:B; Bi : ` B.

If A 6= ?, return the deduction DEF(B; A) : ` A. ( 3 ) If there exists B ! C such that fB ! C; Bg .

Let D1 = Hp( ( n fB ! Cg) [ fCg ; A).

If D1 is an interpretation, then return D1.

Otherwise, return the deduction DMP(B ! C; B) D1 : ` A. ( 4 ) If there exists B such that ::B 2

Let D1 = Hp( ( n f::Bg) [ fBg ; A).

If D1 is an interpretation, then return D1.

Otherwise, return the deduction D::E(B) D1 : ` A. ( 5 ) If A = p with p 2 V and :p 62 .

Let D1 = Hp( [ f:pg; ?).

If D1 is an interpretation, then return D1.

Otherwise, D1 is a deduction of :p; ` K with :K 2 Fm(D1); return the deduction E:E(D1) : ` p. ( 6 ) If A = B ! C.

Let D1 = Hp( [ fBg; C).

If D1 is an interpretation, then return D1.

Otherwise, D1 is a deduction of B; ` C; return EDL(D1) : ` B ! C. ( 7 ) If A = :B.

Let D1 = Hp( [ fBg; ?).

If D1 is an interpretation, then return D1.

Otherwise, D1 is a deduction of B; ` K with :K 2 Fm(D1); return the deduction EI:(D) : ` :B.

Remark 1. Hereafter A = ? or (A 2 V and :A 2 ). is a consistent set of literals and (A = ? or :A 2 induction hypothesis that Hp( 0; A0) satis es (H1) and (H2). Using the induction hypothesis, the correctness of Hp easily follows. Note that, if none of the cases ( 1 ){( 7 ) is matched, then the property in Remark 1 holds. Thus, in case (8), if A 2 V and D1 is an interpretation, by the induction hypothesis D1 j= n fKg. By Remark 1 :A 2 , hence D1 j= :A as well. If none of the cases ( 1 ){(9) is matched, then Remark 2 holds; thus, in Case (10) is a consistent set of literals, hence \ V is a model of . tu 3

Future work

In this paper we have presented a work in progress on the design of terminating proof-search procedures for Hilbert calculi. Here we only discuss the f!; :gfragment of the Hilbert calculus [5] for CPL. We have implemented the procedure Hc de ned in Sec. 2 in Prolog, extending it to the full language 1. In the full language, the main problems arise from disjunctive goals and from the relationships between the implicative and negated assumptions and the goal to be proved. To get a complete strategy, we have to introduce some \reasoning by absurd" steps and some care is needed to avoid in nite loops.

The main drawback is that in general the obtained proofs are very huge. For instance, the deduction of :(p ! q) ! p consists of 53 formulas and involves very large instances of the axioms. This comes from the fact that the number of lines of E DL(D) is three times the number of lines of D. To reduce the size of deductions, we plan to develop techniques similar to those used in [4]. We also aim at investigating the extension to Intuitionistic Propositional Logic, using the machinery in [4] to get termination. Further possible extensions regard the intermediate logics, by exploiting the ltration techniques introduced in [1].

References

1. A. Avellone , P. Miglioli , U. Moscato , and M. Ornaghi . Generalized tableau systems for intermediate propositional logics . In D. Galmiche, editor, TABLEAUX 1997 , volume 1227 of LNAI , pages 43 { 61 . Springer-Verlag, 1997 .

2. M. D'Agostino . Classical natural deduction . In S.N. Artemov et al., editor, We Will Show Them! , pages 429 { 468 . College Publications , 2005 .

3. M. Ferrari and C. Fiorentini . Proof-search in natural deduction calculus for classical propositional logic . In H. De Nivelle, editor, TABLEAUX 2015 , volume 9323 of LNCS , pages 237 { 252 . Springer International Publishing, 2015 .

4. M. Ferrari , C. Fiorentini , and G. Fiorino. An evaluation-driven decision procedure for G3i . ACM Transactions on Computational Logic (TOCL) , 6 ( 1 ):8: 1 {8: 37 , 2015 .

5. S.C. Kleene . Introduction to Metamathematics. Van Nostrand, New York, 1952 .

6. W. Sieg and J. Byrnes . Normal natural deduction proofs (in classical logic) . Studia Logica , 60 ( 1 ): 67 { 106 , 1998 .

7. A.S. Troelstra and H. Schwichtenberg . Basic Proof Theory , volume 43 of Cambridge Tracts in Theoretical Computer Science. Cambridge University Press, 2nd edition, 2000 .

1 The Prolog prototype is available at https://drive.google.com/open?id= 0ByzJsfKRVFPMVUE2VzBtN2xpUEU