Mathematical Problems of Computer Science 56, 65–72, 2021.

UDC 510.6

On Proof Complexity of Some Type of Tautologies

Vahagn N. Altunyan and Garik V. Petrosyan

Yerevan State University

e-mail: altunyanv@gmail.com, garik.petrosyan.1@gmail.com

Abstract

In this paper, we investigate the proof complexities of a special type of tautologies,
which are described as tautologies consisting of implications and literals. In particular,
we prove that the proof of this kind of tautologies can be polynomially reduced to the
proof of tautologies consisting of formulas that are described by sign-alternating trees.

Keywords: Frege systems, Tautology, Sign-alternating tree, Proof complexity.

1. Introduction

One of the most fundamental problems of the proof complexity theory is to find an efficient
proof system for classical propositional calculus. There is a widespread understanding that
polynomial-time computability is the correct mathematical model of feasible computation.
According to the opinion, a truly effective system should have a polynomial-size p(n) proof
for every tautology of size n. In [1], Cook and Reckhow named such a system a super system.
They showed that NP = coNP iff there exists a super system. It is well known that many
systems are not super. This question about the Frege system, the most natural calculi for
propositional logic, is still open.

In many papers, some specific sets of tautologies are introduced, and it is shown that
the question about polynomially bounded sizes for Frege-proofs of all tautologies is reduced
to an analogous question for a set of specific tautologies. In particular, Lutz Strasburger
introduced in [2] the notion of balanced formulas and showed that if there are polynomially
bounded Frege proofs for the set of balanced tautologies, then the Frege systems are super.
An analogous result for some other class of tautologies is proved in [3].

In this work, we introduce formulas that can be described by sign-alternating trees (sat
formulas) and show that the proofs of tautologies that contain only ⊃ and ¬ symbols,
where ¬ is used only in literals, can be polynomially reduced to proofs of specific formulas
constructed from sat formulas.

2. Main Notions and Notations

We will use the current concepts of a classical tautology, Frege proof systems for classical
propositional logic, proof and proof complexity [1]. Let us recall some of them.

65



66 On Proof Complexity of Some Type of Tautologies

A Frege system F uses a denumerable set of propositional variables, a finite, complete
set of propositional connectives; F has a finite set of inference rules defined by a figure of the
form A1A2...An

B
(the rules of inference with zero hypotheses are the axioms schemes); F must

be sound and complete, i.e., for each rule of inference A1A2...An
B

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

The particular choice of a language for the presented propositional formulas is immaterial
in this consideration. However, for some technical reasons, we assume that the language
contains propositional variables, logical connectives ¬, ∧, ∨, ⊃ and parentheses (, ). Note
that some parentheses can be omitted in generally accepted cases.

By |φ| we denote the size of a formula φ, defined as the number of entries of all logical
signs in it. It is obvious that the full size of a formula, which is understood to be the number
of all symbols is bounded by some linear function in |φ|.

In the theory of proof complexity, the two main characteristics of the proof are: t-
complexity (length), defined as the number of proof steps, l-complexity (size), defined as the
sum of sizes for all formulas in the proof (formal definitions are, for example, in [4]).

Let ϕ be a proof system and φ be a tautology. We denote by lϕφ(t
ϕ
φ) the minimal possible

value of l-complexity (t-complexity) for all ϕ-proofs of tautology φ.
Let M be some set of tautologies.

Definition 1: We call the ϕ-proofs of tautologies from a set M l-polynomially (t-
polynomially) bounded if there is a polynomial p such that lϕφ ≤ p(|φ|) (tϕφ ≤ p(|φ|)) for
all φ from M.

Definition 2: We call the ϕ-proofs of tautologies from a set M l-linearly (t-linearly) bounded
if there is a linear function f such that lϕφ ≤ f(|φ|) (tϕφ ≤ f(|φ|)) for all φ from M.

Now we’ll give the definition of sat formulas and prove some lemmas, which are necessary
for proving the main result.

Definition 3: We’ll say that a formula is described by a sign-alternating tree (sat formula)
if it satisfies the following rules.

1. it’s a literal

