UDC 51.01:164

MATHEMATICS

F. A. KABAKOV

ON THE INTUITIONISTIC DERIVABILITY OF CERTAIN REALIZABLE FORMULAS OF PROPOSITIONAL LOGIC

(Presented by Academician P. S. Novikov on 3 XI 1969)

The well-known result of J. Rose \((^1)\) on the incompleteness of Heyting’s intuitionistic propositional calculus (the calculus \(H\)) with respect to realizability makes it interesting to search for such nontrivial classes of propositional formulas for which realizability and derivability in Heyting’s calculus coincide. In this direction there are a number of results. Thus, Rose himself showed in \((^1)\) that realizability and derivability in Heyting’s calculus coincide for propositional formulas containing no implication. In \((^2)\) it was proved that if the formulas \(A\) and \(B\) contain no implication, then the formula \(A \supset B\) is realizable and derivable in \(H\) simultaneously. Finally, Yu. T. Medvedev \((^3)\) proved that realizability and derivability in \(H\) coincide for every formula not containing at least one of the connectives \(\neg, \vee, \supset\). The formula constructed by Rose that is realizable and not derivable in \(H\) has the form \(((A \supset B) \supset C) \supset C\), i.e., contains an “implication in the premise” (and this property here, so to speak, is iterated twice). The aim of the present note is to show that, without resorting to sufficiently complicated accumulations of the implication sign, the gap between derivability in the intuitionistic propositional calculus and realizability cannot be achieved.

We consider propositional formulas constructed in the usual way from propositional variables \(p_1, p_2, \ldots\), the connectives \(\&, \vee, \supset, \neg\), and parentheses \((,)\). All necessary information on the theory of realizability for arithmetical formulas, i.e., for formulas of the ordinary logical-arithmetical language considered in Kleene’s book \((^4)\), may be found in Ch. XV, § 82 of that book. A propositional formula \(A(p_1,\ldots,p_n)\) is called realizable if there is an algorithm transforming every \(n\)-term sequence \(F_1,\ldots,F_n\) of closed arithmetical formulas into a realization of the arithmetical formula \(A(F_1,\ldots,F_n)\). The assertions “the formula \(\Phi\) is realizable” and “the formula \(\Phi\) is derivable in the intuitionistic propositional calculus” are abbreviated respectively by \(r\Phi\) and \(\vdash \Phi\). By “Nelson’s theorem” we shall here call the proposition “if \(\vdash \Phi\), then \(r\Phi\),” which is a well-known consequence of the analogous proposition on arithmetical formulas, proved by D. Nelson in \((^5)\).

To each propositional formula \(A\) we assign, in the following way, a number \(\operatorname{im}(A)\), which, in the sense of interest to us, characterizes the presence in \(A\) of the connective \(\supset\): (I) if \(A\) contains no occurrences of the connective \(\supset\), or has the form \(\neg A'\), then \(\operatorname{im}(A)=0\); (II) \(\operatorname{im}(A \& B)=\operatorname{im}(A \vee B)=\max(\operatorname{im}(A),\operatorname{im}(B))\); (III) \(\operatorname{im}(A \supset B)=1+\max(\operatorname{im}(A),\operatorname{im}(B))\).

Denote by \(\operatorname{Im}_n\) the class of propositional formulas \(A\) for which \(\operatorname{im}(A)\le n\). We shall be interested in the class \(\operatorname{Im}_1\). Informally speaking, this class consists of exactly those formulas which can be constructed with the help of the connectives \(\&, \vee\), and \(\neg\), starting from arbitrary formulas that are negations or that contain no more than one occurrence of the connective \(\supset\). (A formula \(A\) of the class \(\operatorname{Im}_1\), of course, may contain subformulas \(A'\) with \(\operatorname{im}(A')>1\), including any iterations of “implication in the premise,” but,

obviously, always only under the sign of negation, which does not worsen the formula \(A\) in the sense of interest to us, since the negation of any propositional formula is intuitionistically equivalent to some formula not containing implication.)

Theorem 1. Every realizable formula of the class \(\operatorname{Im}_1\) is derivable in the intuitionistic propositional calculus.

We shall show that for every formula \(A(p_1,\ldots,p_n)\) not derivable in \(H\) and belonging to the class \(\operatorname{Im}_1\), a refutation \({}^{(6)}\) of this formula can be effectively constructed, i.e., such a system \(F_1,\ldots,F_n\) of arithmetical formulas (possibly with free variables) for which the arithmetical formula \(A(F_1,\ldots,F_n)\) is not realizable. The theorem will follow from this.

Lemma 1. If the propositional formulas \(A\) and \(B\) are equivalent (i.e., if \(\vdash (A \supset B)\ \&\ (B \supset A)\)), then from any refutation of one of them one can effectively construct a refutation of the other.

Lemma 2. From any refutation of a given propositional formula \(A\) one can effectively construct a refutation of any propositional formula \(B\) from which \(A\) is obtained by the substitution rule.

