Mathematical Problems of Computer Science 53, 14–20, 2020.

UDC 510.6

Investigation of Monotonous Properties for Frege

Systems

Arsen A. Hambardzumyan

Yerevan State University

e-mail: arsen.hambardzumyan2@ysumail.am

Abstract

In this paper, we investigate the relations between the Frege proof lines of minimal
tautologies and the results of substitutions in them. We show that there is a sequence
of tautologies ψn, each of which has a unique minimal tautology ϕn, such that for every
n the Frege proof lines of ϕn are an order more than the Frege proof lines for ψn.

Keywords: Minimal tautology, Frege systems, Proof lines, Monotonous and strong
monotonous of proof systems.

1. Introduction

The minimal tautologies play a main role in the proof complexity area. Really, all propo-
sitional formulas, the proof complexities of which are investigated in many well-known pa-
pers, are minimal tautologies. There is a traditional assumption that a minimal tautology
shouldn’t be more complicated than any substitution in it. This idea was first revised by
Anikeev in [1]. He introduced the notion of a monotonous proof system and gave examples
of monotonous and non-monotonous systems, but both of them are not complete systems.
In [2]-[5], the notion of strongly monotonous systems for propositional proof systems is ad-
ditionally introduced and the properties of monotonous and strongly monotonous for many
propositional proof systems of classical and non-classical logics are investigated. Some of the
investigated systems (resolution systems, cut-free sequent systems) are monotonous systems,
in each of which the proof lines of all minimal tautologies are not more than the proof lines
for the results of substitutions in them. Some others are not monotonous (systems based on
the splitting method, elimination systems), the proof lines of some substituted formulas in
each of which can be less than the proof lines of some corresponding minimal tautologies.
It was proved that Frege systems are not strongly monotonous, but the question of mono-
tonicity of Frege systems still remained open. In this paper we prove that Frege systems are
not monotonous: it is shown that there is a sequence of tautologies ψn, each of which has a
unique minimal tautology ϕn, such that for every n the Frege proof lines of ϕn are an order
more than the Frege proof lines of ψn.

14



A. Hambardzumyan 15

2. Preliminaries

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

Definition 1: 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.

In the theory of proof complexity, one of the main characteristics of the proof is t-
complexity, defined as the number of proof steps. Let φ be a proof system and ϕ be a
tautology. We denote by tφϕ the minimal possible value of t-complexity for all φ-proofs of the
tautology ϕ.

Definition 2: Two proof systems are called t-linearly equivalent if any proof in one system
can be modified to a proof of the same tautology in another system, so that the t-complexity
of the proof is increased not more than linearly.

In [6], it is proved that all Frege systems are t-linearly equivalent.
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 only logical connectives ¬,⊃ and assume that ∨ and & are presented in traditional
ways through ¬,⊃. We assume that F has the well-known inference rule modus ponens.

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: A tautology is called minimal if the replacement result of all occurrences for
each of its non-elementary subformulas by some new variable is not a tautology.

We denote by S(ϕ) the set of all formulas, every of which is the result of some substitution
in a minimal tautology ϕ.

Definition 4: The proof system φ is called t-monotonous if for every tautology ψ there is a
minimal tautology ϕ, such that ψ ∈ S(ϕ) and tφϕ = t

φ
ψ.

Definition 5: The proof system φ is called t-strongly monotonous if for every tautology ψ
there is no minimal tautology ϕ, such that ψ ∈ S(ϕ) and tφϕ > t

φ
ψ.

3. Main Results

Here we give the main theorem, but first we should give the following auxiliary statements.

Lemma 1: Let P(A) be a tautology, A be some of its subformulas of size n, and P(A) not
contain q. There is a modified image of the subformula A to A′(q), and there are not more
than 2n Ti(q) tautologies that can be proved in a constant number of steps, so that no minimal
tautology can be obtained from P ′(A′,q) = (q ⊃ P(A′(q)))&T1(q)& . . . &Ti(q)& . . . tautology
by replacing with new variables neither any of the formulas A′(q),T1(q), . . . ,Ti(q), . . ., nor
their non-elementary subformulas.



16 Investigation of Monotonous Properties for Frege Systems

Proof:
Let’s describe the modification of each subformula U of A, while we will add new con-