2. has a form r ∧ (T1 ∨ T2), where r is a literal and T1, T2 are sat formulas

Lemma 1: For any formulas A, B, C, the following formulas have polynomially bounded
proofs.

1. A ≡ (C ⊃ A) ∧ (¬C ⊃ A)

2. A ⊃ (B ⊃ A)

3. (¬A ⊃ (B ⊃ A)) ≡ (¬A ⊃ ¬B)

4. ¬¬A ≡ A

5. A ⊃ (B ⊃ C) ≡ A ∧ B ⊃ C

6. A ∧ ¬A ∧ B ⊃ C



V. Altunyan and G. Petrosyan 67

7. A ∧ B ⊃ A

8. ¬(A ⊃ B) ≡ A ∧ ¬B

9. A ⊃ (B ∧ C) ≡ (A ⊃ B) ∧ (A ⊃ C)

10. A ⊃ (B ⊃ C) ≡ B ⊃ (A ⊃ C)

11. A ⊃ (A ⊃ B) ≡ A ⊃ B

12. (A ⊃ B) ∧ (C ⊃ B) ≡ (A ∨ C) ⊃ B

The proof is trivial as all the formulas are tautologies and have fixed length proofs, so
the proof complexities may be assumed to be linearly bounded.

Lemma 2: Tautologies of the form

A ⊃ (B1 ⊃ ...(Bn−1 ⊃ (Bn ⊃ A))...)

have polynomially bounded proofs.

Proof. We can prove the tautology above by the following steps.

A ⊢ A
A ⊢ A ⊃ (Bn ⊃ A) 2nd formula of Lemma 1
A ⊢ (Bn ⊃ A) modus ponens
A ⊢ (Bn ⊃ A) ⊃ (Bn−1 ⊃ (Bn ⊃ A))
A ⊢ (Bn−1 ⊃ (Bn ⊃ A)) modus ponens
...

A ⊢ (B1 ⊃ ...(Bn−1 ⊃ (Bn ⊃ A))...)

The number of proof steps is linearly bounded and the size of each formula in proof is also
linearly bounded, so the proof is polynomially bounded.

Lemma 3: Tautologies of the form

d1 ⊃ (d2 ⊃ (... ⊃ dk)...)

where d1, d2, ..., dk are literals, have polynomially bounded proofs.

Proof. After applying the operation of replacement by an equivalent formula (k − 2)
times using the 5th formula of Lemma 1, we get:

d1 ⊃ (d2 ⊃ (... ⊃ dk)...) ≡ d1 ∧ d2 ∧ ... ∧ dk−1 ⊃ dk

In this case, if there exist 1 ≤ i, j, ≤ k − 1 such that di = ¬dj then replacing them with
equivalent formulas using the 6th formula of Lemma 1, we’ll get a polynomially bounded
proof, or if there exist such 1 ≤ i ≤ k − 1 such that di = dk then replacing it with equiv-
alent formulas using the 7th formula of Lemma 1, we’ll get a polynomially bounded proof,
otherwise the formula isn’t a tautology.



68 On Proof Complexity of Some Type of Tautologies

3. Main Result

Definition 4: Any propositional formula A is called sat-constructed if it is in the following
form: A = ¬(T1 ∧ T2 ∧ ... ∧ Tn), where Ti(1 ≤ i ≤ n) are sat formulas.

Theorem 1: Let M be the set of all sat-constructed tautologies. If proofs of formulas from
the set M are l-polynomially (t-polynomially) bounded, then proofs of all tautologies contain-
ing only ⊃ and ¬ symbols, where ¬ is used only in literals, are l-polynomially (t-polynomially)
bounded.

Proof. We need to prove that any tautology A containing only ⊃ and ¬ symbols, where
¬ is used only in literals, can be reduced to a sat-constructed tautology in polynomially
bounded number of steps and length.

If the number of implications in the formula is bounded by, let’s say, 3, then it can
be reduced to ¬(p1 ∧ ¬p1), and the reduction complexity will be constant which is also a
polynomial. We now assume that formula A contains more than 3 implications. A can be
expressed in the following form:

A = (S1 ⊃ ...(Sc−1 ⊃ (Sc ⊃ q1))...) (1)