These two lemmas are immediate consequences of D. Nelson’s theorem and the corresponding definitions.

Lemma 3. For every propositional formula that contains no implication sign and is not derivable in \(H\), one can effectively construct its refutation.

In essence, Lemma 3 is a paraphrase of Theorem 7.5 in \({}^{(1)}\), whose proof contains the construction of the desired refutation.

Lemma 4. For every propositional formula not derivable in \(H\) of the form \(A \supset B\), where \(A\) and \(B\) contain no implication sign, one can effectively construct its refutation.

For the proof of Lemma 4 one may refer to the procedure from the proof of the main result in \({}^{(2)}\). With the application of Lemmas 1, 2, 3 this procedure leads to the construction of the required refutation.

Theorem 1 can now be proved by induction on the logical length \(\lambda(A)\) of the formula \(A\). Here the basis of the induction (the formula is a propositional variable) is obvious. To carry out the induction step, suppose that the theorem is true for formulas of logical length less than \(k\), and let \(\lambda(A)=k>0\). The case \(A \supset \neg A'\) is obvious. Let \(A \supset B \supset C\). From \(\operatorname{im}(A)\leq 1\) it follows that \(\operatorname{im}(B)=\operatorname{im}(C)=0\). We apply Lemma 4 (and, possibly, Lemma 1, if \(B \supset \neg B'\) or \(C \supset \neg C'\)). If \(A \supset B\ \&\ C\), then from \(\operatorname{m}(B\ \&\ C)\leq 1\) and \(\nvdash B\ \&\ C\) it follows that \((\operatorname{im}(B)\leq 1\ \&\ \nvdash B)\vee(\operatorname{im}(C)\leq 1\ \&\ \nvdash C)\). The true member of this disjunction is found effectively; to it we apply the induction hypothesis, after which a refutation is easily constructed also for \(B\ \&\ C\). Finally, let \(A \supset B\vee C\). From \(\operatorname{im}(B\vee C)\leq 1\) and \(\nvdash B\vee C\) it follows that \((\operatorname{im}(B)\leq 1\ \&\ \nvdash B)\ \&\ (\operatorname{im}(C)\leq 1\ \&\ \nvdash C)\). By the induction hypothesis there are refutations of the formulas \(B\) and \(C\). From these refutations, according to F. L. Varshavskii’s theorem \({}^{(6)}\), a refutation can be effectively constructed also for \(B\vee C\). The theorem is proved.

The example constructed by Rose \({}^{(1)}\) of a realizable formula not derivable in \(H\) shows that our theorem is false for the class \(\operatorname{Im}_3\). For the class \(\operatorname{Im}_2\) the question apparently remains open; in any case, all other examples of realizable formulas not derivable in \(H\) that are known to the author at present belong to the classes \(\operatorname{Im}_n\), where \(n\geq 3\)*.

* Note added in proof. After the present note had been sent to press, F. L. Varshavskii and Yu. T. Medvedev, in private conversation, drew my attention to the realizable formula not derivable in \(H\)

\[ ((\neg a\vee \neg\neg a)\supset(\neg b\vee \neg\neg b))\supset (\neg a\supset \neg b)\vee(\neg a\supset \neg\neg b)\vee(\neg\neg a\supset \neg a)\vee(\neg\neg a\supset \neg\neg b). \]

It is not hard to see that this formula is equivalent to some formula of the class \(\operatorname{Im}_2\). Thus \(\operatorname{Im}_1\) is the only one of the classes \(\operatorname{Im}_2\) for which Theorem 1 is valid.

Theorem 2. Every finitely generally significant \((^{7})\) formula of the class \(\mathrm{Im}_1\) is derivable in the intuitionistic propositional calculus.

The proof of this theorem can be carried out according to the same plan as the proof of Theorem 1, using the known properties of finite general significance \((^{7,3})\). Then Theorem 1 could have been obtained as an immediate consequence of Theorem 2 and Theorem 6 of \((^{3})\), according to which every realizable propositional formula is finitely generally significant. We have, however, preferred here a presentation that does not depend on the notion of finite general significance and its properties.

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

Received
27 X 1969

CITED LITERATURE

\(^{1}\) G. F. Rose, Trans. Am. Math. Soc., 75, 1 (1953).
\(^{2}\) F. A. Kabakov, Zs. math. Logik und Grundlagen d. Math., 9, 97 (1963).
\(^{3}\) Yu. T. Medvedev, DAN, 158, No. 4, 771 (1963).
\(^{4}\) C. K. Kleene, Introduction to Metamathematics, Moscow, 1957.
\(^{5}\) D. Nelson, Trans. Am. Math. Soc., 61, 307 (1947).
\(^{6}\) F. L. Varkhovskii, DAN, 161, No. 6, 1257 (1965).
\(^{7}\) Yu. T. Medvedev, DAN, 142, No. 5, 1015 (1962).