MATHEMATICS

V. A. YANKOV

ON REALIZABLE FORMULAS OF PROPOSITIONAL LOGIC

(Presented by Academician P. S. Novikov, 20 III 1963)

1. Formulas of propositional logic are constructed on the basis of an infinite sequence of propositional variables with the help of the logical connectives \(\&,\ \vee,\ \supset,\ \neg\) and parentheses \(\left(^{1}\right)\). In the exposition we shall use conjunction and disjunction as multi-place connectives, each time understanding the formula
   \(A_1 \& \ldots \& A_k\) as
   \((A_1 \& (A_2 \& \ldots \& (A_k)\ldots))\) (similarly for disjunction). We shall also sometimes write \(A_1 \& \ldots \& A_k\) and \(A_1 \vee \ldots \vee A_k\), respectively, in the form \(\displaystyle \mathop{\&}_{i=1}^{k} A_i,\ \displaystyle \bigvee_{i=1}^{k} A_i\).

The definition of realizability of formulas of logico-arithmetical calculus is given in Kleene’s paper \(\left(^{2}\right)\), and also in his monograph \(\left(^{1}\right)\).

We shall call a formula \(P\) of propositional logic realizable if there exists an algorithm which, for every substitution in \(P\) of closed logico-arithmetical formulas in place of propositional variables, makes it possible to obtain a realization of the result of the substitution. This definition is a constructive analogue of the definition of J. R. Rose \(\left(^{3}\right)\).

It is known that all formulas of propositional logic derivable in Heyting’s intuitionistic calculus are realizable \(\left(^{4}\right)\) (on Heyting’s calculus see \(\left(^{5}\right)\) or \(\left(^{1}\right)\)). The formula \(\neg \neg a \supset a\) (\(a\) is a propositional variable) is not realizable. Rose showed that the formula
\[ ((\neg \neg M \supset M) \supset \neg \neg M \vee \neg M) \supset \neg \neg M \vee \neg M, \]
where \(M\) is \(\neg a \vee \neg b\) (\(a\) and \(b\) are distinct propositional variables), is realizable, but not derivable in the intuitionistic propositional calculus. In what follows we shall denote this formula by the letter \(J\).

Theorem 1 indicates also some further formulas, not derivable in the intuitionistic propositional calculus and realizable, and establishes their connection with one another and with the formula \(J\). The use of the derivability symbol \(\vdash\) in the present context differs from its use in \(\left(^{1}\right)\). \(A \vdash B\), if \(B\) is derivable from \(A\) by means of the intuitionistic axioms, modus ponens, and the substitution rule.

By the symbol \(I_n\) \((n \geqslant 3)\) we shall denote the formula
\[ \mathop{\&}_{k<m} \neg(a_k \& a_m)\ \&\ \mathop{\&}_{i=1}^{\,n-1} ((\neg a_1 \& \ldots \& \neg a_{i-1} \& \neg a_{i+1} \& \ldots \& \neg a_{n-1}) \supset \]
\[ \supset a_i \vee a_n)) \supset a_n \vee \neg a_n; \]
where \(a_1,\ldots,a_n\) are pairwise distinct propositional variables.

By the symbol \(K_n\) \((n \geqslant 3)\) we shall denote the formula
\[ \left( \mathop{\&}_{i<j} \neg(a_i \& a_j)\ \&\ \mathop{\&}_{i<j} ((\neg a_1 \& \ldots \& \neg a_{i-1} \& \neg a_{i+1} \& \ldots \& \neg a_n) \supset a_i \vee a_j) \right) \supset \bigvee_{i=1}^{n} a_i, \]
where \(a_i\) are as in the definition of \(I_n\).

Finally, by the symbol \(R\) we shall denote the formula
\[ (((\neg \neg a \supset a) \supset a \vee \neg a)\ \&\ ((\neg \neg b \supset b) \supset \]
\[ \supset b \vee \neg b)\ \&\ \neg(a \& b)\ \&\ \neg(\neg a \& \neg b)) \supset \neg a \vee \neg b, \]
where \(a\) and \(b\) are distinct propositional variables.

Theorem 1. a) The formulas \(I_3\) and \(R\) are both realizable and neither is derivable from the other (and, a fortiori, they are not derivable in the intuitionistic calculus).

b) \(I_3 \vdash J\), but it is not true that \(J \vdash I_3\).

c) For every \(n \geq 3\), the formulas \(I_n\) and \(K_n\) are not derivable in the intuitionistic propositional calculus, but \(I_3 \vdash I_n\) and \(I_n \vdash K_n\) (and hence both \(I_n\) and \(K_n\) are realizable by Nelson’s results \((^4)\)).

Fig. 1

1. The set of seven elements \(0, 1, a, b, c, d, e\), partially ordered in accordance with Fig. 1, where \(1\) is the least and \(0\) the greatest element, is a finite implicative structure (see \((^6)\)).