where Si(1 ≤ i ≤ c) are sub-formulas and q1 is a literal. We can replace A with an
equivalent formula using the 1st formula of Lemma 1 and get (q1 ⊃ A) ∧ (¬q1 ⊃ A). The
first half has a polynomially bounded proof by Lemma 2.

For the second half, we can apply the operation of replacement by an equivalent formula
using the 3rd formula of Lemma 1 and get:

¬q1 ⊃ (S1 ⊃ ...(Sc−1 ⊃ (Sc ⊃ q1))...) ≡ ¬q1 ⊃ (S1 ⊃ ...(Sc−1 ⊃ ¬Sc)...)

So the proof of A has been polynomially reduced to the proof of ¬q1 ⊃ (S1 ⊃ ...(Sc−1 ⊃
¬Sc)...). If Sc is a literal, then we can repeat the same process for the formula we got.
After some repetitions, we’ll end up either with a tautology d1 ⊃ (d2 ⊃ (... ⊃ dk)...), where
di(1 ≤ i ≤ k) are literals. This tautology has a polynomially bounded proof by Lemma 3.
Or we’ll end up with the following formula:

d1 ⊃ (d2 ⊃ ... ⊃ (dm ⊃ (U1 ⊃ ...(Uk ⊃ ¬F)...))...) (2)

where di(1 ≤ i ≤ m) are literals and F is not a literal.
Suppose F = F1 ⊃ F2, applying the replacement by an equivalent formula using the 8th

formula of Lemma 1, we’ll get:

d1 ⊃ (d2 ⊃ ... ⊃ (dm ⊃ (U1 ⊃ ...(Uk ⊃ ¬F)...))...) ≡
d1 ⊃ (d2 ⊃ ... ⊃ (dm ⊃ (U1 ⊃ ...(Uk ⊃ (F1 ∧ ¬F2))...))...)

Applying the operation of replacement by an equivalent formula multiple times using the
9th formula of Lemma 1, we’ll get:

d1 ⊃ (d2 ⊃ ... ⊃ (dm ⊃ (U1 ⊃ ...(Uk ⊃ (F1 ∧ ¬F2))...))...) ≡
d1 ⊃ (d2 ⊃ ... ⊃ (dm ⊃ (U1 ⊃ ...(Uk ⊃ F1)...))...)∧
d1 ⊃ (d2 ⊃ ... ⊃ (dm ⊃ (U1 ⊃ ...(Uk ⊃ ¬F2)...))...)



V. Altunyan and G. Petrosyan 69

So, after polynomially bounded number of steps, we reduced the proof of A to the proof
of two formulas, the first one of which has the form (1) and the second one has the form (2).
Repeating the same process for these formulas, we’ll get l tautologies, and the proof of A
will be reduced to the proof of these tautologies:

d11 ⊃ (d
1
2 ⊃ ... ⊃ (d

1
m1

⊃ (d1 ⊃ (d2 ⊃ ... ⊃ (dm ⊃ (U1 ⊃ ... ⊃ ¬Uk))...)))...)
d21 ⊃ (d

2
2 ⊃ ... ⊃ (d

2
m2

⊃ (d1 ⊃ (d2 ⊃ ... ⊃ (dm ⊃ (U1 ⊃ ... ⊃ ¬Uk))...)))...)
...

dl1 ⊃ (d
l
2 ⊃ ... ⊃ (d

l
ml

⊃ (d1 ⊃ (d2 ⊃ ... ⊃ (dm ⊃ (U1 ⊃ ... ⊃ ¬Uk))...)))...)
where di1, d

i
2, ..., d

i
mi
(1 ≤ i ≤ l) are literals. There are no repetitions among

di1, d
i
2, ..., d

i
mi
, d1, ..., dm, otherwise we can keep a single one of each repetition - replacing

by equivalent formulas using the 10th and 11th formulas of Lemma 1. We may also assume
that there are no variable repetitions, because if a variable and it’s negation are present,
then the formula can be polynomially proved. So we can assume that all the literals among
di1, d

i
2, ..., d

i
mi
, d1, ..., dm are different and all the variables are also different and so the number

