Proof-search in Hilbert calculi Mauro Ferrari1 , Camillo Fiorentini2 , Guido Fiorino3 1 DiSTA, Univ. degli Studi dell’Insubria, Via Mazzini, 5, 21100, Varese, Italy 2 DI, Univ. degli Studi di Milano, Via Comelico, 39, 20135 Milano, Italy 3 DISCO, Univ. degli Studi di Milano-Bicocca, Viale Sarca, 336, 20126, Milano, Italy It is well-known [7] that the standard formalizations of classical and intu- itionistic 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 discus- sion). 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 com- plexity comparable with those based on sequent calculi. In this paper we begin an analogous investigation concerning Hilbert calculi. In particular, we consider the {→, ¬}-fragment of the Hilbert calculus for Classical Propositional Logic defined in [5] and we describe a terminating proof-search procedure for it. 1 The Hilbert calculus Hc 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 ∈ 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) A → (B → A) (Ax2) (A → B) → ((A → (B → C)) → (A → C)) (Ax3) (A → B) → ((A → ¬B) → ¬A) (Ax4) ¬¬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 finite sequence of formulas hA1 , . . . , An i such that An = A and, for every Ai in the sequence, one of the following conditions holds: (a) Ai ∈ Γ (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. 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: (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. t u Let D and E be two deductions, where E = hA1 , . . . , An i. The concatenation of D and E, denoted by D ◦ E, is defined as follows: – let E 0 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 E 0 . One can easily check that: Lemma 1. Let D : Γ ` A and E : ∆ ` B. Then, D ◦ E : Γ ∪ (∆ \ Fm(D)) ` B and Fm(D ◦ E) = Fm(D) ∪ Fm(E). t u 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 de- duction D of A, Γ ` B, as shown in next lemma. Lemma 2 (Deduction Lemma). Let D : A, Γ ` B. Then, there exists a deduction E DL (D) : Γ ` A → B such that, for every C ∈ Fm(D), A → C ∈ Fm(E DL (D)). t u In the next lemma we introduce the deductions E ¬E (D) and E I¬ (D). Lemma 3. (i) Let D : ¬A, Γ ` K such that ¬K ∈ Fm(D). Then, there exists a deduction E ¬E (D) : Γ ` A. (ii) Let D : A, Γ ` K such that ¬K ∈ Fm(D). Then, there exists a deduction E I¬ (D) : Γ ` ¬A. Proof. We prove Point (i). By the Deduction Lemma, there exists a deduction E DL (D) : Γ ` ¬A → K such that ¬A → ¬K ∈ Fm(D). Let us consider the derivation DEF→ (A, K) : ¬A → K, ¬A → ¬K ` A defined in Proposition 1.(4). We can set E ¬E (D) = E DL (D) ◦ DEF→ (A, K) which, by Lemma 1, is a deduction of Γ ` A. The definition of the deduction E I¬ (D) of Point (ii) is similar using DEF→¬ (A, K) instead of DEF→ (A, K). t u A (classical) interpretation I is a subset of V; the validity of a formula A in I, denoted by I |= A, is defined as usual. Given a set of formulas Γ , I is a model of Γ , denoted by I |= Γ , iff I |= C, for every C ∈ Γ . A set of literals is consistent if it does not contain a complementary pair of literals {p, ¬p}. Given a consistent set of literals Γ , the interpretation Γ ∩ V is a model of Γ . 2 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 define the procedure Hp satisfying the following properties: (H1) If A ∈ L, Hp(Γ, A) returns either a deduction D : Γ ` A or a model of Γ ∪ {¬A}. (H2) Hp(Γ, ⊥) returns either a deduction D : Γ ` K such that ¬K ∈ Fm(D) or a model of Γ . 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 defined by cases on Γ and A. The first case among (1)–(9) match- ing 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 |A| the number of symbols occurring in A. Given a finite set Γ of formulas, we set: [ X V(Γ ) = V(A) |Γ | = |A| Lit(Γ ) = Γ ∩ Lit A∈Γ A∈Γ Let Γ1 and Γ2 be two finite sets of formulas and let A1 and A2 be either for- mulas or ⊥. We define the ordering relation (Γ1 , A1 ) ≺ (Γ2 , A2 ) iff the following conditions hold (where |⊥| = 1): (1) V(Γ1 ∪ {A1 }) ⊆ V(Γ2 ∪ {A2 }); (2) either Lit(Γ1 ) ) Lit(Γ2 ) or Lit(Γ1 ) = Lit(Γ2 ) and |Γ1 | + |A1 | < |Γ2 | + |A2 |. One can easily prove that ≺ is well-founded, namely: every ≺-chain of the form · · · ≺ (Γ2 , A2 ) ≺ (Γ1 , A1 ) ≺ (Γ0 , A0 ) has finite length. Indeed, by Point (1) of the definition of ≺, along a ≺-chain no new propositional variable is added, hence we cannot apply Point (2) infinitely 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(|Γ | + |A|). 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) sat- isfies properties (H1) and (H2). One can easily check that every recursive call Hp(Γ 0 , A0 ) performed in the computation of Hp(Γ, A) satisfies (Γ 0 , A0 ) ≺ (Γ, A). In particular, note that no new variables are added, hence V(Γ 0 ∪ {A0 }) ⊆ V(Γ ∪ {A}); 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 ∈ Γ . Return the deduction only consisting of A. (2) If there exists B such that {B, ¬B} ⊆ Γ . 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 {B → C, B} ⊆ Γ . Let D1 = Hp( (Γ \ {B → C}) ∪ {C} , 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 ∈ Γ Let D1 = Hp( (Γ \ {¬¬B}) ∪ {B} , A). If D1 is an interpretation, then return D1 . Otherwise, return the deduction D¬¬E (B) ◦ D1 : Γ ` A. (5) If A = p with p ∈ V and ¬p 6∈ Γ . Let D1 = Hp(Γ ∪ {¬p}, ⊥). If D1 is an interpretation, then return D1 . Otherwise, D1 is a deduction of ¬p, Γ ` K with ¬K ∈ Fm(D1 ); return the deduction E ¬E (D1 ) : Γ ` p. (6) If A = B → C. Let D1 = Hp(Γ ∪ {B}, C). If D1 is an interpretation, then return D1 . Otherwise, D1 is a deduction of B, Γ ` C; return E DL (D1 ) : Γ ` B → C. (7) If A = ¬B. Let D1 = Hp(Γ ∪ {B}, ⊥). If D1 is an interpretation, then return D1 . Otherwise, D1 is a deduction of B, Γ ` K with ¬K ∈ Fm(D1 ); return the deduction E I¬ (D) : Γ ` ¬B. Remark 1. Hereafter A = ⊥ or (A ∈ V and ¬A ∈ Γ ). (8) If there exists ¬K ∈ Γ such that K = B → C. Let D1 = Hp(Γ \ {¬K}, K). If D1 is an interpretation, then return D1 . Otherwise, D1 is a deduction of Γ \ {¬K} ` K. If A = ⊥, then return the deduction h¬Ki ◦ D1 : Γ ` K. If A 6= ⊥, then return the deduction D1 ◦ DEF (K, A) : Γ ` A. (9) If there exists B → C such that B → C ∈ Γ Let D1 = Hp(Γ \ {B → C}, B) and D2 = Hp((Γ \ {B → C}) ∪ {C}, A). If, for some i ∈ {1, 2}, Di is an interpretation, then return Di . Otherwise, return D1 ◦ DMP (B → C, B) ◦ D2 : Γ ` A. Remark 2. Here Γ is a consistent set of literals and (A = ⊥ or ¬A ∈ Γ ). (10) Return the interpretation Γ ∩ V. Figure 1. Procedure Hp (Γ , A) induction hypothesis that Hp(Γ 0 , A0 ) satisfies (H1) and (H2). Using the induc- tion 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 ∈ V and D1 is an interpretation, by the induction hypothesis D1 |= Γ \ {K}. By Remark 1 ¬A ∈ Γ , hence D1 |= ¬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 Γ . t u 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 {→, ¬}- fragment of the Hilbert calculus [5] for CPL. We have implemented the pro- cedure Hc defined 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 infinite 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 filtration 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. Artëmov 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