Yu. T. Medvedev

Finite Problems

(Presented by Academician A. N. Kolmogorov on 17 X 1961)

The completeness of Heyting’s intuitionistic propositional calculus \(H\), formulated by Heyting \((^1)\), has been investigated by many authors. An algebraic model with respect to which \(H\) is complete was constructed by Jaśkowski \((^2)\). McKinsey and Tarski \((^3)\) proved the completeness of \(H\) in the topological sense. From the substantive point of view, these and related results still do not settle the question of the completeness of \(H\), since they were obtained for models having the character of ad hoc interpretations. A. N. Kolmogorov \((^4)\) proposed a constructive interpretation of intuitionistic logic, the idea of which consists in identifying true logical formulas with “always solvable” problems. In accordance with this idea, completeness of a calculus interpreted as a certain calculus of problems means the derivability of any formula corresponding to an “always solvable” problem. Rose \((^5)\) discovered the incompleteness of the calculus \(H\), interpreted as a calculus of problems for the recursive realization of formulas \((^6)\).

The present work is devoted to the question of the completeness of the calculus \(P\), which is the positive part of \(H\) (i.e., the part in which negation is not considered). The model is formed by problems of Kolmogorov type, which we call finite, because they can be studied by means of the theory of finite sets. For such a model it is possible to prove the completeness of \(P\) in the sense indicated above (Theorem 1). An analogous result (Theorem 2) holds for the infinite analogue of finite problems—mass problems in the sense of the author’s earlier works \((^7,^8)\). In the concluding paragraph some remarks are given on formulas containing negation.

1. By a finite problem in the present work is meant any problem whose solution is an element of some previously known nonempty finite collection \(F\) of admissible possibilities. Examples of finite problems may be problems of determining the truth or falsity of propositions: here the set \(F\) contains two elements—“truth” and “falsehood,” and the solution is whichever of them is the truth value of the given proposition. Chess problems may also be regarded as finite under a suitable interpretation.

Let us note that to every precisely posed (not necessarily finite) problem \(\mathfrak{A}\) one can associate a finite problem \(\mathfrak{A}_n\) that “approximates” it. To this end, consider a language \(\mathcal{R}\) of which it is known that in it one can express the solution of the problem \(\mathfrak{A}\). As the collection \(F_n\) of admissible possibilities for \(\mathfrak{A}_n\) we take the set of all texts in the language \(\mathcal{R}\) having length \(\leq n\), and as solutions—those elements of \(F_n\) that express the solution of \(\mathfrak{A}\). (For sufficiently large \(n\), the finite problem \(\mathfrak{A}_n\) becomes equivalent to the problem \(\mathfrak{A}\). However, it may turn out that finding such an \(n\) is feasible only after solving \(\mathfrak{A}\).)

The set of solutions of a finite problem may be empty (in contrast to the set of admissible possibilities).

If \(F\) is the set of admissible possibilities for \(\mathfrak{A}\), and \(X\) is the set of all solutions, then we shall write

\[ F = \varphi(\mathfrak{A}), \qquad X = \chi(\mathfrak{A}). \]

The adjective “finitary,” referring to the word “problem,” will sometimes be omitted for brevity.

1. Let us introduce the operations of conjunction, implication, and disjunction of problems. First we agree on some notation. Let \(E_1\) and \(E_2\) be arbitrary sets. Then:

1) By \(E_1 \times E_2\) is denoted the Cartesian product of \(E_1\) by \(E_2\), i.e. the set of all ordered pairs \((x,y)\), where \(x \in E_1,\ y \in E_2\).

2) By \(E_2^{E_1}\) is denoted the set of all mappings of \(E_1\) into \(E_2\).

3) By \(\{E_1 \mid E_2\}\) is denoted the union of the sets \(E_1 \times \{1\}\) and \(E_2 \times \{2\}\), where \(\{1\}\) and \(\{2\}\) are one-element sets consisting respectively of the numerals 1 and 2. The set \(\{E_1 \mid E_2\}\) is naturally called the ordered union of \(E_1\) and \(E_2\).

Now let \(\mathfrak A_1\) and \(\mathfrak A_2\) be arbitrary finitary problems, with

\[ \varphi(\mathfrak A_1)=F_1,\qquad \chi(\mathfrak A_1)=X_1,\qquad \varphi(\mathfrak A_2)=F_2,\qquad \chi(\mathfrak A_2)=X_2 . \]

