61 

 

Mathematical Problems of Computer Science 58, 61–66, 2022. 

doi: 10.51408/1963-0093 

 

 

 
    UDC 510.64 

 

Proof Complexity of Hard-Determinable Balanced 

Tautologies in Frege   Systems 

 

Anahit A. Chubarya 

Yerevan State University 

e-mail: achubaryan@ysu.am 

 

Abstract 

 
Hard-determinable property and balanced property of tautologies are specified as 

important properties in the study of proof complexities formerly. In this paper hard-
determinable and balanced properties are studied together. It is shown that some 

sequences of hard determinable balanced tautologies have polynomially bounded Frege 
proofs. 

Keywords: Hard-determinable tautologies, Balanced tautologies, Frege systems,  Proof 

complexity characteristics. 

Article info: Received 29 June 2022; accepted 29 September 2022. 

 

 

 

 

1. Introduction  
 

One of the most fundamental problems in proof complexity theory is to find an efficient proof 

system for classical propositional logic (CPL). 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 𝑝(𝑛) proof 
for every tautology of size 𝑛. In [1] Cook and Reckhow named such a system a supersystem. They 
showed that 𝑁𝑃 = 𝑐𝑜𝑁𝑃 iff there exists a supersystem. 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 polynomial bounded sizes for Frege proofs of all tautologies is reduced to an 

analogous question for a set of specific tautologies. In particular the hard-determinable tautologies 

and  balanced tautologies are  introduced in [2,3] as such sets of specific tautologies. In this paper, 

the hard-determinable and balanced properties are studied together and it is shown that some 

mailto:achubaryan@ysu.am


Proof Complexity of Hard-Determinable Balanced Tautologies in Frege Systems 62 

sequences of hard-determinable balanced tautologies have polynomial bounded Frege proofs. 

Using the notions and results of this paper and the results of [3-4] the above-mentioned statement 

of Cook and Reckhow can be rephrased as follows: 𝑁𝑃 = 𝑐𝑜𝑁𝑃 iff in some Frege system of CPL 
the proofs for all hard-determinable balanced formulas are polynomially bounded. 

 

2. Preliminaries 

 

To prove our main result, we recall some notions and notation.  We will use the  current concepts 

of the unit Boolean cube (𝐸𝑛), a propositional formula, a tautology, a proof system for CPL, and 
proof complexity. The particular choice of a language for presenting propositional formulas is 

immaterial in this consideration. However, because of some technical reasons we assume that the 

language contains propositional variables, denoted by small Latin letters with indices. Logical 

connectives ¬, &, ∨, ⊃, and parentheses ( , ). Note that some parentheses can be omitted in 
generally accepted cases. 

 

2.1. Hard-determinable and Balanced Tautologies 

Following the usual terminology we call the variables and negated variables literals.  

The conjunct 𝐾 (clause) can be represented simply as a set of literals (no conjunct contains a 
variable and its negation simultaneously).  

In [3] the following notion is introduced.  

We call each of the following trivial identities for a propositional formula ψ a replacement-rule: 

 

0&ψ = 0,   ψ&0 = 0,   1&ψ = ψ,  ψ&1 = ψ,  ψ&ψ = ψ, ψ&¬ψ = 0, ¬ψ&ψ = 0, 

0∨ ψ =ψ, ψ∨ 0=ψ, 1∨ψ =1, ψ∨1 =1, ψ∨ψ = ψ, ψ∨¬ ψ =1, ¬ψ∨ψ=1, 

0⊃ψ=1, ψ⊃0=¬ψ, 1⊃ψ =ψ, ψ⊃1=1, ψ⊃ψ =1, ψ⊃¬ψ = ¬ψ, ¬ψ⊃ ψ = ψ, 

¬0 = 1, ¬1 = 0, ¬¬ψ = ψ. 

Application of a replacement rule to certain word consists in replacing some its subwords, having 

the form of the left-hand side of one of the above identities by the corresponding right-hand side. 

