In this article we present a class of formulas 'n, n 2 N at, that need at least 2n assumption occurrences to be proved in a normal proof in Natural Deduction for purely implicational minimal propositional logic. In purely implicational classical propositional logic, with Peirce's rule, each 'n is proved with only one assumption occurrence in Natural Deduction in a normal proof. Besides that, the formulas 'n have exponentially sized proofs in cut-free Sequent Calculus. In fact 2n is the lower-bound for normal proofs in ND and cut-free Sequent proofs. We brie y discuss the consequences of the existence of this class of formulas for designing automatic proof-procedures based on these deductive systems.
Introduction
Providing proofs for propositional tautologies seems to be a hard task.
Huge proofs are such that their size is super-polynomial with regard to
the size of their conclusions. Knowing that there is a classical
propositional logic tautology having only huge proofs is related to know whether
N P = CoN P or not (see [
Dealing with arbitrary and general proof systems is quite hard, and is obviously out of scope of this article. However, studying particular proof systems for key logics, like M!or classical logic, can shed some light on practical aspects of implementing propositional theorem provers from the e ciency and economy of storage point of view. M!carries almost all the proof-theoretical and logical information to produce polynomially bounded proofs in well-behaved1 propositional logics. Thus we can conclude that focusing investigations on M!is worth of noticing.
There are many proof systems for M!. The most well-known are
structural/analytic proof systems. Well-known systems are the Sequent
Calculus ([
All the formal propositional proofs/derivations in this article are presented in Prawitz-style Natural Deduction. The size of these normal proofs/derivations is polynomially simulated by cut-free Sequent Calculus and/or Tableaux. Thus, the lower bound shown here also applies to them. 2
The purely implicational minimal logic The (purely) implicational minimal logic M!is the fragment of minimal logic containing only the logical constant !. Its semantics is the intuitionistic Kripke semantics restricted to ! only. Given propositional language L, a M!model is a structure hU; ; Vi, where U is a non-empty set (worlds), is a partial order relation on U and V is a function from U into the power set of L, such that if i; j 2 U and i j then V(i) V(j). Given a model, the satisfaction relationship j= between worlds, in the model, and formulas is de ned as: { hU; ; Vi j=i p, p 2 L, i , p 2 V(i) { hU; ; Vi j=i 1 ! 2, i , for every j 2 U , such that i hU; ; Vi j=j 1 then hU; ; Vi j=j 2. j, if
Obs: In (full) minimal logic, ? has no special meaning, so there is no item declaring that hU; ; Vi 6j=i ?. We remind that M!does not have the ? in its language.
As usual a formula is valid in a model M, namely M j= , if and only if, it is satis able in every world i of the model, namely 8i 2 U M j=i . A formula is a M!tautology, if and only if, it is valid in every model. A formula is satis able in M!if it is valid in a model M of M!. The problem of knowing whether a formula is satis able or not is trivial in M!. Every formula is satis able in the model hf?g; ; Vi, where ? is the 2014 3. NEEDING EXPONENTIALLY MANY ASSUMPTIONS only world, and p 2 V(?), for every p. Thus, SAT is not an interesting problem in M!. The same cannot be told about knowing whether a formula is a M!tautology or not.
It is known that Prawitz Natural Deduction system for minimal logic
with only the !-rules (!-Elim and !-Intro below) is sound and complete
for the M!Kripke semantics. As a consequence of this, Gentzen's LJ
system (see [
The following formula combines two instances of the formula mentioned above in order to have a formula that needs 4 times an assumption. ((((A ! ) ! A) ! A) ! ) ! C (1) where
= (((D ! C) ! D) ! D) ! C. 2 A rule is invertible, i , whenever the premises are valid the conclusion is valid and whenever any premise is invalid the conclusion is also invalid 2014 In gure 1 we show a normal derivation of this formula 1 above. We can see that it has 4 assumptions of ((A ! ) ! A) ! A) ! ). They are from the two assumption occurrences in the derivation shown below, that is used twice in the proof in gure 1
[A]1 ((A ! ) ! A) ! A
A ! (((A ! ) ! A) ! A) ! 1
[(A ! ) ! A]2
A ((A ! ) ! A) ! A 2 (((A ! ) ! A) ! A) !
We can see how to use this pattern such that if it is repeated n-times we de ne a formula 'n, such that, any normal proof of 'n has to use an assumption at least 2n times, see section 4. Before we proceed with 'n de nition, we have to show that the need for repeating assumptions is not the case for classical propositional logic.
Consider now that the logic is the purely implicational classical logic
instead of the purely implicational minimal logic. That is, we consider the
! introduction and elimination rules, plus the classical absurdity rule,
or the Peirce's rule: from C ! D ` C then infer C. Taking into account
the version with Peirce's rule, we provide the proof of the formula 1 with
only use of assumption, as shown in gure 2. This comes from the fact
that (((D ! C) ! D) ! D) in an instance of the implicational form of
Peirce's rule, so it is provable. From this proof and = (((D ! C) !
D) ! D) ! C we prove C. itself is provable by means of a proof of
the Peirce's formula ((A ! ) ! A) ! A) and the (((A ! ) ! A) !
A) ! discharged to proof the desired formula. The purely implicational
classical logic is not the focus of this article, in [
No bounds for occurrence assumptions in M! In this section we prove that for each n there is a formula 'n, such that, any normal proof of 'n has at least 2n occurrence assumptions of the same formula, that are all of them discharged in only one introduction rule. The following proposition 1 shows that 2n is an upper bound by showing the normal proof that uses 2n assumptions for proving 'n. Theorem 1 shows 2014 [D]3 (((D ! C) ! D) ! D)
C D ! C 3 [(((A ! ) ! A) ! A) ! ]5
[(D ! C) ! D]4 [(((A ! ) ! A) ! A) ! ]5
D ((D ! C) ! D) ! D 4
C ((((A ! ) ! A) ! A) ! ) ! C 5 that there is no normal proof for any of the 'n, in M!, with less than 2n assumptions discharged. In the sequel we de ne 'n. As it was already said in section 3, 'n arises from an iteration process derived from the previous examples.
De nition 1. Let [X; Y ] = (((X ! Y ) ! X) ! X) ! Y . Using [X; Y ] we de ne recursively a family of formulas. Consider the propositional letters C and Di, i > 0. Let i, i > 0, be the formula recursively de ned as:
1 = [D1; C] i+1 = [Di+1; i] 'i+1 = i+1 ! C Using this family of formulas we de ne the formula 'n, n > 0, such that, for any i 0:
We can observe that '1 = 1 ! C can be proved by using proof , replacing for C and A for D1, and applying an !-introduction as the last rule. The obtained proof has 2 occurrence assumptions of the formula 1. The proof of '2 is the proof shown in gure 1, replacing by 1, A by D2 and D by D1, resulting in the proof shown below. (2) (3) 2014
The following lemma will be used in the proof of proposition 1. Lemma 1. In the formula i, i > 0, if we simultaneously replace C by 1, and for each k > 0, Dk by Dk+1, the resulting formula is [Di+1; i]. Proof. This lemma is proved by induction on i. For 1 we observe that replacing C by 1 and D1 by D2 in 1, the resulting formula is [D2; 1]. Assuming that for i > 0, replacing of C by 1 and, for each k = 1; i, simultaneously replacing Di by Di+1 in i, yields [Di+1; i]. Observing that i+1 = [Di+1; i] and by inductive hypothesis, simultaneous replacing of C by 1 and Dk by Dk+1 in i, k = 1; i, yields i+1. As Di+1 does not occur in i, nally replacing Di+1 by Di+2 in i+1 = [Di+1; i+1] yields [Di+2; i+1]. This proves the inductive step.
Another observation is that substitutions as the above shown in the lemma, if applied in a derivation in M!, do imply that the resulting tree is a valid derivation too. This fact is justi ed by observing that the replacements are always on atomic formulas and the rules of M!do not have provisos to be unsatis ed as consequence of these replacements. Thus,we have the following fact.
Fact 1 If is a derivation of from 1; : : : ; l and a substitution S (of atomic formulas only) is applied to then S( ) is a derivation of S( ) from S( 1); : : : ; S( l). Besides that, if is normal then S( ) is normal too.
As '1 has two (21) occurrences of the same assumption and '2 has four (22) occurrences of the same assumptions, we have the following result.
Proposition 1. For any n > 0, there is a normal proof of 'n having 2n occurrences of the same assumptions, that are discharged by the last rule of the proof. 2014 Proof. The proof proceeds by induction. The basis n = 1 is the proof shown inside proof below. Assuming that 'i, i > 0 has a normal proof 'i having 2i occurrences of i discharged by its last inference rule. Thus, we have a normal derivation of C from 2i occurrences of i, remembering that 'i = i ! C. We argue that if we simultaneously replace C by 1, and for each k = 1; i, replace Dk by Dk+1, we will have, by lemma 1 and fact 1, a normal derivation of 1 from 2i occurrences of [Di+1; i]. Let us call this derivation ?. The following derivation (see gure 3) is a derivation of C from ((((Di+1 ! i) ! Di+1) ! Di+1) ! i) ! C, i.e., it is a derivation of C from i+1, and hence, by an !-introduction of we have a normal derivation of 'i+1 discharging 2i + 2i = 2i+1 assumptions of the formula i+1
The following proposition provides 2i as the lower bound for number of assumption occurrences of a sole formula in proving 'i by means of normal proofs in M!.
Theorem 1. Any normal proof of 'i in M!has at least 2i assumption occurrences of i.
Proof. We prove that for any i, there is no normal proof of 'i with less than 2i assumption occurrences of i. We rst observe that '1, i.e., ((((D1 ! C) ! D1) ! D1) ! C) ! C is not provable with only one occurrence of 1 = (((D1 ! C) ! D1) ! D1) ! C). If this was the case we would have, from an analysis of the form of the normal proof of C from 1, that ((D1 ! C) ! D1) ! D1 would be provable in M!, and this cannot be the case since this formula is only classically valid. A Kripke model 2014 with two worlds such that in the rst world neither C nor D1 holds and in second D1 holds but not C falsi es (((D1 ! C) ! D1) ! D1) ! C.
Consider that there are normal proofs of 'i with less than 2i assumption occurrences of i. So there is the least k (k > 0), such that, 'k has a normal proof with less than 2k assumption occurrences of k. Let k be such proof. Since 'k = k ! C, this proof is as follows. We remember that k is the only open assumption in k. Since k = [Dk; k 1] = (((Dk ! k 1) ! Dk) ! Dk) ! k 1, it has to be major premise of an !-elim rule. If this is not the case then k is minor premise of a !-elim rule having a major premise of the form k ! . This formula on its turn has to be sub-formula of the open assumption of this branch, for the derivation is normal and k ! can be only conclusion of an application of an !-elim rule. Since the only open assumption in k is k itself, the case of k as minor premise is not possible. Thus, as k is major premise, k is of the following form, remembering how is k, showed in the rst line of this paragraph.
0 (((Dk ! k 1) ! Dk) ! Dk) [(((Dk ! k 1) ! Dk) ! Dk) ! k 1]l The proof above is a proof of 'k 1 with less than 2k 1 assumption occurrences of k 1 discharged by the last rule. This contradicts the fact that k is the least number holding this property.
[ k 1]l k 1
C k 1 ! C
l 2014 5. A BRIEF DISCUSSION ON COUNTER-MODEL CONSTRUCTION IN SEQUENT CALCULUS FOR M! 5
A brief discussion on counter-model construction in Sequent Calculus for M! Consider the following (incomplete) sequent calculus for M!. ; p ) p; [ ]
Axiom ; 1 ) 2; [ ] ) 1 ! 2; [ ] !-right ) ; [ ; ] ; !
The formulas in the right-hand side of the sequent and between the brackets are used only for counter-model construction. The main idea is that a sequent of the form ; p ) q; [ ] having all members of [ as propositional letters and f ; pg \ fq; g = ; is falsi ed in a Kripke model with two worlds3. From this case and using the invertible (if any premise is not valid the conclusion is too) rules of the system it is possible to build a polynomially sized Kripke model for the conclusion of the tree. Remember that in this case we do not have a proof. As already said, this system is incomplete, for it is unable to prove any of the formulas belonging to the class we presented here. The mentioned formulas are only provable if the correct version of !-left rule is used, as the following, instead of the above.
; ! ) ; [ ; ] ; !
; ! ; ) ) ; [ ] !-left
In this case a counter-model generation is not so obvious, since a loopdetecting mechanism is need.We apologize the lack of a deeper technical discussion due to lack of space. We can, however o er a more intuitive reason. If there were a bound on the use of repeated formulas, we could have used both versions of the !-left rule for a counter-model generation. Of course, for every formula there is a bound, for example the formula ((((A ! B) ! A) ! A) ! B) ! B the bound is 2. What we have shown is that there is no xed bound for every formula. In fact, if such a xed bound existed we would have that every M!formula would have a polynomially sized search-space to nd either proofs or counter-models and this is counter-intuitive. 3 We cannot provide the details here due to lack of space
2014
6
Conclusion Our contribution is in the context that M!is the hardest and most representative propositional logic to de ne e cient proof-procedures. We show an example alerting for the fact that allowing unlimited use of assumptions is worth for any complete proof-procedure. This example runs in M!. We are not aware of a similar example for classical logic. In this case classical propositional logic would be more e cient than M!if such example does not existed. Propositional logic complexity has a lot of conjectures, starting with the relations between the main complexity classes. This article has the sole purpose of providing an example where the exponential grow of proofs has nothing to do with disjunction and combinatorial principles like the Pigeon-Hole4. We provided such example.
Developers of theorem provers have to be aware of many aspects of
the logic in order to design a e cient system. A system that saves
memory and it is fast. Of course, dealing with PSPACE-complete problems
is not a so easy task. Any information that can guide the designer is of
help. Knowing that the number of copies of a formulas in a proof can be
a \bottleneck" for saving memory, an obvious solution would be the use
of references instead of copies when representing proofs. The number of
references is exponential, but references to formulas are smaller than
formulas in most of the cases. This approach points out to the use of graphs
(digraphs in fact) for representing proofs. There are a lot of developments
done in this direction reported in the literature. Most of them are more
semantically than implementation driven. Proof-nets (see [
Acknowledgments The author would like to thank prof. Gilles Dowek for hearing and reading the initial ideas presented here and providing very good suggestions. We want to thank Je erson dos Santos for reading, pointing unclear explanations and helping improving the text. 4 The pigeon-hole principle was used to provide a super-polynomial lower bound for Robinson's (propositional) Resolution 2014