of those literals doesn’t exceed |A|. Also note that each time a new formula was generated
an implication from F was removed, so l < |F| < |A|.

Applying the operation of replacement by an equivalent formula using the 10th formula
of Lemma 1, we’ll get the following form for our l formulas:

C1 = d2 ⊃ (d3 ⊃ ... ⊃ (dm ⊃ (d1 ⊃ (d11 ⊃ ... ⊃ (d
1
m1

⊃ (U1 ⊃ ... ⊃ ¬Uk))...)))...)
C2 = d2 ⊃ (d3 ⊃ ... ⊃ (dm ⊃ (d1 ⊃ (d21 ⊃ ... ⊃ (d

2
m2

⊃ (U1 ⊃ ... ⊃ ¬Uk))...)))...)
...

Cl = d2 ⊃ (d3 ⊃ ... ⊃ (dm ⊃ (d1 ⊃ (dl1 ⊃ ... ⊃ (d
l
ml

⊃ (U1 ⊃ ... ⊃ ¬Uk))...)))...)

At this point, we’ve reduced the proof of A to the proof of C1 ∧C2 ∧ ...∧Cl polynomially.
Applying the operation of replacement by an equivalent formula using the 9th formula

of Lemma 1, we’ll get:

C1 ∧ C2 ∧ ... ∧ Cl ≡ d2 ⊃ (d3 ⊃ ... ⊃ (dm ⊃ (C′1 ∧ C
′
2 ∧ ... ∧ C

′
l))...)

where

C′1 = (d1 ⊃ (d
1
1 ⊃ ... ⊃ (d

1
m1

⊃ (U1 ⊃ ... ⊃ ¬Uk))...))
C′2 = (d1 ⊃ (d

2
1 ⊃ ... ⊃ (d

2
m2

⊃ (U1 ⊃ ... ⊃ ¬Uk))...))
...

C′l = (d1 ⊃ (d
l
1 ⊃ ... ⊃ (d

l
ml

⊃ (U1 ⊃ ... ⊃ ¬Uk))...))
Applying the operation of replacement by an equivalent formula using the 5th formula

of Lemma 1, we’ll get the following form for above formulas:

C′1 = d1 ∧ d
1
1 ∧ ... ∧ d

1
m1

⊃ (U1 ⊃ ... ⊃ ¬Uk)
C′2 = d1 ∧ d

2
1 ∧ ... ∧ d

2
m2

⊃ (U1 ⊃ ... ⊃ ¬Uk)
...

C′l = d1 ∧ d
l
1 ∧ ... ∧ d

l
ml

⊃ (U1 ⊃ ... ⊃ ¬Uk)



70 On Proof Complexity of Some Type of Tautologies

Applying the operation of replacement by an equivalent formula using the 12th formula
of Lemma 1, we’ll get:

C′1 ∧ C
′
2 ∧ ... ∧ C

′
l ≡ (d1 ∧ d

1
1 ∧ ... ∧ d

1
m1

∨ d1 ∧ d21 ∧ ... ∧ d
2
m1

∨ ...∨
d1 ∧ dl1 ∧ ... ∧ d

l
m1

) ⊃ (U1 ⊃ ... ⊃ ¬Uk)

Let’s prove that the DNF generated above - (d1 ∧ d11 ∧ ... ∧ d1m1 ∨ d1 ∧ d
2
1 ∧ ... ∧ d2m1 ∨ ... ∨

d1 ∧ dl1 ∧ ... ∧ dlm1) is an sat formula.
As we can see, each of the conjunctions includes d1. Note that we can clearly split the

DNF into two subDNF’s - one generated from F1 and the other generated from F2. For
each of F1 and F2, we repeated the same process and so if the generated DNFs from F1 and
F2 are both sat formulas, then the DNF generated above is also an sat formula. Note that
we can make the assumption above, as after finite repetitions of splitting operation, we’ll
reach a literal, which is an sat formula.

At this point, we have polynomially reduced the proof of tautology A to the proof of the
following tautology:

d2 ⊃ (d3 ⊃ ... ⊃ (dm ⊃ (d1 ∧ d11 ∧ ... ∧ d
1
m1

∨ d1 ∧ d21 ∧ ... ∧ d
2
m1

∨ ...∨
d1 ∧ dl1 ∧ ... ∧ d

l
m1

) ⊃ (U1 ⊃ ... ⊃ ¬Uk)...)

By deduction theorem the proof of the above formula is equivalent to the following proof:

d2, ..., dm, (d1 ∧ d11 ∧ ... ∧ d
1
m1

∨ d1 ∧ d21 ∧ ... ∧ d
2
m1

∨ ...∨
d1 ∧ dl1 ∧ ... ∧ d

l
m1

) ⊢ (U1 ⊃ ... ⊃ ¬Uk)...)

Note that all the hypotheses are sat formulas and that we can repeat all the previous
steps on formula (U1 ⊃ ... ⊃ ¬Uk) even though we have some hypotheses. Repeating this
process, the proof of A will be reduced to the proof of the following formula:

T1 ∧ T2 ∧ ... ∧ Tn ⊃ c1,

where Ti(1 ≤ i ≤ n) are sat formulas and c1 is a literal. Note that new Ti-s are generated
only when we consider the last sub-formula of A and then remove it for the next step, so
this guarantees that n ≤ |A|.

Applying the operation of replacement by an equivalent formula using the 1st formula of
Lemma 1, we’ll get:

T1 ∧ T2 ∧ ... ∧ Tn ⊃ c1 ≡ (c1 ⊃ (T1 ∧ T2 ∧ ... ∧ Tn ⊃ c1)) ∧ (¬c1 ⊃ (T1 ∧ T2 ∧ ... ∧ Tn ⊃ c1))

The tautology (c1 ⊃ (T1 ∧ T2 ∧ ... ∧ Tn ⊃ c1)) has a polynomially bounded proof.
We reduced the proof of A to the proof of (¬c1 ⊃ (T1 ∧ T2 ∧ ... ∧ Tn ⊃ c1)). Applying the

operation of replacement by an equivalent formula using the 3rd formula of Lemma 1, we’ll
get:

A ≡ ¬(T1 ∧ T2 ∧ ... ∧ Tn)

All the operations have polynomial complexity. The number of steps is also polynomially
bounded, so the total complexity of reduction is polynomially bounded.



V. Altunyan and G. Petrosyan 7 1

4 . Co n c lu s io n

In t h is wo r k, we in t r o d u c e d sat fo r m u la s a n d r e d u c e d t h e p r o o fs o f t a u t o lo g ie s c o n t a in in g
o n ly ¾ a n d : s ym b o ls , wh e r e : is u s e d o n ly in lit e r a ls , t o t h e p r o o fs o f sat-constructed
t a u t o lo g ie s in p o lyn o m ia lly b o u n d e d n u m b e r o f s t e p s a n d le n g t h . In ve s t ig a t io n o f p r o o f
c o m p le xit ie s o f sat-constructed t a u t o lo g ie s is in p r o c e s s .

R e fe r e n c e s

[1 ] S . A . Co o k a n d A . R . R e c kh o w, \ Th e r e la t ive e ± c ie n c y o f p r o p o s it io n a l p r o o f s ys t e m s " ,
J ournal of Symbolic logic, vo l. 4 4 , p p . 3 6 -5 0 , 1 9 7 9 .

[2 ] L . S t r a s b u r g e r , \ E xt e n s io n wit h o u t Cu t " , Annals of P ure and Applied L ogic, vo l. 1 6 3 ,
n o . 1 2 , p p . 1 9 9 5 -2 0 0 7 , 2 0 1 2 .

[3 ] A . A . Ch u b a r ya n a n d G. V . P e t r o s ya n , \ S o m e n o t e s o n p r o o f c o m p le xit ie s in Fr e g e
s ys t e m s " , Sciences of E urope, vo l 1 . # 1 2 ( 1 2 ) , P h ys ic s a n d Ma t h e m a t ic s , p p . 3 1 { 3 4 ,
2 0 1 7 .

