UDC 517.12

MATHEMATICS

M. M. KIPNIS

ON A PROPERTY OF PROPOSITIONAL FORMULAS

(Presented by Academician P. S. Novikov on 6 VII 1966)

1. A. A. Markov stated the following proposition: whatever the propositional formulas \(P_1\) and \(P_2\) may be, if the formula \((P_1 \vee P_2)\) is realizable, then either \(P_1\) is realizable or \(P_2\) is realizable. In the present note it is shown that this proposition cannot be refuted by an example (Theorem 1 and Corollary 1). A similar assertion was proved classically by F. L. Varakhovskii \((^1)\), but the definition of a realizable formula in his work differs from the constructive variant of J. F. Rose’s definition \((^2)\) adopted here.

2. Let \(n\) be an arbitrary natural number. Fix some Gödel numbering of \(n\)-term systems of closed logical-arithmetical formulas. For convenience we shall assume that to each number there corresponds some system. By the symbol \(A_k^j\) \((1 \leq j \leq n)\) we denote the \(j\)-th term of the system with Gödel number \(k\). Let \(P\) be a propositional formula in the variables \(p_1, \ldots, p_n\), and let \(\varphi\) be a partial recursive function of one argument (p.r.f.-1). We shall say that \(\varphi\) realizes \(P\) if, for every \(k\), \(\varphi(k)\) is defined and realizes, in the sense of Kleene \((^3)\), the formula \(P(A_k^1, \ldots, A_k^n)\) (here \(P(A_k^1, \ldots, A_k^n)\) denotes the result of substituting the formulas \(A_k^1, \ldots, A_k^n\) into the formula \(P\) in place of the variables \(p_1, \ldots, p_n\), respectively). A propositional formula \(P\) will be called realizable if there exists a p.r.f.-1 \(\varphi\) realizing the formula \(P\).

3. Theorem 1. Whatever the p.r.f.-1 \(\varphi\) and the propositional formulas \(P_1\) and \(P_2\) may be, such p.r.f.-1 \(\psi_1\) and \(\psi_2\) can be constructed that, if \(\varphi\) realizes the formula \((P_1 \vee P_2)\), then there cannot fail to exist a number \(s\) such that: 1) \(s = 1\) or \(s = 2\); 2) \(\psi_s\) realizes \(P_s\).

We briefly outline the proof of Theorem 1. Construct a sequence \(M\) of recursively enumerable sets, taking \(i \in M_k\) if and only if the formula

\[ \exists y\,(T_1(i,i,y)\&U(y)=k) \]

is realizable (with respect to the predicates \(T_1(a,x,y)\) and \(U(y)=k\), see \((^4)\), pp. 248 and 250). It can be shown that if \(k \ne r\), then the sets \(M_k\) and \(M_r\) are disjoint and recursively inseparable \((^5)\).

We denote by the symbol \(A_{im}^j\) the formula

\[ \mathop{\&}_{k=1}^{m}\bigl(\exists y\,(T_1(i,i,y)\&U(y)=k)\supset A_k^j\bigr)\quad (1 \leq j \leq n). \]

It can be shown that if

\[ i \in M_k,\qquad m \geq k, \tag{1} \]

then the formulas \(A_{im}^j \sim A_k^j\) are realizable and, consequently, for any propositional formula \(P\) in the variables \(p_1,\ldots,p_n\) the formula

\[ P(A_k^1,\ldots,A_k^n)\sim P(A_{im}^1,\ldots,A_{im}^n) \tag{2} \]

is realizable.

Let \(\rho(i,m)\) be such a general recursive function that for any natural numbers \(i\) and \(m\) the number \(\rho(i,m)\) is a Gödel number of the system \(A^1_{im}, \ldots, A^n_{im}\). Using the pairwise recursive inseparability of the sets of the sequence \(M\), one can show that the following is true.

Lemma. Whatever the p.r.f.-1 \(\varphi\) and the propositional formulas \(P_1\) and \(P_2\) may be, there cannot fail to exist a number \(s\) such that: 1) \(s=0\) or \(s=1\); 2) if \(\varphi\) realizes the formula \((P_1 \vee P_2)\), then for every \(k\) there are natural numbers \(i,m\), and \(c\) such that \(i \in M_k\), \(m \geqslant k\), and
\[ \varphi(\rho(i,m)) = 2^s \cdot 3^c. \]

Using this lemma and the realizability of formula (2) under condition (1), one can carry out a proof of Theorem 1 that is consistent with both the classical and the constructive understanding of mathematical judgments. From Theorem 1, with the aid of the principle of constructive choice \({}^{(6)}\), there is derived

Corollary 1. Whatever the p.r.f.-1 \(\varphi\) and the propositional formulas \(P_1\) and \(P_2\) may be, one can construct such a p.r.f.-1 \(\psi_1\) that, if \(\varphi\) realizes the formula \((P_1 \vee P_2)\) and \(P_2\) is not realizable, then \(\psi_1\) realizes \(P_1\).

Within classical logic, from Theorem 1 one can obtain

Corollary 2. If the propositional formula \((P_1 \vee P_2)\) is realizable, then the formula \(P_1\) is realizable or the formula \(P_2\) is realizable.

1. The proof of Theorem 1 found by the author does not, however, give an algorithm which, for each realizable propositional formula of the form \((P_1 \vee P_2)\), would indicate that one of the formulas \(P_1, P_2\) which is realizable. The question of the existence of such an algorithm remains open.

Moscow State University
named after M. V. Lomonosov

Received
30 VI 1966

REFERENCES

1. F. L. Varpakhovskii, DAN, 161, No. 6, 1257 (1965).
2. G. F. Rose, Trans. Am. Math. Soc., 75, 1 (1953).
3. S. C. Kleene, J. Symbolic Logic, 10, 109 (1945).
4. S. K. Kleene, Introduction to Metamathematics, IL, 1957.
5. S. C. Kleene, Proc. Koninkl. Nederl. Akad. Wet., A 53, 800 (1950).
6. A. A. Markov, Tr. Matem. inst. im. V. A. Steklova AN SSSR, 67, 8 (1962).