UDC 517.12

MATHEMATICS

L. A. LEVIN

SOME SYNTACTIC THEOREMS ON THE CALCULUS OF FINITE PROBLEMS OF Yu. T. MEDVEDEV

(Presented by Academician A. N. Kolmogorov, 5 VII 1968)

In the well-known work of A. N. Kolmogorov (^1) an interpretation was given of intuitionistic logic (^2) as a calculus of problems. Subsequently this idea was refined from various points of view (see, for example, (^3–5)). Another refinement of this interpretation of A. N. Kolmogorov is indicated in the work (^6), later continued in (^7, ^8). In the present paper we give certain results concerning the logic of finite problems constructed in (^6). Familiarity with the concepts and terminology of the paper (^6) will be assumed. We show (Theorem 2) that the logic of finite problems is, in a certain sense, complete. In addition, a syntactic description of this logic will be given (Theorem 4), and a calculus will be constructed (containing, however, a certain additional infinitary rule of inference D) whose class of derivable formulas coincides with the class of finitely generally valid formulas (Corollary 1).

We first give five definitions.

Definition 1. By a logic we shall mean any class of formulas of the propositional calculus that contains all axioms of the intuitionistic propositional calculus and is closed under the application of the rules modus ponens and substitution.

Definition 2. By an $\alpha$-logic we mean any logic containing the formula

\[ \alpha = (\neg x \supset (y \vee z)) \supset ((\neg x \supset y) \vee (\neg x \supset z)). \]

Definition 3. A weakly constructive logic is any logic that contains no formula of the form of a disjunction of some number of classically underivable formulas.

Definition 4. We define, for formulas of the propositional calculus, the concept of rank in the following inductive manner: a) every formula of the form $\neg \varphi$ has rank 1; b) if $\psi$ has rank 1 and $\varphi$ is an arbitrary formula, then the formula $\varphi \supset \psi$ has rank 1; c) if $\varphi$ is a formula of rank $k$, and $\psi$ is of rank $l$, then $\varphi \vee \psi$ is a formula of rank $k + l$, $\varphi \& \psi$ is of rank $k \cdot l$, and $\varphi \supset \psi$ is of rank $l^k$; d) the rank of all remaining formulas is infinite.

Definition 5. A logic is called finite if, for every formula $\varphi(x_1, x_2, \ldots, x_n)$ not belonging to it, there exist formulas $\psi_1, \ldots, \psi_n$ of finite rank such that the formula $\varphi(\psi_1, \psi_2, \ldots, \psi_n)$ also does not belong to this logic.

Theorem 1. The class of finitely generally valid formulas (i.e., formulas always solvable in the sense of the work (^6)) is a weakly constructive finite $\alpha$-logic.

Theorem 2. The class of finitely generally valid formulas is the greatest weakly constructive $\alpha$-logic.

Theorem 3. The class of finitely generally valid formulas is the least finite $\alpha$-logic.

Corollary 1. Let $U$ be a calculus containing the axioms and rules of inference of the intuitionistic propositional calculus, with the formula $\alpha$ added as an axiom, and also the following rule of inference:

D. If $\varphi(x_1, \ldots, x_n)$ is such a formula that, for any formulas $\psi_1, \ldots, \psi_n$ of finite rank, $\vdash \varphi(\psi_1, \ldots, \psi_n)$, then $\vdash \varphi(x_1, \ldots, x_n)$.

The class of derivable formulas of the calculi \(U\) coincides with the class of finitely generally valid formulas.

Theorem 4. The class of finitely generally valid formulas is the unique weakly constructive finite \(\alpha\)-logic.

This theorem follows trivially from Theorems 2 and 3.

We shall now formulate Lemmas 1–6, needed for the proof of Theorems 2 and 3. Each of these lemmas follows easily from the preceding ones.