Each of the operations on problems introduced below is specified by indicating the set \(F\) of possibilities and the set \(X\) of solutions of the problem \(\mathfrak A\) that is the result of applying this operation.

I. For the conjunction \(\mathfrak A=\mathfrak A_1 \& \mathfrak A_2\) we put \(F=F_1 \times F_2,\ X=X_1 \times X_2\).

II. For the implication \(\mathfrak A=\mathfrak A_1 \supset \mathfrak A_2\) we put \(F=F_2^{F_1},\ X=\) (the set of all those mappings of \(F_1\) into \(F_2\), each of which maps \(X_1\) into \(X_2\)).

III. For the disjunction \(\mathfrak A=\mathfrak A_1 \vee \mathfrak A_2\) we put

\[ F=\{F_1 \mid F_2\},\qquad X=\{X_1 \mid X_2\}. \]

It is easy to verify that our definitions agree with the constructive interpretation given in the above-mentioned work of A. N. Kolmogorov.

1. Let us define the notion of an always solvable compound problem. A logical formula \(U(z_1,\ldots,z_m)\), containing no connectives except \(\&,\ \supset\), and \(\vee\), may be regarded as a compound problem that is a function of the problems \(z_1,\ldots,z_m\). The latter play the role of independent variables, in place of which one may substitute concrete problems \(\mathfrak A_1,\ldots,\mathfrak A_m\), obtaining as a result the problem \(U=U(\mathfrak A_1,\ldots,\mathfrak A_m)\). From the definition of the operations on problems it follows that then \(F=\varphi(\mathfrak A)\) depends on \(F_1=\varphi(\mathfrak A_1),\ldots,F_m=\varphi(\mathfrak A_m)\) and does not depend on \(X_1=\chi(\mathfrak A_1),\ldots,\ldots,X_m=\chi(\mathfrak A_m)\). Consider fixed sets \(F_1,\ldots,F_m\). To the choice of different systems of sets \(X_i\) \((X_i \subseteq F_i,\ i=1,\ldots,m)\) there will correspond different \(U(\mathfrak A_1,\ldots,\mathfrak A_m)\) with one and the same set \(F\) and different sets \(X\). If there exists an element of \(F\) belonging to all such \(X\) (i.e. the intersection of all such \(X\) is nonempty), then we shall say that the given compound problem \(U\) is solvable on the system of sets \(F_1,\ldots,F_m\). If \(U(z_1,\ldots,z_m)\) is solvable on every system of (finite) sets \(F_1,\ldots,F_m\), then we call it always solvable. This definition has a transparent meaning: the always-solvability of \(U\) means that we are able to solve any problem \(U(\mathfrak A_1,\ldots,\mathfrak A_m)\), knowing only the sets of admissible possibilities of the problems \(\mathfrak A_1,\ldots,\mathfrak A_m\).

2. The axioms of the positive calculus \(\Pi\) are the following eight formulas:

3. \(x \supset (y \supset x)\).

4. \((x \supset (y \supset z)) \supset ((x \supset y) \supset (x \supset z))\).

5. \(x \supset (y \supset (x \& y))\).

6. \((x \& y) \supset x\).

7. \((x \& y) \supset y\).

8. \(x \supset (x \vee y)\).

9. \(y \supset (x \vee y)\).

10. \((x \supset z) \supset ((y \supset z) \supset ((x \vee y)\supset z))\).

If \(\Delta\) is a finite (possibly empty) sequence of formulas and \(A\) is a formula, then the notation \(\Delta \vdash A\) means that \(A\) is derivable from \(\Delta\) and axioms 1–8 using the rule modus ponens and the substitution rule.

In what follows we shall use the term “always solvable formula,” understanding by this the always-solvability of the corresponding composite problem. A formula that is not always solvable is called refutable.

Lemma 1. If \(\Delta \vdash A\) and every formula of the sequence \(\Delta\) is always solvable, then the formula \(A\) is also always solvable.

Hence, for empty \(\Delta\), there follows

Corollary. Every derivable formula of the calculus \(\Pi\) is always solvable.

In order to describe the main points in the proof of the converse proposition, let us introduce some terms. First of all, we shall write \(\prod_{i\le n} C_i\) instead of the conjunction \(C_1 \& \ldots \& C_n\), and \(\sum_{i\le n} C_i\) instead of the disjunction \(C_1 \vee \ldots \vee C_n\), and call each formula \(C_i\) a term of the given conjunction or disjunction. If all the \(C_i\) are variables (i.e., simple letters), then the given conjunction or disjunction is called elementary. We say that a formula \(J\) is a critical implication if \(J\) has the form

