Yu. T. Medvedev

INTERPRETATION OF LOGICAL FORMULAS BY MEANS OF FINITE PROBLEMS AND ITS CONNECTION WITH REALIZABILITY THEORY

(Presented by Academician A. N. Kolmogorov, VIII 4, 1962)

In the paper ([1]) a certain notion of general validity of logical formulas was investigated, based on their interpretation as composite problems of Kolmogorov type. Theorems 1 and 2 of the present paper and the results of the preceding one show that, for formulas of the Heyting calculus H which do not contain at least one of the connectives $\neg$, $\vee$, $\supset$, general validity is equivalent to derivability in H. It follows from Theorem 7 that this assertion remains true when general validity in our sense is replaced by Kleene–Rosser realizability. The latter fact had been known only in the part concerning the connective $\supset$ (([2]), Theorem 7.5).

1. The class of formulas of the calculus H that are generally valid in the sense of ([1]) (i.e., the class of always solvable formulas) will be denoted by $\mathfrak{T}$.

Theorem 1. If a formula $A$ does not contain disjunction $\vee$, then from $A \in \mathfrak{T}$ it follows that $A$ is derivable in H.

The proof is carried out by the same method as was used in proving Theorem 1 in ([1]). (The essential point is the establishment of a lemma analogous to Lemma 3 in ([1]); it is formulated verbatim in the same way, but the term “critical implication” is defined differently.)

Theorem 2. If a formula $A$ does not contain implication $\supset$, then from $A \in \mathfrak{T}$ it follows that $A$ is derivable in H.

This theorem follows from the following three easily proved propositions, which are also of independent interest.

Theorem 3 (Rose, ([2]), Theorem 7.1). If a formula $A$ of the calculus H is not derivable in H and contains no implication, then $A$ is equivalent in H to the disjunction of a certain number of formulas not derivable in the classical propositional calculus.

Theorem 4. If a formula $A$ has the form of a disjunction, then from $A \in \mathfrak{T}$ it follows that at least one member of this disjunction belongs to $\mathfrak{T}$.

Theorem 5. If $A \in \mathfrak{T}$, then $A$ is derivable in the classical propositional calculus.

2. We denote by $\mathrm{P}$ the class of realizable formulas of the calculus H.

Theorem 6. From $U \in \mathrm{P}$ it follows that $U \in \mathfrak{T}$.

In view of the comparative simplicity of the proof of this theorem, it is given below (with some abbreviation).

Definition 1. Let $E_1,\ldots,E_n$ be some system of sets of natural numbers. We shall say that this system has an effectively empty intersection if there exists a general recursive function $p$ such that from $p(x)=y$ it follows that $1 \leq y \leq n$ and $x \in E_y$.

Remark. By analogy with the notion of multiple separability in descriptive set theory ([3]) one may introduce the following definition: sets of natural numbers $E_1,\ldots,E_n$ are called recursively multiply separable if there exist recursive sets $B_1,\ldots,B_n$ such that $E_i \subseteq B_i$ for $1 \leq i \leq n$ and the intersection of all the $B_i$ is empty. It is easy to show that the property of a system of sets $E_1,\ldots,E_n$ having effectively empty intersection is equivalent to the sets of this system being recursively multiply separable.

Lemma 1. For every natural number (n \geq 2) there exists a system of (n) pairwise disjoint recursively enumerable sets that has no effectively empty intersection.

For the proof, consider a partial recursive function (w) of two variables, universal for the class of all partial recursive functions of one variable. Denote by (q) the partial recursive function (q(x) \simeq w(x,x)), and let (E_i) ((1 \leq i \leq n)) be the set of all those (x) for which (q(x)=i). We shall show that the system of sets (E_1,\ldots,E_n) is the desired one. First of all, it is clear that the sets of this system are recursively enumerable and pairwise disjoint. Suppose that the system has an effectively empty intersection, and that (p) is the general recursive function referred to in Definition 1. By the universality of (w), there exists an (e) such that (p(x)=w(e,x)) for all (x). Denoting (p(e)) by (k), we shall have
[
k=w(e,e)=q(e).
]
From the definition of the function (p) it follows that (1 \leq k \leq n) and (e \in E_k), whence (q(e) \ne k). The contradiction obtained proves that the system (E_1,\ldots,E_n) has no effectively empty intersection.

Lemma 2. For every natural number (N \geq 2) there exists a system of (N-1) pairwise disjoint recursively enumerable sets
[
E_1,\ldots,E_{N-1},
]
having the following property: the system of (N) sets
[
E_1,\ldots,E_{N-1}, E_N,
]
where (E_N) is the complement of the set
[
\bigcup_{1}^{N-1} E_i,
]
has no effectively empty intersection.