Lemma 1. For any formula \(\varphi\) of finite rank there exists a formula \(\psi\) of the form
\[ \psi=\neg\psi_1\vee\neg\psi_2\ldots\vee\neg\psi_k \]
such that the formula \((\varphi\sim\psi)\) belongs to every \(\alpha\)-logic.

The proof is carried out by induction, using the definition of the rank of a formula.

Lemma 2. Every logic contains all classically provable formulas of the form \(\neg\psi\).

This lemma is a direct consequence of the well-known theorem of V. I. Glivenko \((^9)\) on the intuitionistic derivability of classically derivable formulas having the form of negations.

Lemma 3. Every logic contains a formula of the form \(\neg\psi_1\vee\ldots\vee\neg\psi_k\), if for some \(i\), \(1\le i\le k\), the formula \(\neg\psi_i\) is classically derivable.

Lemma 4. Every weakly constructive logic contains the formula \(\neg\psi_1\vee\ldots\vee\neg\psi_k\) if and only if, for some \(i\), \(1\le i\le k\), the formula \(\neg\psi_i\) is classically derivable.

Lemma 5. Every \(\alpha\)-logic contains all finitely generally valid formulas of finite rank.

This follows from Lemmas 1 and 3.

Lemma 6. Every weakly constructive \(\alpha\)-logic contains a formula \(\psi\) of finite rank if and only if \(\psi\) is finitely generally valid.

This follows from Lemmas 1 and 4.

Let us prove Theorems 2 and 3 with the aid of these lemmas.

Proof of Theorem 2. Let \(\varphi(x_1,\ldots,x_n)\) be refutable. Then there also exist formulas \(\psi_1,\ldots,\psi_n\) of finite ranks such that the formula \(\varphi(\psi_1,\ldots,\psi_n)\) is refutable (by virtue of Definition 5 and Theorem 1). But then, by Lemma 6, the formula \(\varphi(\psi_1,\ldots,\psi_n)\) belongs to no weakly constructive \(\alpha\)-logic. Hence the formula \(\varphi(x_1,\ldots,x_n)\) has the same property, as was required.

Proof of Theorem 3. Let \(\varphi(x_1,\ldots,x_n)\) not belong to some finite \(\alpha\)-logic. Then there exist formulas \(\psi_1,\ldots,\psi_n\) of finite rank such that the formula \(\varphi(\psi_1,\ldots,\psi_n)\) (of finite rank) also does not belong to this logic. Then \(\varphi(\psi_1,\ldots,\psi_n)\) is refutable (by Lemma 5). But then \(\varphi(x_1,\ldots,x_n)\) is also refutable, as was required.

Results close to those presented here were also obtained independently by V. A. Yankov.

The present work was carried out in 1965 under the influence of lectures on mathematical logic delivered in the physics-and-mathematics boarding school at Moscow University by A. N. Kolmogorov, to whom the author takes this opportunity to express gratitude for drawing attention to the topic considered.

The author also expresses gratitude to Yu. T. Medvedev and A. B. Sosinsky for their help in writing the article.

Moscow State University
named after M. V. Lomonosov

Received
5 VI 1968

CITED LITERATURE

1. A. N. Kolmogoroff, Math. Zs., 35, No. 1, 58 (1932).
2. A. Heyting, Sitzungsber. Preuss. Akad. Wiss., Phys.-math. Kl., S. 42 (1930).
3. S. C. Kleene, J. Symbolic Logic, 10, 109 (1945).
4. Gene F. Rose, Trans. Am. Math. Soc., 75, No. 1, 1 (1953).
5. H. A. Shanin, Tr. Matem. inst. im. V. A. Steklova AN SSSR, 52, 226 (1958).
6. Yu. T. Medvedev, DAN, 142, No. 5, 1015 (1962).
7. Yu. T. Medvedev, DAN, 148, No. 4, 771 (1963).
8. Yu. T. Medvedev, DAN, 169, No. 1, 20 (1966).
9. V. I. Glivenko, Bull. Sci. Acad. Roy. Belg., 15, 183 (1929).