Let 𝜑 be a propositional formula, let 𝑃 = {𝑝1, 𝑝2, … , 𝑝𝑛} be the set of the variables of 𝜑, and let 
𝑃′ = {𝑝𝑖1 , 𝑝𝑖2 , … , 𝑝𝑖𝑚 } (1 ≤ 𝑚 ≤ 𝑛) be some subset of 𝑃. 
 

Definition 1: Given 𝜎 = {𝜎1, 𝜎2, … , 𝜎𝑚} ∈ 𝐸
𝑚, the conjunct 𝐾𝜎 = {𝑝𝑖1

𝜎1 , 𝑝𝑖2
𝜎2 , … , 𝑝𝑖𝑚

𝜎𝑚 }  is called 𝜑-

determinative if assigning 𝜎1 (1 ≤ 𝑗 ≤ 𝑚) to each 𝑝𝑖𝑗 and successively using replacement rules 

we obtain the value of 𝜑 (0 or 1) independently of the values of the remaining variables.  
 

Definition 2: We call the minimal possible number of variables in a 𝜑-determinative conjunct 
the determinative size of 𝜑 and denote it by ds(𝜑). 
 

By | 𝜑| we denote the size of the formula 𝜑, defined as the number of all logical signs 
entries in it. It is obvious that the full size of the formula, which is understood to be the number 

of all symbols is bounded by some linear function in |𝜑 |. 
 

Definition  3: For sufficiently large 𝑛 the tautologies 𝜑𝑛  are called hard-determinable if there is 
some constant c such that 𝑙𝑜𝑔|𝜑𝑛|𝑑𝑠(𝜑𝑛) → 𝑐 for 𝑛 → ∞.  

Definition  4: A formula 𝜑 is balanced if every propositional variable  occurring in 𝜑 occurs 
exactly twice, once positive and once negative. 
 



A. Chubaryan 63 

Example 1. The tautologies 𝜑𝑛 = 𝑝1 ⊃ (𝑝1 ⊃ (𝑝2 ⊃ (¬𝑝2 ⊃ (… ⊃ (𝑝𝑛 ⊃ 𝑝𝑛 ) … ))))  
  are balanced. It is not difficult to see that 𝑑𝑠(𝜑𝑛) = 1, hence 𝜑𝑛  are not  hard-determinable.  

Example 2. The tautologies 𝑄𝐻𝑄𝑛 = 𝑉0≤𝑖≤𝑛 &1≤𝑗≤𝑛 [𝑉1≤𝑘≤𝑖 �̅�𝑖,𝑗,𝑘 ∨ 𝑉𝑖<𝑘≤𝑛 𝑞𝑘,𝑗,𝑖+1](𝑛 ≥ 1), are 

balanced. Put 𝑄𝑖,𝑗 = 𝑉1≤𝑘≤𝑖 �̅�𝑖,𝑗,𝑘 ∨ 𝑉𝑖<𝑘≤𝑛𝑞𝑘,𝑗,𝑖+1(𝑛 ≥ 1, 0 ≤ 𝑖 ≤ 𝑛, 1 ≤ 𝑗 ≤ 𝑛), then 𝑄𝐻𝑄𝑛 =

𝑉0≤𝑖≤𝑛(𝑄𝑖1&𝑄𝑖2& … &𝑄𝑖𝑗 & … &𝑄𝑖(𝑛−1)&𝑄𝑖𝑛) and therefore 𝑑𝑠(𝑄𝐻𝑄𝑛). It is not difficult to see, 

that |𝑄𝐻𝑄𝑛| =
3𝑛2(𝑛+1)

2
− 1 |, hence 𝑄𝐻𝑄𝑛   are hard-determinable as well. 

 

2.2. Proof  Systems and Proof Complexities 
 

 Let us recall some notions from [1]. 

A Frege system  𝓕 uses a denumerable set of propositional variables, a finite, complete set of 
propositional connectives; 𝓕 has a finite set of inference rules defined by a figure of the form  
𝐴1𝐴2… 𝐴𝑚

𝐵
 (the rules of inference with zero hypotheses are the schemes of axioms); 𝓕 must be 

sound and complete, i.e. for each rule of inference 
𝐴1𝐴2… 𝐴𝑚

𝐵
  every truth-value assignment, 

