Mathematical Problems of Computer Science 59, 27–34, 2023.

doi: 10.51408/1963-0099

UDC 510.64

The Relationship Between the Proof Complexities of

Linear Proofs in Quantified Sequent Calculus and

Substitution Frege Systems

Hakob A. Tamazyan

Yerevan State University, Yerevan, Armenia

e-mail: hakob.tamazyan@ysu.am

Abstract

It has formerly been proved that there is an exponential speed-up in the number of
lines of the quantified propositional sequent calculus over substitution Frege systems
when considering proofs as trees. This paper shows that a linear proof of any quantifier-
free tautology in quantified propositional sequent calculus can be transformed into a
linear proof of the same tautology in a substitution Frege systems with no more than
polynomially increasing proof lines and size.
Keywords: Sequent systems, Frege systems, Proof size, Number of proof lines, Ex-
ponential speed-up.
Article info: Received 23 March 2023; sent for review 2 April 2023; accepted 19 May
2023.

1. Introduction

The existence of a propositional proof system that has proofs of polynomial size for all
tautologies is equivalent to the equation NP = co-NP [1]. This observation has gained
attention in recent years, leading to the examination of new proof systems. Through the
discovery of new systems, the computational power of existing ones is gaining a greater
understanding. A hierarchy of proof systems has been established based on two complexity
measures (size and lines), and the relationships between these systems are being explored.
Alessandra Carbone in [2] compared the number of derivation lines in the form of a tree
in some propositional calculus systems and revealed a distinctive property of the quantified
propositional sequent calculus (QPK system). Namely, for some sequences of formulas,
the QPK system has an exponential speed-up by lines with respect to the substitution
sequent calculus (SPK system) and substitution Frege systems (SF systems) when proofs
are considered as trees. It was shown in [3] that the lines of linear proofs of the same formulae
families in all three systems are the same by order. Later, in [4], the same result was achieved
if one considers the sizes of linear proofs of the same formulae families for comparison.

27



28 The Relationship Between the Proof Complexities of Linear Proofs in QPK and Substitution SF

In this paper, the relationship between the proof complexities of linear proofs in QPK and
SF has been investigated for all quantifier-free tautologies: it turns out that QPK system
has no significant advantage over SF when only linear proofs are considered. Specifically,
after the transformation of linear QPK-proof of a quantifier-free tautology into a linear SF-
proof of the same tautology by some algorithm, both complexities (the number of lines and
sizes) of linear proofs in SF can increase polynomially at most.

2. Preliminaries

First and foremost, lets define several proof systems according to [1, 5, 6].
The Frege system F uses a denumerable set of propositional variables, a finite, complete

set of propositional connectives. It has a finite set of inference rules defined by a figure of
the form A1A2...Am

B
(the rules of inference with zero hypotheses are the schemes of axioms).

F must be sound and complete, i.e., for each rule of inference A1A2...Am
B

every truth-value
assignment, satisfying A1A2...Am, also satisfies B, and F must prove every tautology.

The Substitution Frege system SF is defined by adding to F the substitution rule

A(p)

A(B)

where simultaneous substitution of the formula B is allowed for the variable p.
The LK Sequent calculus was introduced by Gentzen [7] for first-order logic. Each line

in LK-proof is a sequent: a sequent is written in the form:

A1, . . . , An → B1, . . . , Bm

where A1, . . . , An and B1, . . . , Bm are formulas. We denote these sequences of formulas by
capital Greek letters Γ, ∆, etc. As a quantifier symbol in LK, we will include only the
universal quantification ∀. The existential quantification symbol ∃ will be added by the
following definition:

(∃x)A(x) ≡ ¬(∀x)¬A(x).
The inference rules of the sequent calculus LK are as follows:

• Initial sequents are sequents of the following form:

A → A

where A is any formula.

• Structural rules:

Weakening : left
Γ → ∆

A, Γ → ∆
Weakening : right

Γ → ∆
Γ → ∆, A