[4 ] J. N o r d s t r o m , \ N a r r o w p r o o fs m a y b e s p a c io u s : S e p a r a t in g s p a c e a n d wid t h in r e s o -
lu t io n " , SIAM J ournal on Computing, vo l. 3 9 , n o . 1 , p p . 5 9 -1 2 1 , 2 0 1 9 .

Submitted 08.09.2021, accepted 18.11.2021.

àñáß ïÇåÇ ÝáõÛݳµ³ÝáõÃÛáõÝÝ»ñÇ ³ñï³ÍÙ³Ý
µ³ñ¹áõÃÛáõÝÝ»ñÇ í»ñ³µ»ñÛ³É

ì³Ñ³·Ý Ü. ²ÉÃáõÝÛ³Ý ¨ ¶³ñÇÏ ì. ä»ïñáëÛ³Ý

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

e-mail: altunyanv@gmail.com, garik.petrosyan.1@gmail.com

²Ù÷á÷áõÙ

²Ûë Ñá¹í³ÍáõÙ áõëáõÙݳëÇñíáõÙ »Ý ³ñï³ÍÙ³Ý µ³ñ¹áõÃÛáõÝÝ»ñÁ ѳïáõÏ ïÇåÇ
ÝáõÛݳµ³ÝáõÃÛáõÝÝ»ñÇ Ñ³Ù³ñ, áñáÝù Ýϳñ³·ñíáõÙ »Ù áñå»ë ÇÙåÉÇϳódzݻñáí
¨ ÉÇï»ñ³ÉÝ»ñáí ϳ½Ùí³Í ÝáõÛݳµ³ÝáõÃÛáõÝÝ»ñ: سëݳíáñ³å»ë ³å³óáõóí»É ¿,
áñ ³Û¹ ï»ëùÇ ÝáõÛݳµ³ÝáõÃÛáõÝ»ñÇ ³ñï³ÍáõÙÝ»ñÁ µ³½Ù³Ý¹³Ùáñ»Ý ѳݷ»óíáõÙ
»Ý Ý߳ݳ÷áË Í³é»ñáí Ý»ñϳ۳óíáÕ ÝáõÛݳµ³ÝáõÃÛáõÝ Ñ³Ý¹Çë³óáÕ µ³Ý³Ó¨»ñÇ
³ñï³ÍáõÙÝ»ñÇÝ:

´³Ý³ÉÇ µ³é»ñ՝ üñ»·»Ç ѳٳϳñ·»ñ, ÝáõÛݳµ³ÝáõÃÛáõÝÝ»ñ, Ý߳ݳ÷áË Í³é»ñ,
³ñï³ÍÙ³Ý µ³ñ¹áõÃÛáõÝ:



7 2 On Proof Complexity of Some Type of Tautologies

Î ñëîæíîñòè âûâîäîâ íåêîòîðîãî òèïà òàâòîëîãèé

Âààãí Í. Àëòóíÿí è Ãàðèê Â. Ïåòðîñÿí

Åðåâàíñêèé ãîñóäàðñòâåííûé óíèâåðñèòåò
e-mail: altunyanv@gmail.com, garik.petrosyan.1@gmail.com

Àííîòàöèÿ

 íàñòîÿùåé ñòàòüå èññëåäîâàíû ñëîæíîñòè âûâîäîâ òàâòîëîãèé ñïåöèàëüíîãî
âèäà, êîòîðûå ìîæíî îïèñàòü êàê òàâòîëîãèè ñîñòîÿùèå èç èìïëèêàöèé è
ëèòåðàëîâ.  ÷àñòíîñòè, äîêàçàíî, ÷òî âûâîäû òàâòîëîãèé òàêîãî âèäà ìîæíî
ïîëèíîìèàëüíî ñâåñòè ê âûâîäàì òàâòîëîãèé, êîòîðûå ÿâëÿþòñÿ ôîðìóëàìè,
îïèñûâàåìûìè çíàêîïåðåìåííûìè äåðåâüÿìè.

Êëþ÷åâûå ñëîâà: ñèñòåìû Ôðåãå, òàâòîëîãèè, çíàêîïåðåìåííûå äåðåâüÿ,
ñëîæíîñòü âûâîäà.


	06_Altunyan_56
	5555