UDC 517.11

MATHEMATICS

V. I. KHOMICH

ON THE COMPLEXITY OF REALIZING PROPOSITIONAL FORMULAS

(Presented by Academician A. A. Dorodnitsyn, 8 VI 1970)

In paper \((^9)\) results were obtained showing that, along with propositional formulas that have no upper bound for the complexity of realizability, there are also formulas for which the function \(\lambda x\, C_1 \cdot 14^x + C_2\)*, for certain \(C_1\) and \(C_2\), is an upper bound for the complexity of realizability. The question arises: is it true that every propositional formula either has no upper bound for the complexity of realizability, or the function \(\lambda x\, C_1 \cdot 14^x + C_2\) is its upper bound for the complexity of realizability?

In the present paper results will be presented that concern only part of the question posed: a condition will be formulated sufficient for a propositional formula not to have an upper bound for the complexity of realizability; an affirmative answer will be given to the question posed in the case when the propositional formula is a formula in one variable.

We shall use the terminology and concepts introduced in papers \((^{1-6})\), and shall also assume that the reader is familiar with paper \((^9)\).

1. In \((^9)\) concepts concerning propositional formulas are introduced for formulas in one variable. We shall extend them to an arbitrary propositional formula.

Let \(k\) be a natural number, and let \(Q\) be a \(k\)-term system of closed logical-arithmetical formulas. By the symbol \(Q_i\) \((1 \leq i \leq k)\) we shall denote the \(i\)-th term of the system \(Q\). Let \(n\) be a natural number, and let \(G\) be a propositional formula in the variables \(p_1, \ldots, p_k\). We shall say that a normal algorithm \(\mathfrak A\) over the alphabet \(A\)* \(n\)-realizes the formula \(G\) if, for every \(k\)-term system of closed logical-arithmetical formulas \(Q\) such that \(|Q_i^o| \leq n\) \((1 \leq i \leq k)\),

a) the algorithm \(\mathfrak A\) is applicable to \(Q\);

b) \(\mathfrak A(Q)\) realizes the formula \(G(Q_1, \ldots, Q_k)\).

Let \(G\) be a propositional formula. We shall say that \(G\) has no upper bound for the complexity of realizability if, for any general recursive function \(f\), there exists a natural number \(N\) such that for every natural number \(m\) such that \(m \geq N\), and every normal algorithm \(\mathfrak A\) in the alphabet \(A^+\) that \(m\)-realizes \(G\), one has \(\mathfrak A' \geq f(m)\).

* Here and below we use \(\lambda\)-notation (see \((^2)\), p. 37) for functions.

** A propositional formula \(G\) is a formula in the variables \(p_1, \ldots, p_k\) if \(p_i\) \((1 \leq i \leq k)\) occurs in \(G\) and no propositional variable other than \(p_1, \ldots, p_k\) occurs in \(G\).

*** In the present paper, as in \((^9)\), \(A\) is the alphabet of logical-arithmetical formulas, and \(A^+\) is the standard two-letter extension of the alphabet \(A\).

We note that Theorem 5 of paper (⁹) remains true also when \(F\) and \(G\) are arbitrary propositional formulas, and not formulas in one variable, as is required in paper (⁹).

1. Let \(J_1\) be the first Jaśkowski matrix (see (⁶), p. 7).

Theorem 1. If a propositional formula \(G\) is refutable on \(J_1\), then \(G\) has no upper bound for realizability complexity.

For the proof of this theorem one uses Theorem 4 of paper (⁹), as well as the strengthening, mentioned above, of Theorem 5 of paper (⁹), and a fragment of the proof of Theorem 1 of paper (⁸) (if \(G\) is refutable on \(J_1\), then \(G \vdash \neg\neg p \supset p\) in the intuitionistic propositional calculus with the substitution rule).

1. Let \(G\) be a propositional formula, and let \(f\) be a general recursive function. We shall say that \(f\) is an upper bound for the realizability complexity of the formula \(G\), if for every natural number \(n\) there exists a normal quasi-algorithm \(\mathfrak A\) in the alphabet \(A^+\) such that \(\mathfrak A\) \(n\)-realizes \(G\) and \(\mathfrak A_3 \leq f(n)\).

Theorem 2. Let \(G_1,\ldots,G_k\) and \(F\) be propositional formulas, and let \(f_1,\ldots,f_k\) be general recursive functions such that \(f_i\) is an upper bound for the realizability complexity of \(G_i\) \((1 \leq i \leq k)\), and suppose that the formula \((G_1 \& \ldots \& G_k)\supset F\) is derivable in the intuitionistic propositional calculus. Then there exist natural numbers \(C_0,C_1,\ldots,C_k\) such that the function

\[ \lambda x\sum_{i=1}^{k} C_i\cdot f_i(x)+C_0 \]

is an upper bound for the realizability complexity of \(F\).

We shall say that a propositional formula \(G\) has a trivial upper bound for realizability complexity if, for some natural numbers \(C_1\) and \(C_2\), the function \(\lambda x\, C_1\cdot 14^x+C_2\) is an upper bound for the realizability complexity of \(G\).

From Theorem 1 of paper (⁷), Theorem 9 of paper (⁹), and Theorems 1 and 2 of the present paper, the following can be obtained:

Theorem 3. Every propositional formula \(G\) in one variable either has no upper bound for realizability complexity, or has a trivial upper bound for realizability complexity.

The author expresses deep gratitude to A. A. Markov and N. M. Nagorny for their attention to the work and valuable advice.

Computing Center
Academy of Sciences of the USSR
Moscow

Received
4 VI 1970

REFERENCES

¹ A. A. Markov, Tr. Matem. inst. im. V. A. Steklova AN SSSR, 42 (1954).
² S. K. Kleene, Introduction to Metamathematics, Moscow, 1957.
³ N. A. Shanin, Tr. Matem. inst. im. V. A. Steklova AN SSSR, 43 (1955).
⁴ A. A. Markov, Izv. AN SSSR, ser. matem., 31, No. 1, 161 (1967).
⁵ S. C. Kleene, J. Symbolic Logic, 10, 109 (1945).
⁶ G. F. Rose, Trans. Am. Math. Soc., 75, 1 (1953).
⁷ I. Nishimura, J. Symbolic Logic, 25, 327 (1960).
⁸ V. A. Yankov, Izv. AN SSSR, ser. matem., 32, No. 1, 208.
⁹ V. I. Khomich, DAN, 191, No. 5, 1004 (1970).