juncts, i.e., Ti(q)s.

1. If U is a variable, then its modification is itself U ′ = U. No conjunct will be added.

2. If U = (U1 ⊃ U2), and q is true(1), then U is equivalent to (U1 ⊃ (q ⊃ U2)). The mod-
ified image of U will be U ′ = (U ′1 ⊃ (q ⊃ U ′2)), where U ′1 and U ′2 are modified images of
U1 and U2, correspondingly. We will add new conjuncts ((¬q) ⊃ (U ′1 ⊃ (q ⊃ U ′2))) and
((¬q) ⊃ (q ⊃ U ′2)). If we replace (U ′1 ⊃ (q ⊃ U ′2)) in P ′, then ((¬q) ⊃ (U ′1 ⊃ (q ⊃ U ′2)))
will not remain a tautology. If we replace (q ⊃ U ′2), then ((¬q) ⊃ (q ⊃ U ′2)) will not
remain a tautology.

3. If U = (¬U1), then we should modify U1 to U ′1. The modified image of U will
be U ′ = (¬U ′1). Then we add (U ′1 ⊃ (¬(¬U ′1))) in case U ′1 is a tautology, and
((¬(¬U ′1)) ⊃ U ′1) otherwise as a conjunct. If we replace (¬U ′1) or (¬(¬U ′1)) in P ′,
then the added conjunction won’t remain a tautology.

We can replace U ′1 in case of ¬, and U ′1 and U ′2 in the case of ⊃ in added conjuncts,
but P ′(A′,q) won’t remain a tautology, because the corresponding conjuncts were added to
P ′, which won’t allow replacing these formulas. The necessity of the given modifications is
presented in Appendix A.

We will add q ⊃ to P(A′(q)) because we assumed q is true(1) when modifying ⊃.
So, no minimal can be obtained by replacing any subformula of A or Ti(q) in

(q ⊃ P(A′(q)))& . . . &Ti(q) . . .. Lemma 1 is proved.

Lemma 2: For any formula A of size n, there exists a proof of q ` A′(q) ⊃ A with O(n)
steps.

Proof: For any (U1 ⊃ (q ⊃ U2))
1. ` (q ⊃ ((U1 ⊃ (q ⊃ U2))) ⊃ (U1 ⊃ U2))
2. ` ((U1 ⊃ (q ⊃ U2)) ⊃ (U1 ⊃ U2)) Modus ponens of premise q and 1.
3. ` (q ⊃ ((U1 ⊃ U2) ⊃ (U1 ⊃ (q ⊃ U2))))
4. ` ((U1 ⊃ U2) ⊃ (U1 ⊃ (q ⊃ U2))) Modus ponens of premise q and 3.
...
X1 ` (A′ ⊃ A) from the resulting equivalences using the replacement theorem (Replace-

ment Theorem 6 [7]) and taking into account that the following formulas are tautologies:

((D ∼ D′) ⊃ ((C ∼ C′) ⊃ ((D ⊃ C) ⊃ (D′ ⊃ C′)))),

((D ∼ D′) ⊃ ((¬D) ∼ (¬D′))).
Using constant proofs of each of these tautologies and constructing A step by step con-

necting to two equivalent formulas, not the old ones, but equivalent formulas, X1 = O(n).
Lemma 2 is proved.

Consider the formula P = A∨ (p ⊃ p), where p,q,t,r are not present in A.
Obviously, t∨ (p ⊃ p) is minimal of P. If A is a minimal tautology, then A ∨ r is also

minimal of P .
We can construct P ′ applying Lemma 1 to P :

P ′(A′(q)) = (q ⊃ (A′(q) ∨ (p ⊃ p)))& . . . &Ti(q)& . . .



A. Hambardzumyan 17

It’s obvious that P ′ can be proved in O(n) steps and its only minimal is as follows:

M(q,r,A) = (q ⊃ (A′(q) ∨ r))& . . . &Ti(q)& . . .

Suppose it can be proved in f(n) steps. The following three tautologies can be proved in
at most f(n) steps.

(q ⊃ (A′(q) ∨ (¬r)))& . . . &Ti(q)& . . .
((¬q) ⊃ (A′(¬q) ∨ r))& . . . &Ti((¬q))& . . .