The implicative structure \(M\) just described is identical to the matrix \(\Gamma\) \((\Gamma(I_0)\times I_0)\), obtained from the classical matrix by the operations of direct product and \(\Gamma\), see \((^6)\). There also is given the definition of the general validity of a formula on an implicative structure.

Theorem 2. Every realizable formula of propositional logic is generally valid on \(M\).

We shall outline the main stages of the proof of this theorem (in what follows \(a \exp b\) will denote the same thing as \(a^b\)).

Let \(K_{y,z}\) be the set of natural numbers of the form

\[ (2 \exp y)\cdot(3 \exp ((2 \exp p)\cdot(3 \exp ((2 \exp z)\cdot(3 \exp q))))) \]

for given \(y\) and \(z\) (all lowercase Latin letters denote variables, which subsequently range over the natural numbers). Then the meaningful predicate “\(t\) is the Gödel number of a general recursive function whose values belong to \(K_{y,z}\)” can be expressed by a formula \(Q(t,y,z)\) of the logical-arithmetical language from \((^1)\). Let \(P(y,z)\) be the formula
\[ \forall t\,(t \leq y \supset \neg Q(t,y,z)), \]
and let \(R(y,z)\) be the formula
\[ P(y,z)\ \&\ \forall t\,(t<z \supset \neg P(y,z)). \]

Lemma 1. There is a proposition expressed by the formula

\[ \forall y\ \neg\neg \exists z\,R(y,z). \]

Let \(g(y)\) enumerate without repetitions some enumerable but not decidable set. Then the predicate \(g(y)=x\) is expressed in Kleene’s logical-arithmetical language \((^1)\) by some formula \(G(y,x)\). Let \(S(x)\) be the formula
\[ \exists y\,(G(y,x)\ \&\ \exists z\,R(y,z)). \]

Lemma 2. There is a proposition expressed by the formula

\[ \forall x\,(\neg\neg S(x)\equiv \exists y\,G(x,y)). \]

Lemma 3. Let \(x,y,k\) be such that: 1) \(k\) realizes the formula
\[ \neg\neg S(x)\supset S(x); \]
2) \(g(y)=x\); then \(k>y\).

With the aid of Lemmas 2 and 3 the main

Lemma 4. For every \(x\) the formula
\[ (\neg\neg S(x)\supset S(x))\equiv S(x)\vee \neg S(x) \]
is realizable, but the formula
\[ \forall x\,(\neg\neg S(x)\vee \neg S(x)) \]
is not realizable.

Introduce the following notation:

\[ \begin{aligned} F_0(x)&\text{ is the formula }0=0,\\ F_a(x)&\text{ is the formula }\neg S(x),\\ F_b(x)&\text{ is the formula }S(x),\\ F_c(x)&\text{ is the formula }S(x)\vee \neg S(x),\\ F_d(x)&\text{ is the formula }\neg\neg S(x),\\ F_e(x)&\text{ is the formula }\neg\neg S(x)\vee \neg S(x),\\ F_1(x)&\text{ is the formula }0=1. \end{aligned} \]

Let \(\alpha,\beta\) be variables ranging over the set \(M\).

Lemma 5. a) For any \(x\) and any \(\alpha\) and \(\beta\), the following formulas are realizable:

\[ F_{\alpha}(x)\ \&\ F_{\beta}(x) \equiv F_{\alpha\cap\beta}(x), \qquad F_{\alpha}(x)\vee F_{\beta}(x) \equiv F_{\alpha\cup\beta}(x), \]

\[ (F_{\alpha}(x)\supset F_{\beta}(x)) \equiv F_{\alpha-\beta}(x), \qquad \neg F_{\alpha}(x) \equiv F_{-\alpha}(x). \]

The formula \(\forall x F_{\alpha}(x)\) is realizable if and only if \(\alpha=0\).

With the aid of Lemma 5, Theorem 2 is also proved.

From Theorem 2 it follows, in particular, that the formulas
\[ ((\neg\neg a\supset a)\supset \neg a\vee \neg\neg a)\supset \neg a\vee \neg\neg a \quad\text{and}\quad \neg\neg a\vee(\neg\neg a\supset a) \]
are unrealizable (the unrealizability of the latter formula was first pointed out by F. A. Kabakov).

All the proofs are constructive, and the Leningrad principle is used (see (7)).

Mathematical Institute named after V. A. Steklov
Academy of Sciences of the USSR

Received
9 III 1963

CITED LITERATURE

1. S. K. Kleene, Introduction to Metamathematics, Moscow, 1957.
2. S. C. Kleene, J. Symbolic Logic, 10, 109 (1945).
3. G. F. Rose, Trans. Am. Math. Soc., 75, 1 (1953).
4. D. Nelson, Trans. Am. Math. Soc., 61, 307 (1947).
5. A. Heyting, Sitzungsber. Preus. Akad. Wiss., Phys.-math. Klasse, 42 (1930).
6. B. A. Yankov, DAN, 151, No. (1963).
7. A. A. Markov, Proceedings of the Third All-Union Mathematical Congress, 2, 1956, p. 146.