Exchange : left
Γ1, A, B, Γ2 → ∆
Γ1, B, A, Γ2 → ∆

Exchange : right
Γ → ∆1, A, B, ∆2
Γ → ∆1, B, A, ∆2

Contraction : left
Γ1, A, A, Γ2 → ∆
Γ1, A, Γ2 → ∆

Contraction : right
Γ → ∆1, A, A, ∆2
Γ → ∆1, A, ∆2



H. Tamazyan 29

• Logical rules:

¬ : left
Γ → ∆, A
¬A, Γ → ∆

¬ : right
A, Γ → ∆
Γ → ∆, ¬A

∧ : left
A, B, Γ → ∆
A ∧ B, Γ → ∆

∧ : right
Γ → ∆, A Γ → ∆, B

Γ → ∆, A ∧ B

∨ : left
A, Γ → ∆ B, Γ → ∆

A ∨ B, Γ → ∆
∨ : right

Γ → ∆, A, B
Γ → ∆, A ∨ B

⊃: left
Γ → ∆, A B, Γ → ∆

A ⊃ B, Γ → ∆
⊃: right

A, Γ → ∆, B
Γ → ∆, A ⊃ B

• The cut rule:

Γ → ∆, A A, Γ → ∆
Γ → ∆

Let us denote by PK the sequent calculus LK, where the rules are restricted to propo-
sitional logic.

The substitution system SPK is defined as the propositional sequent calculus PK with
an additional substitution rule:

SBp
Γ → ∆, A(p)
Γ → ∆, A(B)

,

where simultaneous substitution of the formula B is allowed for the variable p, and p does
not appear in Γ, ∆.

The quantifier system QPK is defined as the propositional sequent calculus PK, where
new quantification rules are added:

∀ : left
A(B), Γ → ∆

(∀q)A(q), Γ → ∆
∀ : right

Γ → ∆, A(p)
Γ → ∆, (∀q)A(q)

where B is any formula such that no free variable occurrence in B becomes bounded in
A(B), and with the restriction that the atom p does not occur freely in the lower sequents
of ∀ : right.

Notice that the the following two inferences can be derived in QPK system using the
definition of the quantifier ∃:

∃ : left
A(p), Γ → ∆

(∃q)A(q), Γ → ∆

A(p), Γ → ∆
Γ → ∆, ¬A(p)
Γ → ∆, (∀q)(q)

¬(∀q)¬A(q), Γ → ∆

∃ : right
Γ → ∆, A(B)

Γ → ∆, (∃q)A(q)

Γ → ∆, A(B)
¬A(B), Γ → ∆
(∀q)(q), Γ → ∆

Γ → ∆, ¬(∀q)¬A(q)



30 The Relationship Between the Proof Complexities of Linear Proofs in QPK and Substitution SF

3. Main Results

For a given linear proof in QPK with n number of lines and proof size s, one can always
find a linear proof in SPK of the same tautology having O(n2) lines and O(s5) proof size.

First of all, notice that for any linear proof in SPK, there exists a linear proof in QPK
of the same tautology with the same number of lines. The sequent (∀p)A(p), Γ → ∆, A(B)
is provable for all A, B, and the sequent Γ → ∆, (∀p)A(p) is derivable from ∆ → ∆, A(p).
Hence, after combining them through a cut rule, one derives Γ → ∆, A(B). Here we examine
the relationship between these systems in the opposite scenario.

Lemma. For n, m ≥ 0 and p not appeared in Γ, ∆, the following inference

Γ, A1(p), . . . , An(p) → ∆, An+1(p), . . . , An+m(p)
Γ, A1(B), . . . , An(B) → ∆, An+1(B), . . . , An+m(B)

can be achieved in SPK system with O(n + m) lines using the substitution rule only once.

Proof. First, let’s prove these additional inferences:

1.
Γ → ∆, ¬A
A, Γ → ∆

