On an optimal propositional proof system and the structure of easy subsets of TAUT.
In this paper we develop a connection between optimal propositional proof systems and structural complexity theory--specifically, there exists an optimal propositional proof system if and only if there is a suitable recursive presentation of the class of all easy (polynomial time recognizable) subsets of TAUT. As a corollary we obtain the result that if there does not exist an optimal propositional proof system, then for every theory T there exists an easy subset of TAUT which is not T-provably easy.
Introduction
The first classification of propositional proof systems by their relative
efficiency was done by S. Cook and R. Reckhow [4] in 1979. The
key tool for comparing the relative strength of proof systems is p-
simulation. Intuitively a proof system h p-simulates a second one g if
there is a polynomial time computable function translating proofs in
into proofs in h. A propositional proof system is called p-optimal
if it p-simulates any propositional proof system. The question of the
existence of a p-optimal propositional proof system and its nondeterministic
counterpart, an optimal propositional proof system, posed
by J. Kraj'i-cek and P. Pudl'ak [9], is still open.
It is not known whether many-one complete languages for
exist. For these and other promise classes
no recursively enumerable representation of appropriate sets of Turing
machines is known. Moreover, J. Hartmanis, L. Hemachandra
in [5] and W. Kowalczyk in [7] pointed out that NP " co-NP and
UP possess complete languages if and only if there are recursive
enumerations of polynomial time clocked Turing machines covering
languages from these classes.
In this paper we show that the question of the existence of optimal
(p-optimal) propositional proof systems can be characterized in
a similar manner. The main result of our paper shows that optimal
proof systems for TAUT (the set of all propositional tautologies) exist
if and only if there is a recursive enumeration of polynomial time
clocked Turing machines covering all easy (recognizable in polynomial
time) subsets of TAUT . This means that the problem of the
existence of complete languages for promise classes and the problem
of the existence of optimal proof systems for TAUT , although
distant at first sight, are structurally similar. Since complete languages
for promise classes have been unsuccesfully searched for in
the past our equivalence gives some evidence of the fact that optimal
propositional proof systems might not exist.
Our result can be related to the already existing line of research
in computational complexity. After the revelation of the connection
between the existence of optimal proof systems and the existence of
many-one complete languages for promise classes in [12] and [15], this
subject has been intensively investigated. J. K-obler and J. Messner
in [8] formalized this relationship introducing the concept of test set,
and showed that the existence of p-optimal proof systems for TAUT
and for SAT (the set of all satisfiable boolean formulas) suffices
to obtain a complete language for NP " co-NP. J. Messner and
J. Tor'an showed in [12] that a complete language for UP exists in
case there is a p-optimal proof system for TAUT . We believe that our
results make the next step towards deeper understanding of this link
between optimal proof systems and complete languages for promise
classes.
The paper is organized as follows. In Section 2 we set down notation
that will be used throughout the paper. Background information
about propositional proof systems is presented in Section 3.
The problems of the existence of complete languages for the classes
" co-NP and UP and their characterization in terms of polynomial
time clocked machines covering languages from these classes
are presented in Section 4. In Section 5 we give a precise definition of
a family of propositional formulas which will be used in the proofs
of our main results. In Section 6 our main results are stated and
proved. In the last section we discuss corollaries arising from the
main results of the paper.
Preliminaries
We assume some familiarity with basic complexity theory, see [1].
The symbol \Sigma denotes, throughout the paper, a certain fixed finite
alphabet. The set of all strings over \Sigma is denoted by \Sigma ? . For a string
x, jxj denotes the length of x. For a language A ae \Sigma ? the complement
of A is the set of all strings that are not in A.
We use Turing machines (acceptors and transducers) as our basic
computational model. We will not distinguish between a machine
and its code. For a deterministic Turing machine M and an input w,
denotes the computing time of M on w. When M is
a nondeterministic Turing machine TIME(M , w) is defined only for
w's accepted by M and denotes the number of steps in the shortest
accepting computation of M on w. For a Turing machine M the
denotes the language accepted by M . The output of a
Turing transducer M on input w 2 \Sigma ? is denoted by M(w).
We consider deterministic and nondeterministic polynomial time
clocked Turing machines with uniformly attached standard
clocks which stop their computations in polynomial time (see [1]).
We impose some restrictions on our encoding of these machines.
From the code of any polynomial time clocked Turing machines we
can detect easily (in polynomial time) the natural k such that n k +k
is its polynomial time bound. Let D 1 , D 2 , D 3 , . and N 1 , N 2 , N 3 ,
. be, respectively, standard enumerations of all deterministic and
nondeterministic polynomial time clocked Turing machines.
Recall that the classes P, NP, co-NP are, respectively, the class
of all languages recognized by deterministic Turing machines working
in polynomial time, the class of all languages accepted by nondeterministic
Turing machines working in polynomial time and the class of
complements of all languages from NP. The symbol TAUT denotes
the set (of encodings) of all propositional tautologies over a fixed
adequate set of connectives, SAT denotes the set of all satisfiable
boolean formulas.
Finally, standard polynomial time computable
tupling function.
3 Propositional proof systems
The abstract notion of a propositional proof system was introduced
by S. Cook and R. Reckhow [4] in the following way:
Definition 1. A propositional proof system is a function f
\Gamma!
TAUT computable by a deterministic Turing machine in time bounded
by a polynomial in the length of the input.
A string w such that we call a proof of a formula ff.
A propositional proof system that allows short proofs to all tautologies
is called a polynomially bounded propositional proof system.
Definition 2. (Cook, Reckhow) A propositional proof system is polynomially
bounded if and only if there exists a polynomial p(n) such
that every tautology ff has a proof of length no more than p(jffj) in
this system.
The existence of a polynomially bounded propositional proof system
is equivalent to one of the most fundamental problems in complexity
theory.
Fact 1. (Cook, Reckhow) NP=co-NP if and only if there exists a
polynomially bounded propositional proof system.
S. Cook and R. Reckhow were the first to propose a program of
research aimed at attacking the NP versus co-NP problem by classifying
propositional proof systems by their relative efficiency and
then systematically studying more and more powerful concrete proof
systems (see [2]). A natural way for such a classification is to introduce
a partial order reflecting the relative strength of propositional
proof systems. It was done in two different manners.
Definition 3. (Cook, Reckhow) Propositional proof system P polynomially
simulates (p-simulates) propositional proof system Q if there
exists a polynomial time computable function f
that for every w, if w is a proof of ff in Q, then f(w) is a proof of
ff in P .
Definition 4. (Kraj'i-cek, Pudl'ak) Propositional proof system P simulates
propositional proof system Q if there exists a polynomial p such
that for every tautology ff, if ff has a proof of length n in Q, then ff
has a proof of length - p(n) in P .
Obviously p-simulation is a stronger notion than simulation. We
would like to pay attention to the fact that the simulation between
proof systems may be treated as a counterpart of the complexity-theoretic
notion of reducibility between problems. Analogously the
notion of a complete problem (a complete language) would correspond
to the notion of an optimal proof system. The notion of an
optimal propositional proof system was introduced by J. Kraj'i-cek
and P. Pudl'ak in [9] in two different versions.
Definition 5. A propositional proof system is optimal if it simulates
every other propositional proof system.
A propositional proof system is p-optimal if it p-simulates every other
propositional proof system.
The following open problem, posed by J. Kraj'i-cek and P. Pudl'ak
will be studied in our paper.
Open Problem:
(1) Does there exist an optimal propositional proof system?
(2) Does there exist a p-optimal propositional proof system?
The importance of these questions and their connection with the
NP versus co-NP problem is described by the following fact.
Fact 2. If an optimal (p-optimal) propositional proof system exists,
then NP=co-NP if and only if this system is polynomially bounded.
Complete languages for NP " co-NP and for UP
The classes NP " co-NP and UP are called promise classes because
they are defined using nondeterministic polynomial time clocked
Turing machines which obey special conditions (promises). The problem
whether a given nondeterministic polynomial time clocked Turing
machine indeed defines a language in any of these classes is undecidable
and because of this complete languages for these classes
are not known. Since there exist relativizations for which these two
classes have complete languages as well as relativizations for which
they do not the problems of the existence of complete languages for
seem to be very difficult.
It turns out that the existence of complete languages for these
classes depends on a certain structural condition on the set of machines
defining languages from these classes. Since this condition is
the chief motivation for our main theorems we survey known results
in this direction.
The class NP " co-NP is most often defined using complementary
pairs of nondeterministic Turing machines. We will use strong
nondeterministic Turing machines to define this class. A strong non-deterministic
Turing machine is one that has three possible out-
comes: "yes", "no" and "maybe". We say that such a machine accepts
a language L if the following is true: if x 2 L, then all computations
end up with "yes" or "maybe" and at least one with "yes",
if x 62 L, then all computations end up with "no" or "maybe" and
at least one with "no".
. is a standard enumeration of all nondeterministic
polynomial time clocked Turing machines then
strong nondeterministicg.
The following theorem links the question of the existence of a complete
language for NP " co-NP with the existence of a recursively
enumerable list of machines covering languages from NP " co-NP.
In [7] this list of machines is called a "nice" presentation of
Theorem 1. (Kowalczyk)
There exists a complete language for NP " co-NP if and only if
there exists a recursively enumerable list of strong nondeterministic
polynomial time clocked Turing machines N i 1
::: such that
This theorem can be exploited to obtain the following independence
result. Let T be any formal theory whose language contains
the language of arithmetic, i. e. the language f0,1, -, =, +, \Delta g. We
will not specify T in detail but only assume that T is sound (that is,
in T we can prove only true theorems) and the set of all theorems
of T is recursively enumerable.
Theorem 2. (Kowalczyk)
If NP " co-NP has no complete languages, then for any theory T
there exists L 2 NP " co-NP such that for no nondeterministic
polynomial time clocked N i with L(N i can it be proven in T
that N i is strong nondeterministic.
The class UP is closely related to a one-way function, the notion
central to public-key cryptography (see [13]). This class can be
defined using categorical (unambiguous) Turing machines. We call
a nondeterministic Turing machine categorical or unambiguous if it
has the following property: for any input x there is at most one
accepting computation. We define UP=fL(N i g.
As we can see from the following theorems the problem of the existence
of a complete language for UP is similar to its NP " co-NP
counterpart.
Theorem 3. (Hartmanis, Hemachandra)
There exists a complete language for UP if and only if there exists
a recursively enumerable list of categorical nondeterministic polynomial
time clocked Turing machines N i 1
::: such that fL(N i k
Theorem 4. (Hartmanis, Hemachandra)
If UP has no complete languages, then for any theory T there exists
such that for no nondeterministic polynomial time clocked
can it be proven in T that N i is categorical.
In Sections 6 and 7 we will show that the similarity between the
problems of the existence of complete languages for NP " co-NP
and for UP is also shared by the problem of the existence of an
optimal propositional proof system.
5 Formulas expressing the soundness of Turing machines
In this section we construct boolean formulas which will be used to
verify for a given deterministic polynomial time clocked transducer
M and integer n that M on any input of length n produces propositional
tautologies. We use these formulas in the proofs of Theorems
5 and 6.
For any transducer N we will denote by fN the function computed
by N (f
Definition 6. A Turing transducer N is called sound if fN maps
To any polynomial time clocked transducer M we will assign the
set AM =f Sound 1
M ,.g of propositional formulas
such
M is a propositional tautology if and only if for every
input of length n , the machine M outputs a propositional tautology.
So , for any polynomial time clocked transducer M , it holds: M
is sound if and only if AM ae TAUT .
Let N be a fixed nondeterministic Turing machine working in
polynomial time which accepts a string w if and only if w is not
a propositional tautology. For any fixed polynomial time clocked
transducer M , let us consider the set BM=fhM; 0 n i: There exists a
string x of length n such that M(x) 62 TAUT g. Using the machines
M and N we construct the nondeterministic Turing machine M 0
which guesses a string x of length n, runs M on input x and then
runs N on output produced by M .
works in polynomial time and accepts BM . Let FM;n
be Cook's Theorem formula (see [3]) for the machine M 0 and the
input hM; 0 n i. We define Sound n
M as :FM;n and then the formula
M is a tautology if and only if for every input of length n,
M outputs a tautology. From the structure of Cook's reduction (as
FM;n clearly displays M and n) it follows that for any fixed M , the
set AM is in P.
Moreover, the formulas describing the soundness of Turing machines
possess the following properties:
(1) Global uniformity property
There exists a polynomial time computable function f such that
for any polynomial time clocked transducer M with time bound
(2) Local uniformity property
Let M be any fixed polynomial time clocked transducer. There
exists a polynomial time computable function fM such that for
any w 2 \Sigma ?
6 Main results
A class of sets is recursively presentable if there exists an effective
enumeration of devices for recognizing all and only members
of this class ([10]). In this paper we use the notions of recursive P-
presentation and recursive NP-presentation which are mutations of
the notion of recursive presentability.
Definition 7. By an easy subset of TAUT we mean a set A such
that A ae TAUT and A 2 P ( A is polynomial time recognizable).
Definition 8. An optimal nondeterministic algorithm for TAUT is
a nondeterministic Turing machine M which accepts TAUT and
such that for every nondeterministic Turing machine M 0 which accepts
TAUT there exists a polynomial p such that for every tautology
ff
Let A be any easy subset of TAUT . We say that nondeterministic
polynomial time clocked Turing machine M names the set A if
A. Obviously A may possess many names. The following
theorem states that an optimal propositional proof system exists if
and only if there exists a recursively enumerable list of names for all
easy subsets of TAUT . We would like to pay attention to the similarity
between the next theorem and Theorems 1 and 3 from Section
4.
Theorem 5. Statements (i) - (iii) are equivalent.
(i) There exists an optimal propositional proof system.
(ii) There exists an optimal nondeterministic algorithm for TAUT .
(iii) The class of all easy subsets of TAUT possesses a recursive NP-
presentation.
By the statement (iii) we mean: there exists a recursively enumerable
list of nondeterministic polynomial time clocked Turing machines
::: such that
(2) For every A ae TAUT such that A 2 P there exists j such that
Proof. (i)
With every propositional proof system we can associate a non-deterministic
"guess and verify" algorithm for TAUT . On an input
ff this algorithm guesses a string w and then checks in polynomial
time whether w is a proof of ff. If successful, the algorithm halts in
an accepting state.
Symmetrically any nondeterministic algorithm for TAUT can be
transformed to a propositional proof system. The proof of a formula
ff in this system is a computation of M accepting ff.
Let Opt denote an optimal propositional proof system and let M
denote a nondeterministic Turing machine associated with Opt (a
"guess and verify" algorithm associated with Opt). It can be easily
checked that M accepts TAUT and for any nondeterministic Turing
machine M 0 accepting TAUT there exists a polynomial p such that
for every tautology ff it holds:
Let M be an optimal nondeterministic algorithm for TAUT. A
recursive NP-presentation of all easy subsets of TAUT we will define
in two steps. In the first step we define a recursively enumerable list
of nondeterministic Turing machines F 1 , F 2 , F 3 ,. The machine F k is
obtained by attaching the shut-off clock n k +k to the machine M . On
any input w, the machine F k accepts w if and only if M accepts w in
no more than jwj. The sequence F 1 , F 2 , F 3 ,
F 4 , . of nondeterministic Turing machines possesses the properties
(1) and (2):
(1) For every i it holds
(2) For every A which is an easy subset of TAUT there exists j such
that A ae L(F j )
In the second step we define the new recursively enumerable list
of nondeterministic polynomial time clocked Turing machines K 1 ,
as the machine which simulates
steps of F i and steps of N j (see Section 2 for definition
of N j ) and accepts w if and only if both F i and N j accept w.
Let A be any fixed easy subset of TAUT . There exist k and m
such that A = L(N k ) and A ae L(Fm ). It follows from the definition
of the sequence K 1 , K 2 , K 3 , . that A is accepted by the machine
provides a recursive NP-presentation of
all easy subsets of TAUT .
Let G be the machine generating the codes of the machines from
the sequence N i 1
,. forming a recursive NP-presentation
of all easy subsets of TAUT . We say that a string v 2 \Sigma ? is in good
form if
G; Comp \Gamma Sound jwj
where:
M is a polynomial time clocked Turing transducer with
time bound,
G is a computation of the machine G. This computation
produces a code of a certain machine N i j
M is a computation of the machine N i j
accepting
the formula Sound jwj
is the sequence of zeros (padding).
We call a Turing transducer n-sound if and only if on any input
of length n it produces a propositional tautology.
Let us notice, that if v is in good form then Sound jwj
M as a formula
accepted by a certain machine from NP-presentation is a propositional
tautology. This clearly forces M to be n-sound, where
so M on input w produces a propositional tautology.
Let ff 0 be a certain fixed propositional tautology. We define
in the following way: is in good
G; Comp \Gamma Sound jwj
and ff is a propositional tautology produced by M on input w, otherwise
\Gamma! TAUT .
In order to prove that Opt is polynomial time computable it is
sufficient to notice that using global uniformity property we can
check in polynomial time whether v is in good form. Hence Opt is a
propositional proof system.
It remains to prove that Opt simulates any propositional proof
system. Let h be a propositional proof system computed by the
polynomial time clocked transducer K with time bound n l
the set AK= fSound 1
K , .g is an easy subset of
TAUT , there exists the machine N i j
from the NP-presentation such
that
Let ff be any propositional tautology and let x be its proof in h.
Then ff possesses a proof in Opt of the form:
G; Comp \Gamma Sound jxj
The word Comp \Gamma G is the computation of G producing the code of
K is a computation of N i j
accepting Sound jxj
K .
Let us notice that jComp \Gamma is a constant. Because
is polynomial time clocked there exists a polynomial p such that
p(jxj). The constants c 1 , l and the polynomial
depend only on N i j
which is fixed and connected with K. This
proves that Opt simulates h.
The following definition is a nondeterministic counterpart of Definition
7.
Definition 9. By an NP-easy subset of TAUT we mean a set A
such that A ae TAUT and A 2 NP.
A slight change in the previous proof shows that also the second
version of Theorem 5 is valid. In this version condition (iii) is replaced
by the following one:
(iv) The class of all NP-easy subsets of TAUT possesses a recursive
NP-presentation.
Now we will translate the previous result to the deterministic
case.
Definition 10. An almost optimal deterministic algorithm for TAUT
is a deterministic Turing machine M which accepts TAUT and such
that for every deterministic Turing machine M 0 which accepts TAUT
there exists a polynomial p such, that for every tautology ff
We name such an algorithm as an almost optimal deterministic
algorithm for TAUT because the optimality property is stated for
any input string x which belongs to TAUT and nothing is claimed for
other x's (compare the definition of an optimal acceptor for TAUT
in [11]).
The equivalence (i) $ (ii) in the next theorem is restated from
[9] in order to emphasize the symmetry between Theorem 5 and
Theorem 6.
Theorem 6. Statements (i) - (iii) are equivalent.
(i) There exists a p-optimal propositional proof system.
(ii) There exists an almost optimal deterministic algorithm for TAUT .
(iii) The class of all easy subsets of TAUT possesses a recursive P-
presentation.
By the statement (iii) we mean: there exists a recursively enumerable
list of deterministic polynomial time clocked Turing machines
::: such that
(2) For every A ae TAUT such that A 2 P there exists j such that
Proof. (i)
This follows by the same arguments as in the proof of (ii) ! (iii)
from Theorem 5. The only change is the use of deterministic Turing
machines instead of the nondeterministic ones.
A string v 2 \Sigma ? is in good form if
G; Comp \Gamma Sound jwj
where the appropriate symbols mean the same as before. We define
analogously as in the proof of Theorem 5:
is in good form
G; Comp \Gamma Sound jwj
and ff is a propositional tautology produced by M on input w, otherwise
is a certain fixed propositional tautology.
It remains to prove that Opt p-simulates any propositional proof
system. Let h be a propositional proof system computed by a polynomial
time clocked transducer K with time bound n l
the set AK= fSound 1
K , .g is an easy subset of
TAUT , there exists the machine D i j
from the P-presentation such
that
). The function
G; Comp \Gamma Sound jxj
translates proofs in h into proofs in Opt. The word Comp \Gamma G in the
definition of t is the computation of G producing the code of D i j
K is a computation of D i j
accepting Sound jxj
K .
From the fact that D i j
is deterministic and works in polynomial
time and from local uniformity property (see Section
that Comp \Gamma Sound jxj
K can be constructed in polynomial time. This
proves that t is polynomial time computable.
Definition 11. A Turing machine acceptor M is called sound if
ae TAUT .
The question, whether the set of all sound deterministic (non-
deterministic) polynomial time clocked Turing machines yields the
desired P-presentation (NP-presentation) (that is, whether this set
is recursively enumerable) occurs naturally in connection with Theorems
5 and 6. The negative answer to this question is provided by
the next theorem.
Theorem 7. The set of all sound deterministic (nondeterministic)
polynomial time clocked Turing acceptors is not recursively enumerable

This follows immediately from Rice's Theorem (see [14]).
7 Independence results
Let T be any formal theory satisfying the assumptions from Section
4. The notation T ' fi means that a first order formula fi is provable
in T .
Let M be a Turing machine. By "L(M) ae TAUT " we denote
the first order formula which expresses the soundness of M , i.e.
8w2L(M) [w is a propositional tautology]
Definition 12. A deterministic (nondeterministic) Turing machine
Definition 13. A set A ae TAUT is T -provably NP-easy if there
exists a nondeterministic polynomial time clocked Turing machine
fulfilling (1) - (2)
(1) M is
As in the case of the classes NP " co-NP and for UP we can
obtain the following independence result.
Theorem 8. If there does not exist an optimal propositional proof
system, then for every theory T there exists an easy subset of TAUT
which is not T -provably NP-easy.
Proof. Suppose, on the contrary, that there exists a theory T such
that all easy subsets of TAUT are T -provably NP-easy. Then the
following recursively enumerable set of
machines\Omega is a
nondeterministic polynomial time clocked Turing machine which is
creates a recursive NP-presentation of the class of all
easy subsets of TAUT . By Theorem 5, this implies that there exists
an optimal propositional proof system, giving a contradiction.
The following result can be obtained from the second version of
Theorem 5.
Theorem 9. If there does not exist an optimal propositional proof
system, then for every theory T there exists an NP-easy subset of
TAUT which is not T -provably NP-easy.
The translation of this result to the deterministic case goes along
the following lines.
Definition 14. A set A ae TAUT is T -provably easy if there exists
a deterministic polynomial time clocked Turing machine M fulfilling
(1) M is
Theorem 10. If there does not exist a p-optimal propositional proof
system, then for every theory T there exists an easy subset of TAUT
which is not T -provably easy.
8 Conclusion
In this paper we related the question of the existence of an optimal
propositional proof system to the recursive presentability of the
family of all easy subsets of TAUT by means of polynomial time
clocked Turing machines . The problems of the existence of complete
languages for the classes NP " co-NP and for UP have a
similar characterization. From this characterization a variety of interesting
results about the promise classes NP " co-NP and UP
were derived by recursion-theoretic techniques (see [7], [5]). Although
recursion-theoretic methods seem unable to solve the problem of the
existence of an optimal propositional proof system we believe that
our main results from Section 6 allow the application of these methods
(as it was in case of promise classes, see [5], [6]) to further study
of this problem.



--R

Structural Complexity I (Springer-Verlag
Lectures on Proof Theory.
The complexity of theorem proving procedures
The relative efficiency of propositional proof systems
Complexity classes without machines: On complete languages for UP
On complete problems for NP
Some connections between presentability of complexity classes and the power of formal systems of reasoning
Complete Problems for Promise Classes by Optimal Proof Systems for Test Sets
Propositional proof systems
On the structure of sets in NP and other complexity classes
On optimal algoritms and optimal proof systems
Optimal proof systems for Propositional Logic and complete sets
Computational Complexity
Classes of recursively enumerable sets and their decision problems
On an optimal quantified propositional proof system and a complete language for NP
--TR
Complexity classes without machines: on complete languages for UP
Some Connections between Representability of Complexity Classes and the Power of Formal Systems of Reasoning
On Complete Problems for NP$\cap$CoNP
Optimal Proof Systems for Propositional Logic and Complete Sets
On an Optimal Quantified Propositional Proof System and a Complete Language for NP cap co-NP
Complete Problems for Promise Classes by Optimal Proof Systems for Test Sets
The complexity of theorem-proving procedures

--CTR
Christian Glaer , Alan L. Selman , Samik Sengupta, Reductions between disjoint NP-pairs, Information and Computation, v.200 n.2, p.247-267, 1 August 2005
complexity of computation;complexity classes;complexity of proofs;classical propositional logic