satisfying 𝐴1𝐴2 …  𝐴𝑚, also satisfies 𝐵, and 𝓕 must prove every tautology. 
       In the theory of proof complexity two main characteristics of the proof are:  𝑙 – 
 complexity to  be the size of a proof (= the sum of all formulae sizes) and  𝑡 – complexity to 
 be its length (= the total number of lines). The minimal 𝑙 – complexity (𝑡 – complexity) of a 

 formula 𝜑 in a proof system Φ we denote by 𝑙𝜑
Φ(𝑡𝜑

Φ).  

The polynomial equivalence (𝑝 − 𝑙 --equivalence, 𝑝 − 𝑡 --equivalence) of two proof 

systems by some proof complexity measure means that the transformation of any proof in one 

system into a proof in another system can be performed with no more than polynomial increase of 

proof complexity measure.  

It is well known that any two Frege systems are 𝑝 − 𝑙 -equivalent (𝑝 − 𝑡 -equivalent). 

        Let 𝑀 be some set of tautologies. 
 

Definition 5: We call the Ф-proofs of tautologies from the set 𝑀 𝑡 -polynomially (𝑙 – poly-

nomially) bounded if there is a polynomial 𝑝() such that 𝑡𝜑
𝛷 ≤ 𝑝(|𝜑|)(𝑙𝜑

𝛷 ≤ 𝑝(|𝜑|)) for all 𝜑 

from 𝑀. 

 

2.3. Former Results 
 

It was previously proven that  

a) tautologies without  hard-determinability condition have 𝑡 -polynomially (𝑙 - polynomially) 
bounded proofs in all systems of CPL [4],  

b) hard-determinability condition is sufficient (but not necessary) to obtain exponential lower  
bounds for both proof complexities of tautologies in  “weak” proof systems of CPL (Cut-

free sequent, Resolution, Cutting planes etc.) [4],  

c) hard-determinability condition is not sufficient for exponential lower  bounds of  proof 
complexities in Frege systems: for some examples of hard-determinable formulas the 𝑡 -
polynomially (𝑙 - polynomially)  bounded Frege-proofs  are given in [2]. 

Some proof systems of CPL (calculus of structures with deep inference rules), where the author 

considers only formulas in negation normal form, are studied in [3], where among the rest of the 

results it is proved that 



Proof Complexity of Hard-Determinable Balanced Tautologies in Frege Systems 64 

a) the set of above mentioned balanced formulas 𝑄𝐻𝑄𝑛 have polynomially bounded proofs 
in   one of the studied system 𝑠𝐾𝑆, 

b) the relations between the proof complexities in the system 𝑠𝐾𝑆 and the Frege systems are 
unknown for the present.  

 

3. Main Result 
 

Let 𝐹 be some Frege system with inference rule modus ponens.  
 

Theorem1: The 𝐹 -proofs of tautologies 𝑄𝐻𝑄𝑛 (𝑛 ≥ 1) are 𝑡-polynomially (𝑡-polynomially) 
bounded. 

To prove, we use the method of [2] for description of some polynomially bounded proof of 

𝑄𝐻𝑄𝑛 direct  in 𝐹 by reducing it to 𝐹 -proofs of well-known tautologies 
 

𝑃𝐻𝑃𝑛 = &0≤𝑖≤𝑛𝑉1≤𝑗≤𝑛 𝑝𝑖𝑗 ⊃ 𝑉0≤𝑖<𝑘≤𝑛 𝑉1≤𝑗≤𝑛(𝑝𝑖𝑗 &𝑝𝑘𝑗 )(𝑛 ≥ 1) 
 

presenting the Pigeonhole Principle . It is proved in [5] that the set of these formulas is t-

polynomially (𝑙- polynomially) bounded. 
  The following two auxiliary statements will be of use: 

 

Lemma 1: Given arbitrary formulas 𝛼, 𝛽, 𝛾, 𝛼𝑖, 𝛽𝑖, 𝛼𝑖𝑗  and 𝛽𝑖𝑗, the 𝐹-proofs of the following 

tautologies are 𝑡-polynomially (𝑙-polynomially) bounded: 
 