Γ → ∆, ¬A A → A
Γ → ∆, ¬A ¬A, A →

A, Γ → ∆

2.
Γ → ∆, A ∨ B
Γ → ∆, A, B

Γ → ∆, A ∨ B A → A B → B
Γ → ∆, A ∨ B A → A, B B → B

Γ → ∆, A ∨ B A → A, B B → A, B
Γ → ∆, A ∨ B A ∨ B → A, B

Γ → ∆, A, B

3.
Γ, A ∧ B → ∆
Γ, A, B → ∆

Γ, A ∧ B → ∆ A → A B → B
Γ, A ∧ B → ∆ A, B → A B → B

Γ, A ∧ B → ∆ A, B → A A, B → B
Γ, A ∧ B → ∆ A, B → A ∧ B

Γ, A, B → ∆



H. Tamazyan 31

The final proof will look like this:

Γ, A1(p), . . . , An(p) → ∆, An+1(p), . . . , An+m(p)
Γ, A1(p) ∧ A2(p), . . . , An(p) → ∆, An+1(p), . . . , An+m(p)....

Γ, A1(p) ∧ . . . ∧ An(p) → ∆, An+1(p), . . . , An+m(p)....
Γ, A1(p) ∧ . . . ∧ An(p) → ∆, An+1(p) ∨ . . . ∨ An+m(p)

Γ → ∆, An+1(p) ∨ . . . ∨ An+m(p), ¬(A1(p) ∧ . . . ∧ An(p))
Γ → ∆, An+1(p) ∨ . . . ∨ An+m(p) ∨ ¬(A1(p) ∧ . . . ∧ An(p))

Γ → ∆, An+1(B) ∨ . . . ∨ An+m(B) ∨ ¬(A1(B) ∧ . . . ∧ An(B))
Γ → ∆, An+1(B) ∨ . . . ∨ An+m(B), ¬(A1(B) ∧ . . . ∧ AnB)
Γ, A1(B) ∧ . . . ∧ An(B) → ∆, An+1(B) ∨ . . . ∨ An+m(B)....

Γ, A1(B), . . . , An(B) → ∆, An+1(B), . . . , An+m(B)

Note that in this proof the substitution rule is applied only once.

Theorem 1. For a given linear proof in QPK of some quantifier-free tautology with n
number of lines, there exists a linear proof in SPK of the same tautology having O(n2)
number of lines.

Proof. Suppose P is a given linear proof in QPK. Since P is the proof of a quantifier-
free tautology, if a formula with a quantifier appears in the proof, then it must disappear at
some point in the next lines. These formulas can appear either by quantification rules or by
weakening rules, and the cut rule is the only inference rule capable of removing a formula
from the sequent. Notice that if we apply the cut rule to two sequents and some formula
A with a quantifier is removed, then it is impossible that both of these sequents got this
quantifier by the ∀ : left rule.

First of all, we will remove all applications of the ∀ : left rule in the proof of P . Let
(∀q)A(q) be some formula or subformula in the proof. Suppose it appeared by ∀ : right
rule that infers Γ → ∆, (∀q)A(q) from Γ → ∆, A(p). Since p does not occur free in sequent
Γ → ∆, (∀q)A(q), instead of the ∀ : right rule, we can apply the substitution rule to
Γ → ∆, A(p) and substitute p with some new variable k that did not appear throughout the
proof. If (∀q)A(q) appeared by weakening rules, we will replace it with the formula A(k),
where k is again some new variable that did not appear throughout the proof. According
to the previously mentioned claim, the formula (∀q)A(q) should have been removed at some
point via the cut rule. Therefore, just before the application of cut rule, we will substitute
the variable k with the corresponding matching formula to be able to apply the cut rule
successfully. This substitution is allowed since k does not appear in the remaining formulas
of the sequent.

This removal of formulas with quantifiers from the proof can have the following effects.
Firstly, since these formulas have been replaced with different ones, the contraction rule