((¬q) ⊃ (A′(¬q) ∨ (¬r)))& . . . &Ti((¬q))& . . .
Now we can prove that t

φ
A = O(t

φ
M + |A|) for any minimal tautology A. To do this, we

will use the deduction theorem, which will linearly increase the t-complexity of proof. Now
we will show O(t

φ
M + |A|) step proof of (¬r),q ` A.

(¬r),q `
...
Step t

φ
M . ` M. Using the shortest proof of M from the empty set of premises.

Step t
φ
M + 1. ` (q ⊃ (A′ ∨ r)). By removing & in M.

Step t
φ
M + 2. ` q. It’s a premise.

Step t
φ
M + 3. ` (A′ ∨ r). Using the modus ponens rule for t

φ
M + 2 and t

φ
M + 1.

Step t
φ
M + 4. ` ((¬r) ⊃ (A′ ∨ r) ⊃ A′). It’s a tautology of form ((¬r) ⊃ (a∨ r) ⊃ a)

Step t
φ
M + 5. ` (¬r). It’s a premise.

Step t
φ
M + 6. ` ((A′ ∨ r) ⊃ A′). Using modus ponens for t

φ
M + 5 and t

φ
M + 4.

Step t
φ
M + 7. ` A′. Using modus ponens for t

φ
M + 3 and t

φ
M + 6.

Step t
φ
M + CA. (A

′ ⊃ A). From Lemma 2.
Step t

φ
M + CA + 1. A. Using modus ponens for t

φ
M + 7 and t

φ
M + CA, where CA = O(|A|)

by Lemma 2.
We can prove the following with the same number of steps:

(¬r), (¬q) `((¬q) ⊃ (A′(¬q) ∨ r))& . . . &Ti(¬q)& . . .

(¬(¬r)),q ` (q ⊃ (A′(q) ∨ (¬r)))& . . . &Ti(q)& . . .
(¬(¬r)), (¬q) ` ((¬q) ⊃ (A′(¬q) ∨ (¬r)))& . . . &Ti(¬q)& . . .

Now, using the deduction rule, we can state that there is an O(|A| + f(n)) step proof of
the following 4 formulas

(q ⊃ ((¬r) ⊃ A))
((¬q) ⊃ ((¬r) ⊃ A))
(q ⊃ ((¬(¬r)) ⊃ A))

((¬q) ⊃ ((¬(¬r)) ⊃ A))
From the first two, we will get ((¬r) ⊃ A) in a constant number of steps. From the third

and forth, we will get ((¬(¬r)) ⊃ A) in a constant number of steps. From these two we get
A with a constant number of steps. So, we got a proof of A with O(|A| + tφM ) steps. Note
that the proof of (q ⊃ ((¬r) ⊃ A)) has been used 4 times.

There exists a sequence of formulas Ai, such that t
φ
Ai

= Ω(
|Ai|3/2
log3

2
(|Ai|)

) by [8]. By the proof

above, the following holds t
φ
Ai

= O(|Ai| + t
φ
Mi

), where Mi is the only minimal of P
′(A′i).



18 Investigation of Monotonous Properties for Frege Systems

From the above two estimates we can state that t
φ
Mi

= Ω(
|Ai|3/2
log3

2
(|Ai|)

). Using the Lemma 1, the

derivation of P ′(A′i) is O(|Ai|). Of these two, we can say that the only minimal of P ′(A′i) is
proved in more steps than the tautology itself for some i. Thus, the Frege system φ is not
monotonous.

So, the following was proved:

Theorem 1: Frege systems are not t-monotonous, and consequently, are not t-strongly
monotonous.

4. Conclusion

We prove, that Frege systems are not t-monotonous and, as consequence neither t-strongly
monotonous. As we state above that all the investigated proof systems are not t-strongly
monotonous, then the question of the existence of t-strongly monotonous systems still re-
mains open.

5. Acknowledgement

This work was supported by the RA MES State Committee of Science within the framework
of the research project 18T-1B034. I am grateful to my supervisor, professor of YSU Anahit
Chubaryan for her encouragement and fruitful discussions, and also for helpful suggestions,
which improved and expanded the results.

6. Appendix A

Let’s show that the modifications in Lemma 1 need to be made in each subformula of A,
but not only in A, in the example of P(A) = A∨ (p ⊃ p).

Suppose A = ((a ⊃ b) ⊃ ((¬b) ⊃ (¬a)))
After the modifications only in the outer implication, the resulting formula will be as

follows:

P ′ = (q ⊃ ((a ⊃ b) ⊃ (q ⊃ ((¬b) ⊃ (¬a)))) ∨ (p ⊃ p))
&((¬q) ⊃ ((a ⊃ b) ⊃ (q ⊃ ((¬b) ⊃ (¬a)))))
&((¬q) ⊃ (q ⊃ ((¬b) ⊃ (¬a))))

Let’s replace the formulas (a ⊃ b) and ((¬b) ⊃ (¬a)) in P ′ with t,r correspondingly. The
resulting formula will be:

M ′ = (q ⊃ (t ⊃ (q ⊃ r)) ∨ (p ⊃ p))
&((¬q) ⊃ (t ⊃ (q ⊃ r)))
&((¬q) ⊃ (q ⊃ r))

The resulting tautology M ′ is minimal. Thus, P ′ hasn’t unique minimal, as stated in
theorem. So, the modification in every subformula in formula A is necessary.



A. Hambardzumyan 1 9

References

[1 ] À. Ñ. Àíèêååâ, Î íåêîòîðîé êëàññèôèêàöèè âûâîäèìûõ ïðîïîçèöèîíàëüíûõ
ôîðìóë, Ìàòåìàòè÷åñêèå çàìåòêè, ò. 11, í. 2, ññ. 165-174, 1 9 7 2 .

[2 ] Ã. Ì. Çîãðàáÿí, Ñ. Ì. Ñàÿäÿí è À. À. ×óáàðÿí, Èññëåäîâàíèå ñâîéñòâà
ìîíîòîííîñòè íåêîòîðûõ ïðîïîçèöèîíàëüíûõ ñèñòåì âûâîäîâ êëàññè÷åñêîé
è íåêëàññè÷åñêèõ ëîãèê, ÄÍÀÍ ÐÀ, ò. 119, í. 1, ññ. 33-39, 2019.

[3 ] A . Ch u b a r ya n , A . K a r a b a kh t s ya n a n d G. P e t r o s ya n , \ S o m e P r o p e r t ie s o f S e ve r a l P r o o f
S ys t e m s fo r In t u it io n is t ic , Jo h a n s s o n s a n d Mo n o t o n e P r o p o s it io n a l L o g ic s " , J ournal of
Asian Scienti¯c R esearch, vo l. 8 , n o . 2 , p p . 6 1 -7 2 , 2 0 1 8 .

[4 ] A. A. Aìáàðöóìÿí, Ã. À. Ãàñïàðÿí, Ñ.À. Îâàííèñÿí è À. À. ×óáàðÿí,
Î êîëè÷åñòâå ìèíèìàëüíûõ òàâòîëîãèé è ñâîéñòâàõ èõ âûâîäîâ â ðÿäå
ñèñòåì êëàññè÷åñêîé è íåêëàññè÷åñêèõ ëîãèê,Ìàòåìàòè÷åñêèå âîïðîñû
êèáåðíåòèêè è âû÷åñëèòåëüíîé òåõíèêè, ò. 52, ññ. 66-73, 2019.

[5 ] À. À. ×óáàðÿí, A. A. Aìáàðöóìÿí, Ã. À. Ãàñïàðÿí è Ñ.À.
Îâàííèñÿí, Î íåêîòîðûõ ñâîéñòâàõ ìèíèìàëüíûõ òàâòîëîãèé êëàññè÷åñêîé
è íåêëàññè÷åñêèõ ëîãèê, Äîêëàäû ÍÀÍ ÐÀ, ò. 120, í. 1, ññ. 4-5, 2020.

[6 ] S . A . Co o k a n d R . A .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 " ,
The journal of symbolic logic, vo l. 4 4 , n o . 1 , p p . 3 6 -5 0 , 1 9 7 9 .

[7 ] S . C. K le e n e , Introduction to M etamathematics, V a n N o s t r a n d N e w Y o r k, 1 9 5 2 .

[8 ] A . A . Ch u b a r ya n , H . A . Ta m a z ya n a n d A . S . Ts h it o ya n , \ S o m e im p r o ve m e n t o f lo we r
b o u n d s fo r s t e p s a n d s iz e s o f p r o o fs in fr e g e s ys t e m s " , Sciences of E urope, vo l. 1 , n o .
3 7 , p p . 3 9 -4 4 , 2 0 1 9 .

Submitted 18.03.2020, accepted 26.06.2020.

ØáÝáïáÝáõÃÛ³Ý Ñ³ïÏáõÃÛ³Ý Ñ»ï³½áïáõÙ üñ»·»Ç ѳٳϳñ·»ñáõÙ

²ñë»Ý ². гٵ³ñÓáõÙÛ³Ý

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

e-mail: hambardzumyanarsen99@gmail.com

²Ù÷á÷áõÙ

êáõÛÝ ³ß˳ï³Ýùáõ٠ѻﳽáïí»É »Ý ÙÇÝÇÙ³É ÝáõÛݳµ³ÝáõÃÛáõÝÝ»ñÇ ¨ Ýñ³Ýó
Ù»ç ϳï³ñí³Í ï»Õ³¹ñáõÃÛáõÝÝ»ñÇ ³ñ¹ÛáõÝùÝ»ñÇ Ýí³½³·áõÛÝ ³ñï³ÍÙ³Ý ù³Û»ñÇ
ѳñ³µ»ñáõÃÛáõÝÁ üñ»·»Ç ѳٳϳñ·»ñáõÙ: ²å³óáõóí³Í ¿, áñ ·áÛáõÃÛáõÝ áõÝÇ ³ÛÝåÇëÇ
Ãn áã ÙÇÝÇÙ³É ÝáõÛݳµ³ÝáõÃÛáõÝÝ»ñÇ Ñ³çáñ¹³Ï³ÝáõÃÛáõÝ, áñáÝóÇó Ûáõñ³ù³ÝãÛáõñÝ áõÝÇ
ÙÇ³Ï ³ÛÝåÇëÇ ÙÇÝÇÙ³É 'n ÝáõÛݳµ³ÝáõÃÛáõÝ, áñ üñ»·»Ç ѳٳϳñ·»ñáõÙ í»ñçÇÝÝ»ñÇ
³ñï³ÍáõÙÝ»ñÇ Ýí³½³·áõÛÝ ù³ÛÉ»ñÇ ù³Ý³ÏÝ Áëï ϳñ·Ç ³í»ÉÇ Ù»Í ¿, ù³Ý Ãn
µ³Ý³Ó¨»ñÇ ³ñï³ÍáõÙÝ»ñÇ Ýí³½³·áõÛÝ ù³ÛÉ»ñÇ ù³Ý³ÏÁ:

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



2 0 Investigation of Monotonous Properties for Frege Systems

Èññëåäîâàíèå ñâîéñòâà ìîíîòîííîñòè ñèñòåì Ôðåãå

Àðñåí À. Àìáàðöóìÿí

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

Àííîòàöèÿ

 íàñòîÿùåé ðàáîòå äëÿ ñèñòåì Ôðåãå èññëåäîâàíî ñîîòíîøåíèå êîëè÷åñòâà
øàãîâ âûâîäîâ ìèíèìàëüíûõ òàâòîëîãèé è ðåçóëüòàòîâ ïîäñòàíîâêè â íèõ.
Äîêàçàíî, ÷òî ñóùåñòâóåò òàêàÿ ïîñëåäîâàòåëüíîñòü íåìèíèìàëüíûõ òàâòîëîãèé
Ãn, êàæäàÿ èç êîòîðûõ èìååò åäèíñòâåííóþ ìèíèìàëüíóþ 'n è äëÿ êàæäîãî n
êîëè÷åñòâî ìèíèìàëüíûõ øàãîâ âûâîäîâ â ñèñòåìàõ Ôðåãå ôîðìóë 'n íà ïîðÿäîê
áîëüøå êîëè÷åñòâà ìèíèìàëüíûõ øàãîâ âûâîäîâ â ñèñòåìàõ Ôðåãå ôîðìóë Ãn.

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


	02_Arsen_Hambardzumyan_53
	02