Cybernetics and Systems Analysis, VoL 34, No. 5, 1998

C O N C E R N I N G E X I S T E N T I A L D E F I N I T I O N O F T H E C L A S S NP:. T H E O R E T I C A L A N A L Y S I S O F AN A L T E R N A T I V E A P P R O A C H UDC 519.682.1;681.3

O. V. Gernlan

INTRODUCTION We consider an alternative def'mition of the class NP, which is associated with provability of decision algorithms for languages (problems) from NP. We state and prove some theoretical properties of this class. The proposed definition is motivated by the following considerations. 1. With the traditional definition, there is always a problem (language) Z from N P whose polynomial reduction to the problem (language) SATISFIABILITY theoretically exists and yet cannot be provably constructed. 2. Therefore, if we could construct and prove a polynomial determini~c algorithm for the problem SATISFIABILITY, a polynomial deterministic algorithm for the problem Z would remain only in theory. 3. Moreover, it is established that the NP-completeness property in the traditionally defined class N P is algorithmically undecidable. Thus, if we manage to prove that the problem SATISFIABILITY is undecidable on a polynomial deterministic Turing machine (DTM), then this does not say anything about some NP-complete problem Z ~. N P in the sense of provable definition of its computational complexity. 4. It remains possible to construct a "pure" proof of P = N P which does not lead to a polynomial algorithm for SATISFIABILITY, because there is a sharp dividing line between algorithms realizable by Turing machines in general and algorithms realizable by provably constructable Turing machines (PCTM) in particular. For PCTM we can prove that an algorithm realized by the machine maps input words satisfying some property into one set and words not satisfying that property into another set. An algorithm is regarded as a set of Turing machine instructions (rules) processing input words into output words. Remarks 1-4 are essential: the problem SATISFIABILITY may have a polynomial deterministic algorithm in the form of DTM rules but not a polynomial deterministic algorithm in the form of PCTM rules. This has a direct implication for the solution of problems in practice.

DEFINITIONS The following concepts are assumed known: 1. The concept of Turing machine (TM); deterministic Turing machine (DTM), nondeterministic Turing machine (NDTM); the concept of computation realized on a given input [1-4]. 2. The mathematical concept of algorithm and its TM formalization [1, 5, 6]. 3. The concepts of set, formal system, derivation rules, inconsistency [7-9]. 4. The concepts of language, grammar, context-free grammar (CF-grammar), string, operations on languages [8, 10]. 5. The concept of computational complexity of an algorithm (Turing machine); the definition of the language (problem) SATISFIABILITY [11, 12]. Given two languages L 1 and/-2, the concatenation of L 1 and L2 is the language L 3 = LI.L 2 = {x'yi x ~ L 1, y E

r2}. It has been noted [10, p. 237] that ~ - L l = L1-Z = ~ ( ~ is the empty language). Translated from Kibernetika i Sistemnyi Analiz, No. 5, pp. 15-25, September-October, 1998. Original article submitted August 30, 1996.

1060-0396/98/3405-0645520.00 9

Kluwer Academic/Plenum Publishers

645

Def'mition. The algebraic concatenation ( O ) of the languages L l and/-'2 is the language/-'3 def'med by the following conditions: (1) If L 1 and L 2 are both nonempty, then/-3 = LI O L 2 = {xy] x E L l, y E L2}. (2) If L 1 is empty and L2 is nonempty, then L3 = L l O L 2 = L 2. (3) If L 1 is nonempty and L 2 is empty, then L3 = L 1 O L 2 = L I. (4) If L 1 and I-'2 are both empty languages, then L 3 = L 1 0 I-'2 = ~ Definition. The language generated by some grammar is recursive if there exists an algorithm such that for every word x we can apply this algorithm to decide if the word x is derivable in the given grammar or not. If the language L is recursive, then its complement from = {x ix ~ L} is also recursive. The following facts are known. F1. Every CF-language is recursive. Moreover, Younger's algorithm [13] can decide in polynomial (cubic) time if an arbitrary string x is contained in the given CF-language or not. F2. There is no algorithm that establishes or refutes for an arbitrary CF-language L the fact L = E;* (/~* is the complete language over the alphabet of L). The completeness problem for a CF-language is algorithmicaUy undecidable in the general ease. Yotmger's algorithm requires, however, that the CF-grammar 1~ does contain the rules A --* e (e is the empty string). We therefore consider only CF-grammars that satisfy the following requirements: REQI" I~ does not contain rules of the form A --, e. REQ2: I ~ contains only one rule of the form SO --- e, where SO is the principal nonterminal symbol of the grammar that does not occur in the fight-hand side of any other grammatical rule. The following point is essential: every CF-grammar F' is effectively transformable (i.e., transformable by an algorithm) to a grammar F satisfying REQ1 and REQ2, and this [' is context-free. The algorithm needed for this transformation is proved and described in [13, pp. 172-173]. Therefore in what follows we only consider CF-grammars satisfying REQ1