For the proof it suffices to take, as (E_1,\ldots,E_{N-1}), the sets constructed in the proof of Lemma 1. Then for (N=2) the assertion being proved follows from the fact that (E_1) is not a recursive set. For (N>2), assuming that there exists a general recursive function (\tilde p) satisfying the condition of Definition 1 with respect to the system (E_1,\ldots,E_{N-1}, E_N), one can easily construct (using the recursive enumerability of the sets (E_1,\ldots,E_{N-1})) a general recursive function (p) satisfying this condition with respect to the system (E_1,\ldots,E_{N-1}), in contradiction with Lemma 1. This completes the proof of Lemma 2.

Now let the formula (U(z_1,\ldots,z_m)), constructed from propositional letters (z_1,\ldots,z_m), not be always solvable, i.e. (U \notin \mathrm T). Our aim is to prove that then (U \notin \mathrm P). By the refutability of (U), this formula is not solvable on some system of finite sets (F_1,\ldots,F_m). We may assume that all the (F_i) are the same and coincide with the set (I_n) of natural numbers (k) satisfying the inequality (1 \leq k \leq n), for some natural (n \geq 1). This follows from the following proposition, whose proof we omit: if some formula is solvable on a system of sets (G_1,\ldots,G_m), then it is also solvable on such a system of sets (F_1,\ldots,F_m) for which, for all (i=1,\ldots,m), the number of elements of the set (F_i) does not exceed the number of elements of the set (G_i).

Let us number, in some definite way, all possible ordered sequences of (m) elements of the form
[
c=(X_1,\ldots,X_m),
]
where the (X_j) are subsets of (I_n): (X_j \subseteq I_n) for (1 \leq j \leq m). We obtain a sequence
[
c_1,\ldots,c_N,
]
where
[
c_s=(X_1^{(s)},\ldots,X_m^{(s)})
]
for (1 \leq s \leq N), and moreover
[
N=2^{mn} \geq 2.
]

Let (E_1,\ldots,E_N) be a system of sets whose existence is established in Lemma 2. There exist logical-arithmetical formulas
[
\alpha_1(t),\ldots,\alpha_N(t),
]
containing the single free numerical variable (t) and having the property that (\alpha_i(t)) expresses the predicate (k \in E_i). This means that if, for any natural number (k), (k^) denotes the term representing (k) in the formal arithmetic system under consideration, then for every (s), (1 \leq s \leq N), the relation (k \in E_s) is equivalent to the truth of the statement (\alpha_s(k^)) under the intended interpretation of the predicates…

predicate (\alpha_s(t)). Denote by (\varepsilon_0) and (\varepsilon_1) the arithmetical formulas expressing, respectively, the statements (0=0) and (0=1), and by (\beta_j(t)) the arithmetical formula

[
\Sigma_{r\leq n}\Pi_{s\leq N}\bigl(\delta_{j,r,s}\vee \neg \alpha_s(t)\bigr),
]

where (\delta_{j,r,s}) coincides with (\varepsilon_0) when (r\in X_j^{(s)}), and with (\varepsilon_1) when (r\notin X_j^{(s)}).

Let us show that the arithmetical formula (\omega(t)), obtained from (U(z_1,\ldots,z_m)) by substituting (\beta_1(t),\ldots,\beta_m(t)) for (z_1,\ldots,z_m), is not realizable. This will prove that (U\notin P). Denote by (\mathfrak A_j(k)) the finitary problem for which (\varphi(\mathfrak A_j(k))=I_n), (\chi(\mathfrak A_j(k))=X_j^{(s)}), where (s) ((1\leq s\leq N)) is determined by the condition (k\in E_s) (by the properties of the system (E_1,\ldots,E_N), such an (s) exists and is unique).

Lemma 3. For the realizability of the formula (\Pi_{s\leq N}(\delta_{j,r,s}\vee \neg \alpha_s(k^))), i.e. of the term with number (r) of the disjunction (\beta_j(k^)), it is necessary and sufficient that the condition (r\in\chi(\mathfrak A_j(k))) be satisfied.

For the proof, note that a formula of the form (\alpha_s(k^)) is realizable if and only if the predicate expressed by the formula (\alpha_s(t)) is true for (t=k). This follows from known results of realizability theory ({}^{(4)}) and from the fact that (\alpha_s(k^)) has the form ((\exists u)\gamma(u)) (for (1\leq s\leq N-1)) or the form ((\forall u)\gamma(u)) (for (s=N)), where the formula (\gamma(u)) expresses a primitive recursive predicate. Therefore, for the realizability of the conjunction under consideration it is necessary and sufficient that, for those (s) for which (\delta_{j,r,s}) is (\varepsilon_1), the formula (\alpha_s(k^*)) express a false statement. In other words, from (r\notin X_j^{(s)}) it must follow that (k\notin E_s). This is equivalent to the condition (r\in\chi(\mathfrak A_j(k))).