\[ \left(\prod_{i\le n} \bigl((P_i \supset Q_i)\supset Q_i\bigr)\right)\supset R, \]

where the formulas \(P_i\) are elementary conjunctions, and the formulas \(Q_i\) and \(R\) are elementary disjunctions, and if, moreover, for all \(i=1,\ldots,n\) the condition is fulfilled: no term of the conjunction \(P_i\) is a term of the disjunction \(Q_i\). It is easy to prove

Lemma 2. If \(J\) is a critical implication, then \(J\) is a refutable formula.

The main difficulty is the proof of the following fact.

Lemma 3. For every formula \(A\) one of the following assertions holds: 1) \(A\) is derivable, or 2) there exists a critical implication \(J\) such that \(A\vdash J\).

From Lemmas 1, 2, and 3 there follows our main result:

Theorem 1. Every always solvable formula of the calculus \(\Pi\) is derivable.

This result admits a strengthening, leading to an algorithm of derivability for formulas of the calculus \(\Pi\). Namely, for each formula \(U\) one can effectively specify such a number \(k=k(U)\) that the derivability of \(U\) is equivalent to the solvability of \(U\) on a system of sets each consisting of \(l\ge k\) elements. We do not give here the expression for the function \(k(U)\), which can be found by analyzing the proofs of Lemmas 1, 2, and 3. Let us note only that it gives values for \(k\) that are too large for the derivability algorithm obtained on its basis to be of practical significance.

1. Let us indicate an application of Theorem 1 to the question of the completeness of \(\Pi\) as a positive calculus of mass problems \((^7)\) (in fact, it was the solution of precisely this question that suggested to the author of the present paper the idea of considering finite problems). The following theorem is obtained as a rather simple consequence of Theorem 1 if one uses the construction of operations on mass problems indicated in the author’s dissertation \((^8)\).

Theorem 2. Let a formula \(U(z_1,\ldots,z_m)\) of the calculus \(\Pi\) under substitution of arbitrary degrees of difficulty \(a_1,\ldots,a_m\) in place of \(z_1,\ldots,z_m\) give (as a result of applying to \(a_1,\ldots,a_m\) the operations indicated in \(U\)) degree of difficulty \(0\). Then \(U(z_1,\ldots,z_m)\) is derivable in \(\Pi\).

Thus \(\Pi\) also turns out to be complete as a calculus of mass problems.

1. One can introduce the operation of negation \(\neg\mathfrak A\), defined for an arbitrary finite problem \(\mathfrak A\), by putting \(\neg\mathfrak A=\mathfrak A\supset\mathfrak A_0\), where \(\mathfrak A_0\) is a fixed problem with an empty set of solutions. This permits (just as above for formulas of the calculus \(\Pi\)) the introduction of the notion of always-solvability for formulas of the calculus \(H\). It is easy to see that every

a formula derivable in the calculus \(H\) will always be solvable, but there always exist solvable formulas that are not derivable. Among the latter are, for example, the formula considered for an analogous purpose by Rose \((^5)\) (and even the formula \(((\neg D \supset D) \supset (\neg D \vee \neg D)) \supset (\neg D \vee \neg D)\), where \(D\) is any formula) and the formula \((\neg x \supset (y \vee z)) \supset ((\neg x \supset y) \vee (\neg x \supset z))\).

Thus, \(H\) is incomplete with respect to the interpretation presented.

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

Received
16 X 1961

CITED LITERATURE

\(^{1}\) A. Heyting, Sitzungsber. Preuss. Akad. Wiss., Phys.-math. Kl., S. 42 (1930).
\(^{2}\) S. Jaskowski, Actes du Congrès Intern. de Phil. Sci., 6, Phil. des math., Actualités Sci. et Ind., No. 393, Paris, 1936, p. 58.
\(^{3}\) J. C. C. McKinsey, A. Tarski, J. Symbolic Logic, 13, 1 (1948).
\(^{4}\) A. N. Kolmogoroff, Math. Zs., 35, No. 1, 58 (1932).
\(^{5}\) Gene F. Rose, Trans. Am. Math. Soc., 75, No. 1, 1 (1953).
\(^{6}\) S. C. Kleene, J. Symbolic Logic, 10, 109 (1945).
\(^{7}\) Yu. T. Medvedev, DAN, 104, No. 4, 501 (1955).
\(^{8}\) Yu. T. Medvedev, Dissertation, Moscow State University, 1955.