1) α ∨ α¯, 

2) (α ⊃ β) ⊃ ((β ⊃ γ) ⊃ (α ⊃ γ)), 

3) (β¯ ⊃ α) ⊃ (¯α ⊃ β), 

4) α1 ⊃ (α2 ⊃ (... ⊃ (αk ⊃ α1 &α2 &···&αk)...)) (k ≥ 2), 

5) α ∨ α¯ ⊃ β1 ∨···∨ βk∨α ∨ βk+1 ∨··· ∨ βk+r ∨ α¯ ∨ βk+r+1 ∨··· ∨ βk+r+t   
 (k ≥ 1, r ≥ 1, t ≥ 1), 

      6)  ¬(𝑉1≤𝑖≤𝑘 &1≤𝑗≤𝑚𝛼𝑖𝑗 ) ⊃ &1≤𝑖≤𝑘 𝑉1≤𝑗≤𝑚�̅�𝑖𝑗  (𝑘 ≥ 1, 𝑚 ≥ 1)  

      7)  &1≤𝑖≤𝑘 (𝛽1𝑖 ⋁𝛽2𝑖 ) ⊃ ¬(𝑉1≤𝑖≤𝑘 (�̅�1𝑖&�̅�2𝑖 )) (𝑘 ≥ 1). 
 

The proof is obvious. 
 

Lemma 2: Let 𝑄𝑖𝑗  and 𝑄𝑘𝑗 (0 ≤ 𝑖˂𝑘 ≤ 𝑛, 1 ≤ 𝑗 ≤ 𝑛) be the above denoted  subformulas of 

𝑄𝐻𝑄𝑛, then 𝐹-proofs of the formulas 𝑄𝑖𝑗 ∨ 𝑄𝑘𝑗  be 𝑡-polynomially (𝑙-polynomially) bounded. 
 

The proof follows from the fact of existence of some 𝑠 and 𝑚  (1 ≤ 𝑠 ≤ 𝑛, 1 ≤ 𝑚 ≤ 𝑛) such that  
𝑄𝑖𝑗  contains 𝑞𝑠𝑗𝑚 and 𝑄𝑘𝑗  contains ¬𝑞𝑠𝑗𝑚, and also from 1) and 5) of Lemma 1.  

From 6) of Lemma 1 we infer for the formula 𝑄𝑛 = 𝑉0≤𝑖≤𝑛 &1≤𝑗≤𝑛 𝑄𝑖𝑗 . 

Condition 1: The F-proofs of the formulas 

¬𝑄𝐻𝑄𝑛 ⊃ &0≤𝑖≤𝑛𝑉1≤𝑗≤𝑛¬𝑄𝑖𝑗  

are 𝑡-polynomially (𝑙-polynomially) bounded. 

Put 

 

                         𝑃𝐻𝑃𝑛
’

= &0≤𝑖≤𝑛 𝑉1≤𝑗≤𝑛¬𝑄𝑖𝑗 ⊃ 𝑉0≤𝑖<𝑘≤𝑛𝑉1≤𝑗≤𝑛¬(𝑄𝑖𝑗 &¬𝑄𝑘𝑗 )                          (1) 



A. Chubaryan 65 

 

The formulas (1) are obtained from the 𝑃𝐻𝑃𝑛  by the corresponding substitutions. Hence, 

Condition 2: The 𝐹-proofs of the formulas (1) are 𝑡-polynomially (𝑙-polynomially) bounded. 

Let     

           𝐴𝑛 = 𝑉0≤𝑖<𝑘≤𝑛 𝑉1≤𝑗≤𝑛(¬𝑄𝑖𝑗 & ¬𝑄𝑘𝑗).       
 

Using conditions (1), (2), and item 2) of Lemma 1, we obtain 

Condition 3: The 𝐹-proofs of the formulas ¬ 𝑄𝐻𝑄𝑛 ⊃ 𝐴𝑛   are 𝑡-polynomially (𝑙-polynomially) 
bounded. 
 

From Lemma 2 and item 4) of Lemma 1 we have 

Condition 4: The F-proofs of the formulas 