can not be applied to these replacements anymore, as they can differ from each other.
Therefore, instead of applying the contraction rule to them, in the next lines we will apply
the same inference rules to both of them. As these formulas should disappear in one of the
next lines by the cut rule, we will apply the cut-elimination rule twice so that both of them



32 The Relationship Between the Proof Complexities of Linear Proofs in QPK and Substitution SF

will be removed. There are O(n) applications of the contraction rule, then after this change,
the number of lines will become O(n2). However, according to the lemma, the number of
applications of the substitution rule will not change and will remain O(n).

Secondly, the ∀ : left rule that transformed some sequent A(B), Γ → ∆ into
(∀q)A(q), Γ → ∆, will not be applied to the proof, and the formula B will appear in the next
lines. Hence, there might be an application of the substitution rule in these next lines that
substitutes some variable x into some formula C so that x also appears in the formula B.
This means that besides the formula C, there can also be other formulas with the variable
x in the sequent. Therefore, to fix this, we will apply the substitution to these formulas too.
Considering that the number of applications of the ∀ : left rule was O(n) and removing
each application of the contraction rule adds just one formula to the sequent, the number
of such formulas in the sequent will be O(n). Therefore, according to the lemma, each such
substitution will require O(n) additional lines. Since there are O(n) applications of the sub-
stitution rule, this change will add O(n2) number of lines to our proof. This will conclude
the transformation process, and the transformed SPK proof will have O(n2) lines.

Theorem 2. For a given linear proof in QPK of some quantifier-free tautology with a proof
size s, there exists a linear proof in SPK of the same tautology having O(s5) proof size.

Proof. Suppose P is a given linear proof in QPK with n number of lines and proof size
s. Let P ′ be the transformed SPK proof according to the process described above. To
calculate its size, let’s dive into the transformation process step by step.

We replaced each application of the ∀ : right rule with a substitution rule to substitute
one variable with another. The formulas with quantifiers that appeared by weakening rules
have been replaced by formulas with the same size. Afterwards, we added a substitution
before the application of the cut rule to match the corresponding formula. All these steps
change the number of proof lines and the proof size linearly. Let’s denote them by n′, s′,
respectively.

Moreover, we removed all applications of the ∀ : left rule. Therefore, if some application
of the ∀ : left rule transformed the sequent A(B), Γ → ∆ into (∀q)A(q), Γ → ∆, then after
the removal, the formula B will appear in the next lines. This will increase the proof size
by at most n′ · |A(B)|, where |A(B)| is the size of the formula A(B). Removing the ith
application of the ∀ : left rule increases the proof size by at most n′ ·|Ai(Bi)|, then removing
all of them will add no more than

∑
i

n′ · |Ai(Bi)| = n′ ·
∑
i

|Ai(Bi)| ≤ n′ · s′ ≤ s′2

to the proof size. As s′ is O(s), after this step, the proof size will be O(s2) and the number
of lines will remain O(n).

Removing applications of the contraction rule has the following two effects on the proof
size.

First of all, it will keep the eliminated formula in a sequent, so it will appear in the next
lines. The added proof size can be calculated completely like the previous method. Since
the number of applications of the contraction rule is O(n) and the proof size is O(s2), this
change will make the proof size O(s3). The number of lines will remain O(n).

The second effect of removing applications of the contraction rule will be applying the
same inference rules to both formulas. Since the proof size is O(s3), then applying the same



H. Tamazyan 33

inference rule to the previously eliminated formula can increase the proof size by O(s3). The
number of applications of the contraction rule is O(n), and since n ≤ s, the overall proof
size will become O(s4).

Finally, the removal of the ∀ : left rule causes some substitution steps to also substitute
the same variable in several other formulas of the same sequent. Notice that all these
substitution steps were ∀ : right rule replacements that substitute one variable with another,
as otherwise we won’t face such a problem. Each such substitution that simultaneously
substitutes the same variable in these sequent formulas required O(n) lines. If the ith such
substitution is applied to the sequent Si, then this change will overall add no more than∑