Lemma 4. Let (A(z_1,\ldots,z_m)) be any formula of the calculus (H). Denote by (\omega_A(k^)) the formula (A(\beta_1(k^),\ldots,\beta_m(k^*))), and by (\mathfrak A_A(k)) the finitary problem (A(\mathfrak A_1(k),\ldots,\mathfrak A_m(k))). Then there exist computable functions (f_A) and (g_A) such that, for all (k,e,) and (h), the following conditions hold:

1) If (e) realizes (\omega_A(k^*)), then (f_A(e)\in\chi(\mathfrak A_A(k))).

2) If (h\in\chi(\mathfrak A_A(k))), then (g_A(h)) realizes (\omega_A(k^*)).

In this formulation, the domain of definition of the function (g_A) and the range of values of the function (f_A) are assumed to coincide with (\varphi(\mathfrak A_A(k))) (obviously, it does not depend on (k)).

The proof is by induction on the number of logical connectives of the formula (A). If this number is zero, then (A) coincides with the letter (z_j) for some (j), (1\leq j\leq m). Then (\omega_A(k^)) coincides with (\beta_j(k^)), and (\mathfrak A_A(k)) with (\mathfrak A_j(k)). In this case the existence of the functions (f_A) and (g_A) follows almost immediately from Lemma 3 and from the definition of realizability of formulas (taking into account the form of the formulas (\beta_j(k^))). Suppose now that the number of logical connectives of the formula (A) is not zero and that, for formulas with a smaller number of connectives, the assertion of the lemma is true. Then (A) is a formula of one of four forms: (B\,\&\,C), (B\vee C), (B\supset C), or (\neg B). We restrict ourselves to an analysis of the third case, i.e. of a formula (A) of the form (B\supset C). Let, as in the proof of Lemma 1, (w) be a universal partial recursive function, and let (x) realize (\omega_A(k^)). For every (b\in\varphi(\mathfrak A_B(k))), put

[
h(b)=f_C(w(x,g_B(b))).
]

It is easy to verify that if (b\in\chi(\mathfrak A_B(k))), then (h(b)\in\chi(\mathfrak A_C(k))). Thus, to each (x) realizing (\omega_A(k^*)), the written expression assigns (obviously, in a computable way) a function (h\in\chi(\mathfrak A_A(k))), and thereby defines a certain function (f_A) with the required property. The function (g_A) is constructed similarly, using the functions (f_B) and (g_C).

We proceed directly to the proof of Theorem 6. Suppose that the formula (\omega(t)) is realizable. This entails the existence of a general recursive function (r) such that, for every natural (k), the number (r(k)) realizes (\omega(k^*)). We shall denote (\mathfrak A_U(k)) simply by (\mathfrak A(k)). By Lemma 4 there exists a computable function (f) such that, for every natu-

(k) and every (x) realizing (\omega(k^*)), we have (f(x) \in \chi(\mathfrak A(k))). Consequently, for the computable function (f_1(k)=f(r(k))), for every (k) we have (f_1(k) \in \chi(\mathfrak A(k))). Let (\mathfrak A^{(s)}) ((1 \leq s \leq N)) be the finitary problem (U(\mathfrak A^{(s)}_1,\ldots,\mathfrak A^{(s)}_m)), where (\varphi(\mathfrak A^{(s)}_j)=I_n,\ \chi(\mathfrak A^{(s)}_j)=X^{(s)}_j). Obviously, from (k \in E_s) it follows that (\mathfrak A^{(s)}) coincides with (\mathfrak A(k)). Since (U(z_1,\ldots,z_m)) is not solvable on the system of sets (F_1,\ldots,F_m), where each (F_j) is (I_n), for every (k) there exists a least (s), (1 \leq s \leq N), such that (f_1(k) \in \chi(\mathfrak A^{(s)})), and therefore (k \in E_s). Using the computability of (f_1), it is easy to specify a general recursive function which finds (s) from the given (k). Denoting this function by (p), we have (1 \leq p(k) \leq N), and from (p(k)=s) it follows that (k \in E_s). Hence the system (E_1,\ldots,E_N) has an effectively empty intersection, contrary to the original assumption. We must conclude that the formula (\omega(t)) is not realizable, as was required.

From Theorems 1, 2, 6 and the main result of paper ({}^{1}) (Theorem 1), we obtain the following result.

Theorem 7. Let a formula (U) of the calculus (\mathbf H) contain none of the connectives (\neg,\ \vee,\ \supset). Then from (U \in P) it follows that (U) is derivable in (\mathbf H).

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

Received
25 VII 1962

REFERENCES

1. Yu. T. Medvedev, DAN, 142, No. 5, 1015 (1962).
2. Gene F. Rose, Trans. Am. Math. Soc., 75, No. 1, 1 (1953).
3. P. S. Novikov, DAN, 2, No. 5, 273 (1934).
4. S. C. Kleene, Introduction to Metamathematics, N.Y.—Toronto, 1952.