𝐵𝑛 = &0≤𝑖<𝑘≤𝑛 &1≤𝑗≤𝑛 (𝑄𝑖𝑗 ⋁𝑄𝑘𝑗 ) 

are 𝑡-polynomially (𝑙-polynomially) bounded, and from item 7) of Lemma 1 it follows that the 𝐹-
proofs of the formulas ¬𝐴𝑛,𝑚  are 𝑡-polynomially (𝑙-polynomially) bounded as well. 

From the conditions (3), (4), and item 3) of Lemma 1 we have a t-polynomial (l-polynomial) 

bound for the F-proofs of 𝑄𝑛  .  
 

Corollary1: There are hard-determinable balanced formulas the F-proofs of which are t-

polynomially (l-polynomially) bounded. 

        

4. Conclusion 

 

Using the polynomial equivalence of different Frege systems [1], the above mentioned result of 

Cook and Reckhow can be rephrased as follows: 𝑁𝑃 = 𝑐𝑜𝑁𝑃 iff in some Frege system of CPL the 
proofs for all hard-determinable balanced formulas are polynomially bounded. 

 

References 

 
[1] S. A. Cook and A. R. Reckhow, “The relative efficiency of propositional proof systems,” 

J. Symbolic Logic, vol. 44, pp. 36–50, 1979. 

[2] S. R. Aleksanyan and A. A. Chubaryan, “The polynomial bounds of proof complexity in 
Frege systems”, Siberian Mathematical Journal, Springer Verlag, vol. 50, no. 2, pp. 243-

249, 2009. 

[3] L. Sraßburger, “Extension without cut”, Annals of Pure and Applied Logic, vol.163, pp. 
1995- 2007, 2012. 

[4] A. A. Chubaryan, “Relative efficiency of a proof system in classical propositional logic,” 
Izv. NAN Armenii Mat., vol. 37, no. 5, pp. 71–84, 2002.  

[5] S. R. Buss, “Polynomial size proofs of the propositional pigeonhole principle,” Journal 
Symbolic Logic, vol. 52, pp. 916–927, 1987. 

 

 



Proof Complexity of Hard-Determinable Balanced Tautologies in Frege Systems 66 

Դժվար-որոշելի բալանսավորված նույնաբանությունների 

արտածումների բարդությունները  

Ֆրեգեի համակարգերում 

 
Անահիտ Ա. Չուբարյան 

Երևանի պետական համալսարան 

e-mail: achubaryan@ysu.am 

 

Ամփոփում 

       Նախկինում նույնաբանությունների դժվար-որոշելիության հատկությունը և 

բալանսավորված լինելու հատկությունը առանձնացվել էին որպես կարևոր 
հատկություններ արտածումների բարդությունների ուսումնասիրություններում:      
Այս հոդվածոմ դժվար-որոշելիության և բալանսավորված լինելու հատկությունները 
ուսումնասիրվում են համատեղ: Ապացուցվել է, որ դժվար-որոշելի բալանսավորված 

նույնաբանությունների մեկ դասի համար արտածումները Ֆրեգեի համակարգերում 

բազմանդամորեն սահմանափակ են:   

Բանալի բառեր՝ դժվար-որոշելի նույնաբանություններ, բալանսավորված 

նույնաբանություններ, Ֆրեգեի համակարգեր, արտածման բարդությունների 

բնութագրիչներ: 

 

Сложности выводов трудно-определяемых балансированных 

формул в системах Фреге 

        
Аанаит А. Чубарян 

Ереванский государственный университет 

e-mail: achubaryan@ysu.am 

 

Аннотация 

 

        Ранее свойство трудно-определяемости и свойство балансированности тавтологий 

были выдлены как важные свойства в исследованиях сложностей выводов. В настоящей 

статье свойства трудно-определяемости и балансированности изучаются совместно. 

Доказана полиномиальная ограниченность выводов в системах Фреге для некоторого 

класса трудно-определяемых балансированных формул. 

Ключевые слова: трудно-определяемые тавтологии, балансированные тавтологии, системы 
Фреге, характеристики сложностей выводов.   

mailto:achubaryan@ysu.am
mailto:achubaryan@ysu.am

	References