i

c · n · |Si| = c · n ·
∑
i

|Si| ≤ c · s ·
∑
i

|Si|

to the proof size, where |Si| is the size of the sequent Si and c is some constant.
∑

i |Si| is
smaller than the current proof size, therefore the transformed SPK proof will have O(s5)
size.

Corollary. Since the system SPK is polynomially equivalent to the system SF, there is a
transformation of a linear proof of any quantifier-free tautology in QPK into a linear proof
in the system SF that increases the proof lines and size at most polynomially.

4. Conclusion

This work described an algorithm according to which any QPK linear proof can be trans-
formed into a SF linear proof by increasing its lines and size to at most a polynomial extent.
The obtained results show that the QPK system does not have a substantial advantage over
the system SF in terms of linear proofs.

References

[1] S. A. Cook and A. R. Reckhow, “The relative efficiency of propositional proof systems”,
Symbolic Logic, vol. 44, pp. 36–50, 1979.

[2] A. Carbone, “Quantified propositional logic and the number of lines of tree-like proofs”,
Studia Logica, vol. 64, pp. 315–321, 2000.

[3] H. A. Tamazyan and A. A. Chubaryan, “On proof complexities relations in some
systems of propositional calculus, Mathematical Problems of Computer Science, vol.
54, pp. 138–146, 2020.

[4] L. A. Apinyan and A. A Chubaryan, “On sizes of linear and tree-like proofs for any
formulae families in some systems of propositional calculus”, Mathematical Problems
of Computer Science, vol. 57, pp. 47–55, 2022.

[5] P. Pudlák, The Lengths of Proofs, in S. Buss (ed.), Handbook of Proof Theory, Elsevier,
vol. 137, pp. 547-637, 1998.

[6] J. Kraj́ıc̆ek, Proof Complexity, Encyclopedia of Mathematics and Its Applications,
Cambridge University Press, vol. 170, 2019.

[7] G. Gentzen, “Die Widerspruchsfreiheit der reinen Zahlentheorie”, Mathematische An-
nalen, vol. 112, pp. 493–565, 1936.



3 4 The Relationship Between the Proof Complexities of Linear Proofs in QPK and Substitution SF

¶Í³ÛÇÝ ³ñï³ÍáõÙÝ»ñÇ µ³ñ¹áõÃÛáõÝÝ»ñÇ Ï³åÁ ͳí³ÉÇãÝ»ñáí
ë»Ïí»ÝóÇ³É Ñ³Ù³Ï³ñ·áõÙ ¨ ï»Õ³¹ñÙ³Ý

ϳÝáÝáí üñ»·»Ç ѳٳϳñ·»ñáõÙ

гÏáµ ². ³ٳ½Û³Ý

ºñ¨³ÝÇ å»ï³Ï³Ý ѳٳÉë³ñ³Ý, ºñ¨³Ý, г۳ëï³Ý

e-mail: hakob.tamazyan@ysu.am

²Ù÷á÷áõÙ

Ñâÿçü ìåæäó ñëîæíîñòÿìè äîêàçàòåëüñòâ ëèíåéíûõ
âûâîäîâ â ñèñòåìå ñåêâåíöèàëüíîãî èñ÷èñëåíèÿ ñ

êâàíòîðàìè è ñèñòåìàõ Ôðåãå ñ ïðàâèëîì ïîäñòàíîâêè
Àêîá À. Òàìàçÿí

Åðåâàíñêèé ãîñóäàðñòâåííûé óíèâåðñèòåò, Åðåâàí, Àðìåíèÿ
e-mail: hakob.tamazyan@ysu.am

Àííîòàöèÿ

