=Paper=
{{Paper
|id=Vol-1287/lanmr2014_paper_3
|storemode=property
|title=How Many Times Do We Need an Assumption to Prove a Tautology in Minimal Logic: An Example on the Compression Power of Classical Reasoning
|pdfUrl=https://ceur-ws.org/Vol-1287/lanmr2014_paper_3.pdf
|volume=Vol-1287
|dblpUrl=https://dblp.org/rec/conf/lanmr/Haeusler14
}}
==How Many Times Do We Need an Assumption to Prove a Tautology in Minimal Logic: An Example on the Compression Power of Classical Reasoning==
https://ceur-ws.org/Vol-1287/lanmr2014_paper_3.pdf
How many times do we need an assumption to
prove a tautology in Minimal logic: An example
on the compression power of Classical reasoning
Edward Hermann Haeusler
Dep. Informática
PUC-Rio
hermann@inf.puc-rio.br
Abstract In this article we present a class of formulas ϕn , n ∈ N at,
that need at least 2n assumption occurrences to be proved in a normal
proof in Natural Deduction for purely implicational minimal proposi-
tional 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
briefly discuss the consequences of the existence of this class of formu-
las for designing automatic proof-procedures based on these deductive
systems.
1 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 proposi-
tional logic tautology having only huge proofs is related to know whether
N P = CoN P or not (see [2]). Intuitionistic logic is PSPACE-complete
([11]) and Richard Statman (see [16]) showed that purely implicational
minimal logic (M→ ) is PSPACE-complete too. We showed in [8] that,
if a propositional logic has a Natural Deduction (ND) with the sub-
formula property then it is in PSPACE. This follows from the fact that
M→ polynomially encodes any propositional logic that has such ND sys-
tem. Thus, the existence of huge proofs for a more general class of proposi-
tional logics is related to the existence of huge proofs in M→ that amounts
to know whether P SP ACE = N P or not. The relations between these
computational complexity classes and the existence of huge proofs in-
volve arbitrary proof systems, indeed. For example, N P = P SP ACE is
the case, if and only if, for any M→ tautology there is a proof system that
produces a polynomially sized proof of this tautology.
1. INTRODUCTION
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 efficiency 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 con-
clude 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 ([4], Natural Deduction ([4] and [13]) and Tableaux ([1,15])
based. These systems, mainly the first and the third kind, are quite good
in providing means to produce proofs automatically. The backward chain-
ing procedure, for example, if applied to a Sequent Calculus based proof
system provides an automatic way to produce proofs. The problem with
these proof procedures is when a decision on which rule to apply has to
be made and how to deal with non-provable formulas when it is the case.
With respect to this feature of dealing with invalid formulas, the litera-
ture on both systems, Sequent Calculus and Tableaux, provides methods
that either produce a proof or a counter-model uniformly in a unique
proof-procedure. Besides that, since CoPSPACE=PSPACE, providing a
counter-model in M→ is so hard as to provide a proof. We know that
M→ has finite model property and that the size of the counter-model can
be super-polynomial with respect to the formula. It is interesting to inves-
tigate how this is related to the size of proofs in M→ , or at least to have
a concrete evidence that huge proofs may be the case. Most well-known
huge proofs in the literature are considered inside Classical Logic. They
are so in Classical as well as in Minimal logic. Our intention is not only
show huge proofs in M→ . To do that, we could use the polynomial trans-
lations reported in [16] or [8] to generate a formula of the Pigeon-Hole
principle by translating from the full Minimal Logic into M→ . We know,
from [9], that this formula has only super-polynomially sized proofs in
Resolution, and hence in cut-free Sequent Calculus and the same hap-
pens to the translation to M→ in cut-free Sequent Calculus and Natural
Deduction. It is quite hard to detect from these translations why they
are huge in M→ , since there is nothing specific to M→ . We believe that
directly focusing on M→ is a promising path, since M→ has less combinato-
rial alternatives, less logical constants, less alternative deductive system.
The genesis of huge proofs in M→ is interesting and may shed some new
1
With sub-formula property
2 2014
2. THE PURELY IMPLICATIONAL MINIMAL LOGIC
light in propositional logic complexity. This is strongly emphasized by
the fact that the formulas shown in this article does not have huge proofs
when considered the use of Classical Reasoning, performed by Peirce’s
rule. This article has the purpose of showing, by means of these formulas,
how the use of Classical Logic can improve the size of proofs obtained by
an automatic proof procedure of the kind that is able to generated normal
and cut-free derivations. In section 3 we introduce the class of formulas
and in section 4 we show that they have exponentially sized normal proofs
in the usual Natural Deduction for M→ . In the same section we also show
that this is a lower bound in M→ . In classical propositional logic, these
formulas have linear-sized proofs as it is shown in section 3.
All the formal propositional proofs/derivations in this article are pre-
sented in Prawitz-style Natural Deduction. The size of these normal
proofs/derivations is polynomially simulated by cut-free Sequent Calcu-
lus 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 mini-
mal 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 ∈ U and i j then V(i) ⊆ V(j).
Given a model, the satisfaction relationship |= between worlds, in the
model, and formulas is defined as:
– hU, , Vi |=i p, p ∈ L, iff, p ∈ V(i)
– hU, , Vi |=i α1 → α2 , iff, for every j ∈ U , such that i j, if
hU, , Vi |=j α1 then hU, , Vi |=j α2 .
Obs: In (full) minimal logic, ⊥ has no special meaning, so there is no
item declaring that hU, , Vi 6|=i ⊥. We remind that M→ does not have
the ⊥ in its language.
As usual a formula α is valid in a model M, namely M |= α, if and
only if, it is satisfiable in every world i of the model, namely ∀i ∈ U M |=i
α. A formula is a M→ tautology, if and only if, it is valid in every model.
A formula is satisfiable in M→ if it is valid in a model M of M→ . The
problem of knowing whether a formula is satisfiable or not is trivial in
M→ . Every formula is satisfiable in the model h{?}, , Vi, where ? is the
3 2014
3. NEEDING EXPONENTIALLY MANY ASSUMPTIONS
only world, and p ∈ 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 [17]) containing only right and left →-rules is also sound and
complete. As it is well-known one of these rules is not invertible2 . A naive
proof-procedure based on backward chaining for M→ , based only on this
usual Gentzen sequent calculus is not possible.
[α]
|
β α α→β
→-Intro →-Elim
α→β β
3 Needing exponentially many assumptions
In [3] we can find a discussion on the fact that when proving theorems in
a logic weaker than classical logic, the need of using an assumption more
than once has a strong influence on how complex is the proof procedure
and consequently the decision procedure for this logic. There, we can
find the formula ((((A → B) → A) → A) → B) → B. Considering
the proof systems of ND and CS mentioned in the previous section, this
formula needs to use the assumption ((A → B) → A) → A) → B at
least twice in order to be proved in M→ . Inspired by this example, we
can define a class of formulas with no bounds on the use of assumptions.
This shows that limiting the use of assumptions in an automatic proof-
procedure for M→ is not an alternative that ensures completeness. In the
sequel we define the class of formulas. Below you find a normal proof of
((((A → B) → A) → A) → B) → B. Note that it cannot be proved with
less than 2 use of assumptions (((A → B) → A) → A) → B.
The following formula combines two instances of the formula men-
tioned 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, iff, whenever the premises are valid the conclusion is valid and
whenever any premise is invalid the conclusion is also invalid
4 2014
4. NO BOUNDS FOR OCCURRENCE ASSUMPTIONS IN M→
In figure 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 figure 1
[A]1
((A → ξ) → A) → A (((A → ξ) → A) → A) → ξ
ξ
1
A→ξ [(A → ξ) → A]2
A
2
((A → ξ) → A) → A (((A → ξ) → A) → A) → ξ
ξ
We can see how to use this pattern such that if it is repeated n-times
we define 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
definition, 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 figure 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 [12] and [7] we can find
a detailed presentation of the purely implicational classical logic with
some proof-theoretic results. Our discussion on the classical setting has
the purpose of showing how the use of classical logic can, in some cases,
turns proofs smaller.
4 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
5 2014
4. NO BOUNDS FOR OCCURRENCE ASSUMPTIONS IN M→
[(((A → ξ) → A) → A) → ξ]5
[D]3 Σ
(((D → C) → D) → D) ξ
C
3
D→C [(D → C) → D]4 [(((A → ξ) → A) → A) → ξ]5
D Σ
4
((D → C) → D) → D ξ
C
5
((((A → ξ) → A) → A) → ξ) → C
Figure 1. Proof of the formula in purely implicational minimal logic
ΠP eirce1
ΠP eirce2 ((A → ξ) → A) → A [(((A → ξ) → A) → A) → ξ]1
((D → C) → D) → D ξ
C
1
((((A → ξ) → A) → A) → ξ) → C
Figure 2. Proof of the formula in purely implicational classical logic
that there is no normal proof for any of the ϕn , in M→ , with less than
2n assumptions discharged. In the sequel we define ϕn . As it was already
said in section 3, ϕn arises from an iteration process derived from the
previous examples.
Definition 1. Let χ[X, Y ] = (((X → Y ) → X) → X) → Y . Using
χ[X, Y ] we define recursively a family of formulas. Consider the proposi-
tional letters C and Di , i > 0. Let ξi , i > 0, be the formula recursively
defined as:
ξ1 = χ[D1 , C] (2)
ξi+1 = χ[Di+1 , ξi ] (3)
Using this family of formulas we define the formula ϕn , n > 0, such that,
for any i ≥ 0:
ϕi+1 = ξi+1 → C
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 figure 1, replacing ξ by ξ1 , A by
D2 and D by D1 , resulting in the proof shown below.
6 2014
4. NO BOUNDS FOR OCCURRENCE ASSUMPTIONS IN M→
[(((D2 → ξ1 ) → D2 )
→ D2 ) → ξ1 ]5
[D1 ]3 Σ
(((D1 → C) → D1 ) → D1 ) ξ1
[(((D2 → ξ1 ) → D2 )
C
3
D1 → C [(D1 → C) → D1 ]4 → D 2 ) → ξ1 ] 5
D1 Σ
4
((D1 → C) → D1 ) → D1 ξ1
C
5
((((D2 → ξ1 ) → D2 ) → D2 ) → ξ1 ) → C
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, simul-
taneously 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 , finally 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 justified by observing that
the replacements are always on atomic formulas and the rules of M→ do
not have provisos to be unsatisfied 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.
7 2014
4. NO BOUNDS FOR OCCURRENCE ASSUMPTIONS IN M→
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 figure 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
[(((Di+1 → ξi ) → Di+1 ) → Di+1 ) → ξi ]5
[D1 ]3 Π?
(((D1 → C) → D1 ) → D1 ) ξi
C
3
D1 → C [(D1 → C) → D1 ]4 [(((Di+1 → ξi ) → Di+1 ) → Di+1 ) → ξi ]5
D1 Π?
4
((D1 → C) → D1 ) → D1 ξi
C
5
((((Di+1 → ξi ) → Di+1 ) → Di+1 ) → ξi ) → C
Figure 3. Proof of ϕi+1 in M→ with 2i+1 discharged assumptions of ξi+1
Q.E.D.
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 first observe that ϕ1 , i.e.,
((((D1 → C) → D1 ) → D1 ) → C) → C is not provable with only one oc-
currence 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
8 2014
4. NO BOUNDS FOR OCCURRENCE ASSUMPTIONS IN M→
with two worlds such that in the first world neither C nor D1 holds and
in second D1 holds but not C falsifies (((D1 → C) → D1 ) → D1 ) → C.
Consider that there are normal proofs of ϕi with less than 2i assump-
tion 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 .
[ξk ]l
Σk
C
l
ξk → C
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 first line of this paragraph.
Σ0
(((Dk → ξk−1 ) → Dk ) → Dk ) [(((Dk → ξk−1 ) → Dk ) → Dk ) → ξk−1 ]l
ξk−1
Σk
C
l
ξk → C
Note that Σ 0 is a sub-derivation of Σk and it may have ξk as open as-
sumption too, but this is not necessary. If we remove every sub-derivation
like Σ 0 from Σk we end up with a proof as following:
[ξk−1 ]l
Σk−1
C
l
ξk−1 → C
The proof above is a proof of ϕk−1 with less than 2k−1 assumption occur-
rences of ξk−1 discharged by the last rule. This contradicts the fact that
k is the least number holding this property.
Q.E.D.
9 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→ .
Axiom
Ξ, p ⇒ p, [∆]
Ξ, γ1 ⇒ γ2 , [∆]
→-right
Ξ ⇒ γ1 → γ2 , [∆]
Ξ ⇒ α, [γ, ∆] Ξ, β ⇒ γ
→-left
Ξ, α → β ⇒ γ, [∆]
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 {Ξ, p} ∩ {q, ∆} = ∅ is falsified 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 loop-
detecting mechanism is need.We apologize the lack of a deeper technical
discussion due to lack of space. We can, however offer 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 fixed bound for every formula. In fact, if such
a fixed bound existed we would have that every M→ formula would have
a polynomially sized search-space to find either proofs or counter-models
and this is counter-intuitive.
3
We cannot provide the details here due to lack of space
10 2014
6. CONCLUSION
6 Conclusion
Our contribution is in the context that M→ is the hardest and most repre-
sentative propositional logic to define efficient proof-procedures. We show
an example alerting for the fact that allowing unlimited use of assump-
tions 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 efficient than M→ if such
example does not existed. Propositional logic complexity has a lot of con-
jectures, starting with the relations between the main complexity classes.
This article has the sole purpose of providing an example where the ex-
ponential grow of proofs has nothing to do with disjunction and combi-
natorial 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 efficient system. A system that saves mem-
ory 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 for-
mulas 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 se-
mantically than implementation driven. Proof-nets (see [6]) represents an
approach that defends the use of graphs as the most adequate represen-
tation for proofs. We agree with that and we add a practical motivation
for considering digraphs instead of trees for representing proofs (see [14])
7 Acknowledgments
The author would like to thank prof. Gilles Dowek for hearing and read-
ing the initial ideas presented here and providing very good suggestions.
We want to thank Jefferson dos Santos for reading, pointing unclear ex-
planations and helping improving the text.
4
The pigeon-hole principle was used to provide a super-polynomial lower bound for
Robinson’s (propositional) Resolution
11 2014
7. ACKNOWLEDGMENTS
References
1. E.W. Beth. Semantic Entailment and Formal Derivability. Mededelingen der
Koninklijke Nederlandse Akademie van Wetenschappen: Afd. Letterkunde. Noord-
Hollandsche Uitgevers Maatschappij, 1961.
2. Stephen A. Cook. The complexity of theorem-proving procedures. In Proceedings
of the Third Annual ACM Symposium on Theory of Computing, STOC ’71, pages
151–158, New York, NY, USA, 1971. ACM.
3. Gilles Dowek and Ying Jiang. Eigenvariables, bracketing and the decidability of
positive minimal predicate logic. Theoretical Computer Science, 360(13):193 – 208,
2006.
4. G. Gentzen. Untersuchungen ber das logische schlieen i. Mathematische Zeitschrift,
39:176–210, 1935. See english version in [5].
5. G. Gentzen and E. Szabo. The collected papers of Gerhard Gentzen. Studies in
logic and the foundations of mathematics. North-Holland Pub. Co., 1969.
6. Jean-Yves Girard. Proof-nets: The parallel syntax for proof-theory. In P. Agliano
and A. Ursini, editors, Logic and Algebra. Marcel Dekker, New York, 1996.
7. L. Gordeev. On cut elimination in the presence of peirce rule. Archiv fr mathema-
tische Logik und Grundlagenforschung, 26:147–164, 1987.
8. Edward Hermann Haeusler. Propositional logics complexity and the sub-formula
property. CoRR, cs/1401.8209v1, 2014. This a detailed version of [10], pp7-8.
9. A. Haken. The intractability of resolution. Theoretical Computer Science, 39(2–
3):297–308, 1985.
10. Delia Kesner and Petrucio Viana, editors. Proceedings Seventh Workshop on Log-
ical and Semantic Frameworks, with Applications, LSFA 2012, Rio de Janeiro,
Brazil, September 29-30, 2012, volume 113 of EPTCS, 2012.
11. Richard E. Ladner. The computational complexity of provability in systems of
modal propositional logic. SIAM Journal on Computing, 6(3):467–480, 1977.
12. Luiz Carlos Pereira, Edward Hermann Haeusler, Vaston G. Costa, and Wagner
Sanz. A new normalization strategy for the implicational fragment of classical
propositional logic. Studia Logica, 96(1):95–108, 2010.
13. D. Prawitz. Natural deduction: a proof-theoretical study. PhD thesis, Almqvist &
Wiksell, 1965.
14. Marcela Quispe-Cruz, Edward Hermann Haeusler, and Lew Gordeev. Proof-graphs
for minimal implicational logic. In Mauricio Ayala-Rincón, Eduardo Bonelli, and
Ian Mackie, editors, Proceedings 9th International Workshop on Developments
in Computational Models, Buenos Aires, Argentina, 26 August 2013, volume 144
of Electronic Proceedings in Theoretical Computer Science, pages 16–29. Open
Publishing Association, 2014.
15. R. M. Smullyan. First–Order Logic. Springer-Verlag, New York, 1968.
16. Richard Statman. Intuitionistic propositional logic is polynomial-space complete.
Theoretical Computer Science, 9(1):67 – 72, 1979.
17. G. Takeuti. Proof Theory. Studies in logic and the foundations of mathematics.
North-Holland, 1987.
12 2014