and REQ2. The language L M accepted by the Turing machine MT* is defined as follows [12]-

L M = {x E ~*]MT* accepts x}. The traditional definition of NP (in what follows we use the notation NP(1) with subscript (1)) relies on the concept of acceptance of a language by Turing machines. DeFinition [12, p. 48].

NP(I ) = {L: there exists a polynomial-time NDTM M such that L = LM}.

(1)

For the class P(1) of languages accepted by polynomial DTM, the corresponding definition is the following [12, p. 42]" PO) = {L: there exists a polynomial DTM M such that L = LM}. These definitions require the existence of Turing machines. However, as we shall see, it is possible to construct.a language (or languages) for which an accepting polynomial NDTM exists, but it is impossible to provably construct this NDTM. In reality, we always turn to the proof of decidability of the property ~o defining the algorithm. It is immaterial if this proof is called verification, "certification', or certificate verification, as in the following definition [14]: "We say that the acceptance problem A is in the class NPo) if there exists a polynomial p(n) and an algorithm .~ (a certificate verification algorithm) such that the following property holds: the string x is an individual problem A with the answer YES if and only if there exists a string c(x) (a certificate) of symbols from E; such that Ic(x) l <- p(Ixl) and the algorithm ~, receiving the input string x 9 c(x) reaches the answer YES after at most p(Ixl) steps." We accordingly introduce the concept of a provably constructable Turing machine that accepts the language L. Let x E E;* (E is the alphabet of the language L). The Turing machine M i is a set of instructions that process each input word x into some output word y. Let Qr (QN) be the final accepting (rejecting) state. Consider the predicate U(x, Q, L) defined for the final state Q on the input x:

U(x, Q, L) is true if x E L and Q = Qr or x ~ L and Q = QN; otherwise U(x, Q, L) is false.

646