Ðàíåå áûëî äîêàçàíî, ÷òî ñóùåñòâóåò ýêñïîíåíöèàëüíîå óñêîðåíèå êîëè÷åñòâà
øàãîâ â ñèñòåìå ñåêâåíöèàëüíîãî èñ÷èñëåíèÿ âûñêàçûâàíèé ñ êâàíòîðàìè ïî
ñðàâíåíèþ ñ ñèñòåìàìè Ôðåãå ñ ïðàâèëîì ïîäñòàíîâêè, êîãäà ìû ðàññìàòðèâàåì
âûâîäû â âèäå äåðåâüåâ. Ýòà ñòàòüÿ ïîêàçûâàåò, ÷òî ëèíåéíûé âûâîä ëþáîé
áåñêâàíòîðíîé òàâòîëîãèè â ñèñòåìå ñåêâåíöèàëüíîãî èñ÷èñëåíèÿ âûñêàçûâàíèé
ñ êâàíòîðàìè ìîæíî ïðåâðàòèòü â ëèíåéíûé âûâîä òîé æå òàâòîëîãèè â ñèñòåìàõ
Ôðåãå ñ ïðàâèëîì ïîäñòàíîâêè ñ íå áîëåå ÷åì ïîëèíîìèàëüíî âîçðàñòàþùèì
êîëè÷åñòâîì øàãîâ è äëèíîé âûâîäà.

Êëþ÷åâûå ñëîâà: ñåêâåíöèàëüíûå ñèñòåìû, ñèñòåìû Ôðåãå, äëèíà âûâîäà,
êîëè÷åñòâî øàãîâ âûâîäà, ýêñïîíåíöèàëüíîå óñêîðåíèå.

ܳËÏÇÝáõÙ ³å³óáõóí»É ¿, áñ ͳí³ÉÇãÝ»ñáí ë»Ïí»ÝóÇ³É Ñ³Ù³Ï³ñ·áõÙ ³éϳ
¿ ù³ÛÉ»ñÇ ù³Ý³ÏÇ ¿ùëåáÝ»ÝóÇ³É ³ñ³·³óáõÙ ï»Õ³¹ñÙ³Ý Ï³ÝáÝáí üñ»·»Ç
ѳٳϳñ·»ñÇ Ýϳïٳٵ, »ñµ ¹Çï³ñÏáõÙ »Ýù ͳé³ÛÇÝ ³ñï³ÍáõÙÝ»ñÁ: ²Ûë Ñá¹í³ÍÁ
óáõÛó ¿ ï³ÉÇë, áñ ³é³Ýó ͳí³ÉÇãÝ»ñÇ, ó³Ýϳó³Í ÝáõÛݳµ³ÝáõÃÛ³Ý ·Í³ÛÇÝ
³ñï³ÍáõÙÁ ͳí³ÉÇãÝ»ñáí ë»Ïí»ÝóÇ³É Ñ³Ù³Ï³ñ·áõÙ Ñݳñ³íáñ ¿ í»ñ³Í»É ÝáõÛÝ
ÝáõÛݳµ³ÝáõÃÛ³Ý ·Í³ÛÇÝ ³ñï³ÍÙ³Ý ï»Õ³¹ñÙ³Ý Ï³ÝáÝáí üñ»·»Ç ѳٳϳñ·»ñáõÙ`
áõݻݳÉáí ³ñï³ÍÙ³Ý ù³ÛÉ»ñÇ ù³Ý³ÏÇ ¨ »ñϳñáõÃÛ³Ý ³é³í»É³·áõÛÝ µ³½Ù³Ý¹³Ù³ÛÇÝ
³×:

´³Ý³ÉÇ µ³é»ñ` ë»Ïí»ÝóÇ³É Ñ³Ù³Ï³ñ·»ñ, üñ»·»Ç ѳٳϳñ·»ñ, ³ñï³ÍÙ³Ý
»ñϳñáõÃÛáõÝ, ³ñï³ÍÙ³Ý ù³ÛÉ»ñÇ ù³Ý³Ï, ¿ùëåáÝ»ÝóÇ³É ³ñ³·³óáõÙ:


	03_Chub_59_27_34
	03