For every input x r, M i produces the result Yr, so that U(x r, Q, L) is either false or true (or undef'med if the algorithm cycles). Each time that U(xr, Q, L) is true, i.e., satisfies the definition of U(...), the machine M i indeed accepts L. However, if we present only the instruction system of M i, it is impossible to judge, without resorting in general to a formal proof, if M i accepts L or not. We need a formal proof that M/"generates" true predicates U(x r, Q, L) for an arbitrary input x r. If such a proof exists or is explicitly presented, we say that M/is a provably eonstructable machine (PCTM) for L. The only rigorous meaning that we impart to the word "constructable" in the definition of PCTM involves the existence of an effective procedure to generate language-accepting machines, for instance, by enumerating and decoding their Goedel numbers. We thus obtain the following alternative definition:

NP(2 ) = {L: there exists a polynomial provably constructable NDTM M for which L = LM}; P(2) = {L: there exists a polynomial deterministic PCTM that accepts L}.

(2)

In our definition of proofs we impose the following requirements [16] (for the time being, leaving aside the question of their satisfiability). (i) Proofs are finite objects. Therefore, the Goedel number can be establishexl for every proof, and conversely, given a Goedel number we can uniquely determine the code of each proof. (it') The proof of an arbitrary formula e should have a sequence structure Y

where Rz(...) are derivation rules; in each derivation rule the premise formulas are given in parentheses on the left-hand side of the vertical bar and conclusion formulas are given on the right-hand side of the vertical bar; the premise formulas are either axioms from ~kx, or conclusions of previously used rules. Given the code of a proof, we can always effectively establish (i.e., establish using an algorithm) which assertion is proved (e) and is it correctly proved or not. (iiO The explicit definition D of the concept of proof should therefore be such that if the set of axioms ,~x is recursive, then the relation "p is a proof of assertion o from the axioms Ax-" is decidable. This implies the possibility of deciding for any formula o and any proof p whether p is a proof of o in the given formal system or not. ..

MAIN T H E O R E M S FOR NP(I ) Assume that the language L 1 is generated by the CF-grammar r . Assume that the language L 2 does not contain two different words and contains the nonempty word w. Consider the language

Z=

tg ~ | ta.

(3)

Prolmsition 1. Each particular language s (3) is NP(I ). Proof. Suppose that Ll c~ is empty. Then L, = I-,2 = w. This language is accepted by a trivial polynomial NDTM. Clearly, such NDTM exists regardless of F2. F2 implies the following: there is no Turing machine that given an input word encoding the rules of the CF-grammar 1" decides in finitely many steps the completeness of the language L generated by I'. The situation is different concerning the acceptance of the particular language s = L2 = w. For this language, the corresponding Turing machine accepts a single word w. If LI c~ is nonempty, then acceptance of a nonempty CF-language is based on Younger's polynomial algorithm. The existence of the required Turing machine is thus established in this case also. We thus reach the conclusion that every particular language s is accepted by some appropriate polynomial NDTM. By F2, an appropriate PCTM cannot in general be constructed for s Hence, we conclude that the required polynomial NDTM exists, but cannot always be provably constructed. In particular, we obtain that NP(I ) # NP(2 ). T H E O R E M 1. The class NP(I ) is nonrecursive. Proof. It suffices to show that there is no algorithm ~' that for an arbitrary problem (an arbitrary language) decides if it is polynomially solvable or not. Assume that an algorithm ~' exists. Consider the following problem. Let I" be a CFgrammar, L l the language generated by F, Lexp a language for which we a priori know that it is acceptable only by an

647

exponential algorithm (an example of such an exponential language is given below). Consider the acceptance problem for the following language-

L"

= I[tLIc~ : ~

(~) Lexp' if , z; ~ is empty, , if LIc~ is noncmpty.

Clearly, ./t' answers NO concerning the algorithm for the acceptance problem of L* (L* = Lexp in this case) if LI oam is empty and YES if L1oam is nonempty. This provides a solution of the completeness problem for an arbitrary CF-language, which is impossible. We will now suggest an appropriate language Lexp. We assume for simplicity that Lexp is defined on the set S ~ of binary word {0, 1}* that has the property ~-i. Rabin's well-known theorem holds for this case. T H E O R E M (Rabin). For every computable function tiP) , P E B*, there exists a property 4~ of binary words such that the following conditions are satisfied: (a) this property is effectively decidable, i.e., there exists a Turing machine that decides for every word P if it has the property P or not; (b) for every Turing machine R accepting the language B*, its time complexity is greater than tiP) for all binary words, except f'mitely many. We def'mef(P) as.t(/') = 2 IPI, where IPi is the length of the word P. An appropriate constructive definition of 5 can be borrowed from Trakhtenbrot [3]" "the word P has the property ~,,, if it encodes some Turing machine which when applied to P rejects P in fewer than.t(P) = 2 lel steps." We thus have all the elements of the proof of Theorem 1. We will now state and prove the following result: for some NP(l)-complete problem 3 there exists a reduction to the problem SATISFIABILITY (SAT for short) by a polynomial NDTM, but this reduction is not provably realizable (no appropriate polynomial PCTM exists). Thus, if we have found a polynomial deterministic PCTM for SAT, we cannot use this PC'TM directly for 3 because 3 is purely theoretically reducible to SAT. Assume, as before, that r is a given arbitrary CF-grammar, L the language generated by F with the alphabet of terminal symbols ~ = {0, 1}. Given is the problem SAT coded in the set of Boolean variables x 1. . . . . x n. We use the notation SAT(xl . . . . . Xn). We consider each interpretation satisfying SAT(x I . . . . . x n) as a tuple I ordered by ascending variable indices. We identify I with the binary word/a, in which the i-th position from the left is 1 if x i E I and 0 if x i ~ L Now form a new problem L-SAT. Given are SAT(x I . . . . . xn) and r . Is there an ordered tuple I that satisfies SAT(x 1. . . . . xn) and such that the corresponding binary word/B is in the language s = L ~ 0 / " 2 ,

L 2 = {IiB[Ii satisfies SAT(x I . . . . . xn) }.

(4) i

This question is clearly equivalent to the answer YES i f , E L~ or L ~ = f~ (e is the empty word) and I satisfies SAT(x I . . . . . xn). We directly prove that an arbitrary SAT(x I . . . . . xn) is polynomially reducible to some problem L-SAT. Indeed, it is sufficient to take as the CF-grammar r S-*e

S.-. IS S -. OS. This grammar generates a complete CF-language L over E = {e, 0, 1}. Now, it follows from the above that/~, = NP for L~ = ~ . Indeed, assume that SAT(x 1. . . . . xn) generates the satisfying tuples I 1. . . . . I z and let L 2 = {ll B, . . . ,. lz B} Then the language L c~ (D L 2 is identical with the language of some Turing machine accepting the words {Ii B. . . . . lzB}. Let L~ # ~ . Then s is accepted by some Turing machine that applies Younger's algorithm by the following scheme- "If the length of/8 is longer or shorter than n, then reject/B. Otherwise, if/8 does not satisfy SAT(x 1. . . . . xn), then reject/B. Else check derivability of e in L. If e is not derivable in L, then accept/B; else reject/B.. A Turing machine realizing this scheme indeed accepts/_7, if L c~ # ~ . It should be clear that the set of solutions of L regarded as binary words is identical with the language (4). 648

T H E O R E M 2. The language/_7, (4) is polynomially irreducible to SAT by PCTM. Proof. Assume the contrary: for any arbitrary CF-language and SAT, L-SAT is reducible to SAT*. Assume that SAT is satisfiable. Then by satisfiability of SAT*, either Lc~ is empty or e E from. The second case is verified by Younger's algorithm, and if e ~ Lc~ then we conclude that Lc~ is empty. This means that we have a procedure to decide completeness/incompleteness of an arbitrary CF-language in the following way. Take an a priori satisfiable SAT. Suppose that L-SAT is reducible to SAT*. Then by unsatisfiability of SAT* we have L # IX*. If SAT* is satisfiable, then do as described previously for the case Le~ # ~ . We thus solve the completeness problem of an arbitrary CF-language, which is impossible. Reduction by PCTM is thus ruled out. It follows from our proof that E, is irreducible to SAT by any PCTM, and not only by a polynomial PCTM.

TItEORETICAL PROPERTIES OF NP(2) T t t E O R E M 3. The class NP(2 ) is nonrecursive. Proof. We have to show that the relevant property of the language L (i.e., there exists a provably constructable polynomial accepting NDTM for L) is in general undecidable. In other words, there is no algorithm.Jr o that for an arbitrary language L decides if this language is NP(2) or not (in other words, the characteristic function of the class NP(2 ) is uncomputable). To prove this assertion, we introduce the language s such that

where LI c~ = X;*LLl and L l is the language generated by the CF-grammar r . Here L94e~ is the complement of the language L l to the complete language IX* over the alphabet IX. The language L2 does not contain two different words and contains the nonempty word w (i.e., L2 contains the single word w). We have the following assertion for every language L 1 either L 1 = X;* and then/.7, = ~ (3) L 2 = L 2, or L 1 ;~ ~* and then [, = L94c~ Q L2 # L 2 with LI e~ # {e}. In the last case, when L 1 # IX*, the acceptance of the language s can be based on Younger's algorithm, which is cubic in the length of the input word. In some cases, nonemptiness of L1c~ is easily decided given the form of the CF-grammar r . For instance, let 9

S ... B

B - * abc B .-. C b

C..,aar C -*, cBa.

For this CF-grammar we can easily prove that every word shorter than three symbols in the alphabet E = {a, b, c} is not contained in" the language generated by r and thus L1c~ ~ ~ . This conclusion follows directly from the form of the grammar. It remains to show that in some particular case the nonemptiness property of L1c~ is unprovable (undecidable) for this CF-grammar generating L 1. It is thus impossible to decide if s satisfies the def'mition of NP(2 ) or not. This is a critical case. Let us establish the following properties of the language/7,. Proposition 2. If the empty string e ~ LI c~ and w E s = L1c~ (D L 2, then LI c~ is empty. Proof. By contradiction, assume that L1c~ is nonempty. Then no word in s is identical with w and thus w ~ s A contradiction with the assumptions of Proposition 2. Thus, L1c~ is empty. Proposition 3. If LI c~ is empty, then w E s = LI c~ C) L2 and e ~ L1c~ Proof. This proposition is a direct consequence of the definition of NP(2). Proposition 4. There is no general algorithm that for an arbitrary language s decides if it contains the word w or not.

649

Proof is by contradiction. Assume that every language/_7, is accepted by some algorithm. Consider how the corresponding Turing machine accepts the word w. This machine decides in polynomial time that 1) w E L2; 2) 9 E L 1 or e ~ L l (by Younger's algorithm). Assume that e E L 1. But then judging by how the machine accepts the word w we can decide if the language LI c~ is empty (or nonempty), because by Propositions 2 and 3 emptiness of LI c~ is equivalent to acceptance of w with 9 ~ LI e~ This contradicts F2. Now assume that we have a procedure to decide if there exists for/, an accepting polynomial PCTM that uses some algorithm ~ 0 . Also assume that the proofs are recognized by some algorithm/t I . Two mutually exclusive variants are possible: Jt o. establishes for/: that/: ~ NP(2 ) or that s E NP(2 ). Variant 1. ~ ~ establishes for [, that [, ~ NP(2). Then LI e~ cannot be nonempty (i.e., it is necessarily empty). Imleed, let u E Ll c~ Then there is at least one PCTM that accepts L. This PCTM operates by Younger's algorithm and proves that u ~ L l (u E Lie~ But then the language/~ should be NP(2), a contradiction. Thus, Ll e~ is empty. This variant assumes that once a required word u exists, it may be presented as a proof in finite time by the Turing machine that generates the words of If* in a systematic manner and verifies their inclusion in L l by Yotmger's algorithm (for instance, first words of length 0 are generated, then words of length 1, and so on). Variant 2..,~ 0 establishes for [, that/.-, E NP(2). This means that there exists a PCTM that accepts the given language s Let e ~ LI e~ Then acceptance of w implies emptiness of L1c~ Conversely, rejection of w with 9 ~ LI c~ implies nonemptiness of L1c~ In this variant, an appropriate PCTM exists for/:. The required PCTM is constructed by c.rdered enumeration with verification of Turing machines and corresponding proofs. By our assumption about ~t l, this verification is algorithmically realizable. We can now propose an algorithmic procedure to decide the completeness problem for an arbitrary CF-language L 1. 0 decides/: = L lc~ (9/-'2 E NP(2 ) or not. In the latter case, as it follows from variant 1, L1 c~ is empty, i.e., L 1 = I;*. Let L lc~ (D/-'2 E NP(2 ). There is an algorithm ~ 2 that enumerates the arithmetic predicates P(x, y, z), where x is the Goedel number of the specification of the Turing machine MT, y is the Goedel number of the specification of the language L (formula), and z is the G o , e l number of the proof that MT accepts L. By known assumptions [16], the predicate P(x, y, z) is recursive. Therefore, sooner or later we obtain a triple of target numbers in P(x, y, z), and the number x enables us to reconstruct the Turing machine that accepts s We can thus check how this machine accepts the word w. If e E L lcorn, then L l ~ If* . This check is carried out by Younger's algorithm. If 9 ~ /.,1e~ and the Turing machine with number x accepts the word w, then LI c~ = ~ and L 1 =/~*. This contradicts F2. "Now assume that there is no algorithm.Jt, 1 that verifies proofs. In our setting, proofs are derivations in formally consistent theories; each derivation satisfies a rigorously defined recursively verifiable syntax. Thus, the set of proofs is a nonrecursive subset of the set of derivations, i.e., not every derivation is a proof. Therefore, the predicate P(x, "y), where x is a formula and y a proof, is undecidable. We obtain the following: not every syntactically valid derivation of the formula 'Px is recognized as a proof in finite time (in what follows we present an interesting result of this type). Consider the language L* = Z ( 9 / - ' 2 , where L 2 E NP(2 ), Z = P(.~, )9) is true for the formula number .~ and derivation number y (this derivation is a proof of formula $). Then there is a language L* for which no algorithm exists to decide if L* E NP(2 ) (?). We have thus proved that NP(2) is nonrecursive. l e t us present some additional interesting results. T I t E O R E M 4. Assume that there exists an algorithm .,~, which for every problem solvable by a polynomial deterministic Turing machine decides its polynomial solvability. Then/(2) ;~ NP(2)Proof. Assume by contradiction that/(2) = NP(2)- Then we can apply i./t, to decide for an arbitrary problem X that X E NP(2 ) or X ~ NP(2 ), which implies that NP(2) is a recursive set. A contradiction. (Theorem 4 obviously deals with PCTM.) T H E O R E M 5. For some NP(2)-complete language X we cannot prove that X is NP(2)-complete when P(2) ;~ N P w . Proof. Take the language SATISFIABILITY as NP(2)-complete and assume that E is the standard enumeration of Turing machines. We denote by M(x) the Turing machine with input x. Consider the following family of sets: for every i E E and x E E , Xi, x = {YlMi(x) does not stop in [y[ steps and y E SATISFIABILITY}. Clearly, every language Xi. x E NP W, because 650

(a) for given i, x and an arbitrary y we can verify by a provable polynomial NDTM that y E SATISFIABILITY, and (b) M,4,x) does not stop in lyl steps. Assume that Mr(x) stops on the input [y[ in t steps. Then Xi, x = {yl [y[ < t and y E SATISHABILITY}. Clearly, Xi,x is a finite set (for a given alphabet/~), Thus, Xi,x E P(2) in this case. If M~(x) does not stop at all on the input x, then by assumption Xi, x is identical with the language SATISFIABILITY, and thus Xz;x is an NP(2)-complete set in this case. However, in general we can neither prove nor decide algorithmically if M/cycles on the input x or not, because the stopping problem for the Turing machine in general is umiecidable. Thus, if we could prove NP(2)-completeness for an arbitrary NP(E)-complete language, then we could do this also for any language X/,x identical with the language SATISFIABILITY, while the machine Mt4,x) cycles for each such language Xi, x. This observation contradicts the previously noted algorithmic undecidability of the stopping problem. It remains to note that if the Turing machine indeed stops on the input x, then this fact is provable by demonstrating the computation realized on this input. As a consequence, we have the following result. Proposition 5. If P(2) # NP(2), then there is an NP(E)-complete language X such that it is impossible to provably construct a reduction of the language SATISFIABILITY to this language and no polynomial deterministic accepting PCTM exists forX.

PROBLEM OF DISTINGUISHING DERIVATIONS AND PROOFS

The purpose of this section is to formulate the problem of distinguishing derivations and proofs in formally consistent theories. This problem has a direct bearing on both the definition of NP(2) and the definition of NPo) that require an algorithm to verify the solution of problems. In reality (see, for instance, [9, 16]), proofs are assumed algorithmicaUy verifiable. We should note that this is certainly so if proofs in formally consistent theories are identified with syntactically correct derivations. The point is that not every syntactically correct derivation is undisputably a proof, although every proof is a derivation. This delicate and important issue is traceable to the lack of identity between syntax (form) and semantics (content) of abstract mathematical objects, in particular proofs. In this section we construct the language LAR and use it to demonstrate the essence of the problem of distinguishing derivations and proofs in formally consistent theories. By definition, LAR = {y[y = Yl # Y2, where (i) Yl is a specification (set of rules) of the deterministic Turing machine MTe; (it) Y2 is a proof that MTe is f'mite on every input; (iii) MT e accepts the word 'Yl # YE}Let LAR c~ = {YlY ~ LAR}. Assume that every syntactically correct derivation of some formula ~ in a formally Consistent theory F is a proof of ,a (a proof of ,p is a derivation in F that ensures the truth of r in every model of the theory F). We thus identify derivations and proofs. Assume that the machine MTLARc~ accepting LAR c~ is not finite. Therefore, the machine MTLAR accepting LAR is not finite either, because we construct these machines using the same set of rules with the only exception that QY (QN) in MTLAR corresponds to QN (QY) in MTLARc~ Here Qy (QN) is the final accepting (rejecting) state. We thus conclude that MTLA R cannot recognize in a finite time the proof Y2 on some word Yl # Y2, which, however, contradicts the definition of derivation as a f'mite mathematical object with a rigorously defined recursively verifiable syntax; a derivation is a sequence of steps; each derivation step involves application of a derivation rule or an axiom schema; a derivation rule is applicable if its premises are axioms or have been previously obtained in other derivation steps. On the other hand, in a formally consistent theory each derivation/proof guarantees truth of the conclusion. We therefore formally conclude that MTLA R is f'mite and thus MTLARc~ is also f'mite on every input. If we now classify the given derivation as proof (this can be easily formalized by reducing to contradiction the assumption of nonffmiteness of MTLAR), then denoting the proof as y2LARC~ we easily show that either answer (YES/NO) to the question Yt L A R c~ # y2t.ARr E LARCOmleads to a contradiction (yt LARc~ is the specification of MTLARcom). This example shows that, in general, we can distinguish derivations and proofs in formally consistent theories by treating the latter as a proper subset of the former. The issue of defining a proof is not considered at this stage.

651

The introduction of the class NP(2) is justified not only because it is different from NP(I) but also by virtue of the important practical remarks at the beginning of the article. Rigorous and consistent axiomatization is of undisputable value for both practice and theory. In conclusion, I acknowledge the important contribution of graduate student V. G. Naidenko, who suggested considering the concatenation of languages Ll c~ 9 L2, where Ll c~ is the complement of a context-free language, and used this concatenation to prove the theorem on nonrecursiveness of the class P(1) when PO) # NP(o"

REFERENCES l~

2. 3. 4. 5. 6. 7. 8. 9. 10. 11. 12. 13. 14. 15. 16.

652

A. I. Mal'tsev, Algorithms and Recursive Functions [in Russian], Nauka, Moscow (1986). V. A. Uspenskii, Lectures on Computable Functions [in Russian], Fizmatgiz, Moscow (1960). B. A. Trakhtenbrot, Algorithms and Computing Automata [in Russian], Nauka, Moscow (1974). H. Rogers, Theory of Recursive Functions and Effective Computability [Russian translation], Mir, Moscow (1972). V. M. Glushkov, Theory of Algorithms [in Russian], KVIDU, PVO, Kiev (1961). V. M. Glushkov, An Introduction to Cybernetics [in Russian], AN UkrSSR, Kiev (1964). C.-C. Chang and H. 7. Keisler, Model Theory [Russian translation], Mir, Moscow (1977). A. Gross and A. 1.amen, Formal Grammar Theory [Russian translation], Mir, Moscow (1971). S. C. Kleene, Introduction to Metamathematics, Van Nostrand, New York (1952). V. M. Glushkov, G. E. Tseitlin, and E. L. Yushchenko, Algebras, Languages, Programming [in Russian], Naukova Dumka, Kiev (1989). R. M. Karp, "Reducibility of combinatorial problems," Kib. Sb., new series, No. 12 [Russian translations], Mir, Moscow (1975). M. R. Garey and D. S. Johnson, Computers and Intractability, Freeman, San Francisco (1979). D. H. Younger, "Acceptance and analysis of context-free languages in time n3," in: Topics in Mathematical Logic [Russian translations]. A. Aho and J. Ullman, The Theory of Parsing, Translation, and Compiling, Vol. 1, Prentice Hall, Englewood Cliffs, NJ (1972). C. H. Papadimitriou and K. Steiglitz, Combinatorial Optimization: Algorithms and Complexity, Prentice Hall, Englewood Cliffs, NJ (1982). N. Cutland, Computability: An Introduction to Recursive Function Theory, Cambridge Univ. Press (1980).