UDC 517.12

MATHEMATICS

Yu. T. MEDVEDEV

ON THE INTERPRETATION OF LOGICAL FORMULAS BY MEANS OF FINITARY PROBLEMS

(Presented by Academician P. S. Novikov on 18 X 1965)

The present paper is a continuation of the works (¹, ²). Logical formulas that are generally valid in the sense of those works (always-solvable formulas) will henceforth be called finitely generally valid formulas. In the first section a description of finitely generally valid formulas is given in algebraic terms (Theorems 1 and 2). In the second section a new operation on finitary problems is introduced—a weak disjunction. The third section is devoted to extending the concept of finite general validity to a class of formulas of the narrow predicate calculus.

1. Let \(n \geqslant 1\) be a natural number. By \(I_n\) we denote the set of all natural \(i\) such that \(1 \leqslant i \leqslant n\), and by \(\sigma^n\) the family of all nonempty subsets of the set \(I_n\), so that the condition \(E \in \sigma^n\) is equivalent to the two conditions: \(E \subseteq I_n\) and \(E \ne \Lambda\), where \(\Lambda\) is the empty set.

Definition 1. Let \(\sigma \subseteq \sigma^n\). The closure of the family \(\sigma\) with respect to \(\sigma^n\) is the family \(\sigma^* \subseteq \sigma^n\) for which \(E \in \sigma^*\) if and only if \(E_0 \subseteq E \subseteq I_n\) for at least one \(E_0 \in \sigma\).

The operation of closure with respect to \(\sigma^n\) thus introduced is defined for every family \(\sigma \subseteq \sigma^n\) and has the following properties: 1) \(\lambda^* = \lambda\) for the empty family \(\lambda\); 2) \(\sigma^* \supseteq \sigma\); 3) \(\sigma^{**} = \sigma^*\); 4) \((\sigma_1 \cup \sigma_2)^* = \sigma_1^* \cup \sigma_2^*\). This operation, considered together with the set-theoretic operations of union, intersection, and complementation relative to \(\sigma^n\), turns the set of all \(\sigma \subseteq \sigma^n\) into a Boolean algebra with closure in the sense of McKinsey and Tarski (³), which we shall denote by \(\Sigma^n\).

Let \(\Phi^n\) be the set of all closed \(\sigma \in \Sigma^n\). Define on \(\Phi^n\) the following operations (it is convenient to use logical connectives as symbols for these operations):
\[ \sigma_1 \& \sigma_2 = \sigma_1 \cup \sigma_2,\qquad \sigma_1 \vee \sigma_2 = \sigma_1 \cap \sigma_2,\qquad \neg \sigma_1 = (\overline{\sigma_1})^*, \]
\[ \sigma_1 \supset \sigma_2 = (\overline{\sigma_1} \cap \sigma_2)^*, \]
where the bar above denotes complementation relative to \(\sigma^n\). These operations turn the set \(\Phi^n\) into a certain Brouwer algebra (⁴, ⁵), which for simplicity we shall denote by the same symbol \(\Phi^n\). The element \(\sigma_1 \supset \sigma_2\) may be defined as the least element \(\sigma \in \Phi^n\) for which \(\sigma_1 \& \sigma \geqslant \sigma_2\). The element \(\neg \sigma\) is nothing other than \(\sigma \supset \sigma^n\). The least element of the algebras \(\Sigma^n\) and \(\Phi^n\) (corresponding to the empty family \(\lambda\)) will be denoted by the symbol \(0\).

Definition 2. An ordered system \(S\) of finitary problems \(\mathfrak A_1,\ldots,\mathfrak A_n\) \((n \geqslant 1)\) is called reduced if all problems of this system have one and the same set of admissible possibilities:
\[ \varphi(\mathfrak A_1)=\cdots=\varphi(\mathfrak A_n). \]
The number \(n\) is called the order of \(S\).

Definition 3. Let \(S\) be a reduced system of finitary problems whose order is equal to \(n\). Let \(F\) be the set of admissible possibilities, and let \(X_1,\ldots,X_n\) be the corresponding sets of solutions. The characteristic of the system \(S\) is the family \(\sigma(S)\) of sets defined by the following conditions: 1) \(\sigma(S) \subseteq \sigma^n\); 2) if \(E \in \sigma^n\), then \(E \in \sigma(S)\) if and only if the intersection of all those \(X_i\) for which \(i \in E\) is the empty set.

Lemma 1. In order that a family \(\sigma \subseteq \sigma^n\) be the characteristic of some reduced system \(S\) of problems having order \(n\), it is necessary and sufficient that \(\sigma\) be a closed element of the algebra \(\Sigma^n\).

Definition 4. Let \(\sigma_1, \sigma_2 \subseteq \sigma^n\). We say that the family \(\sigma_1\) is a basis of the family \(\sigma_2\) if every element of \(\sigma_2\) contains some element of \(\sigma_1\).

Obviously, the property of the family \(\sigma_1\) to serve as a basis of the family \(\sigma_2\) is equivalent to the relation \(\sigma_1^* \geq \sigma_2\) in the algebra \(\Sigma^n\).

Definition 5. Let \(S_1=\{\mathfrak A_i\}\) and \(S_2=\{\mathfrak B_i\}\) be two reduced systems of problems of one and the same order \(n\). We introduce logical operations over \(S_1\) and \(S_2\), giving new systems of order \(n\), by means of the conventions:
\[ S_1 \& S_2=\{\mathfrak A_i \& \mathfrak B_i\},\qquad S_1 \vee S_2=\{\mathfrak A_i \vee \mathfrak B_i\},\qquad \neg S_1=\{\neg \mathfrak A_i\}, \]
\[ S_1 \supset S_2=\{\mathfrak A_i \supset \mathfrak B_i\}. \]

It turns out that the characteristics of the new systems are completely determined by the characteristics of the systems \(S_1\) and \(S_2\). Moreover, the following holds.

Lemma 2. Let \(S_1\) and \(S_2\) be two reduced systems of problems of one and the same order \(n\), and let \(\sigma_1\) and \(\sigma_2\), respectively, be bases of their characteristics. Then for the system \(S\) obtained as the result of one of the logical operations over \(S_1\) and \(S_2\), a basis \(\sigma\) of the characteristic can be defined as follows:
1) \(S=S_1 \& S_2:\ \sigma=\sigma_1 \& \sigma_2\);
2) \(S=S_1 \vee S_2:\ E\in\sigma\) if and only if \(E=E_1\cup E_2\) for some \(E_1\in\sigma_1\) and \(E_2\in\sigma_2\);
3) \(S=\neg S_1:\ \sigma=\bar{\sigma}_1\);
4) \(S=S_1 \supset S_2:\ E\in\sigma\) if and only if \(E\in\sigma_2\) and there does not exist such an \(E_1\in\sigma_1\) that \(E_1\subseteq E\).

From this lemma it is easy to derive the following assertion.

Lemma 3. For reduced systems \(S_1\) and \(S_2\) of one and the same order \(n\), the relations
\[ \sigma(S_1 \& S_2)=\sigma(S_1)\&\sigma(S_2),\qquad \sigma(S_1\vee S_2)=\sigma(S_1)\vee\sigma(S_2), \]
\[ \sigma(\neg S_1)=\neg\sigma(S_1),\qquad \sigma(S_1\supset S_2)=\sigma(S_1)\supset\sigma(S_2), \]
hold, where the operations on the right-hand side are understood in the sense of the algebra \(\Phi^n\).

Let \(U(z_1,\ldots,z_m)\) be a logical formula containing no logical connectives except \(\&,\vee,\neg,\supset\), and let \(F_1,\ldots,F_m\) be nonempty finite sets. Consider a sequence \(X_k^i\) of sets \((k=1,\ldots,m;\ i=1,\ldots,n)\), for which \(X_k^i\subseteq F_k\). Denote by \(\mathfrak A_k^i\) the finite problem for which
\[ \varphi(\mathfrak A_k^i)=F_k,\qquad \chi(\mathfrak A_k^i)=X_k^i. \]
For fixed \(k\) we have a reduced system \(S_k\) of order \(n\) of problems \(\mathfrak A_k^i\) \((i=1,\ldots,n)\). Let
\[ S=U(S_1,\ldots,S_m) \]
be the reduced system obtained by applying to \(S_1,\ldots,S_m\) the logical operations indicated in the formula \(U\). Suppose that the formula \(U\) is refutable on some system of sets \(F_1,\ldots,F_m\). From the definition of refutability it follows that, for some tuple \(S_1,\ldots,S_m\) of the described form, the system \(S\) has as its characteristic a nonempty family
\[ \sigma(S)\subseteq\sigma^n. \]
By Lemma 3, we have
\[ \sigma(S)=U(\sigma(S_1),\ldots,\sigma(S_m)), \]
where the operations on the right-hand side are understood in the sense of the algebra \(\Phi^n\). Consequently, \(U\), as a function on \(\Phi^n\), is not identically equal to \(0\). Conversely, suppose
\[ U(\sigma_1,\ldots,\sigma_m)=0 \]
in the algebra \(\Phi^n\). Then, with the aid of Lemma 1, it is easy to establish the refutability of \(U\) on some system of sets \(F_1,\ldots,F_m\). We arrive at the following result.

Theorem 1. In order that a formula \(U\) be finitely universally valid, it is necessary and sufficient that \(U\) be identically equal to \(0\) on the Brouwer algebra \(\Phi^n\) for every \(n\geq 1\).

This theorem can be given a somewhat different form. Every finite distributive structure \(L\) can be regarded as a Brouwer algebra if, for each pair \(a,b\in L\), one sets by definition \(a\& b\) equal to the upper bound of \(a\) and \(b\), \(a\vee b\) equal to the lower bound of \(a\) and \(b\), \(a\supset b\) equal to the least \(c\in L\) for which \(a\& c\geq b\) (such a \(c\) exists by virtue of the finiteness and distributivity of \(L\)), and
\[ \neg a=a\supset e, \]
where \(e\) is the greatest element of \(L\). Denote by \(L_n\) the free distributive structure with \(n\) generators \(x_1,\ldots,x_n\) and with an adjoined symbol of the least element \(0\). It is easy to see that \(L_n\), considered as a Brouwer algebra, is isomorphic to \(\Phi^n\). Therefore the following variant of Theorem 1 is valid.

Theorem 2. The class of finitely universally valid formulas coincides with the class of formulas that identically turn into \(0\) on \(L_n\) for every natural \(n\).

It is interesting to compare this result with the well-known fact that, for intuitionistic derivability of a formula, it is necessary and sufficient that this formula identically turn into \(0\) on every finite distributive structure. Let us also note that the structure \(L_n\) is isomorphic to the structure of monotone functions of \(n\) variables of the (two-valued) algebra of logic.

The most convenient way of establishing the refutability of formulas is connected with Lemma 2. In this lemma four (corresponding to the logical connectives) very simple operations are indicated on the bases of characteristics of systems of order \(n\). Since every \(\sigma \subseteq \sigma^n\) is the base of the characteristic (namely, \(\sigma^*\)) of some system of order \(n\), these operations are defined for all such \(\sigma\). Thus we have a certain algebra \(B^n\). The element of \(B^n\) corresponding to the empty family we shall denote by \(0\). It follows from Lemma 2 that a formula \(U\) identically turns into \(0\) on \(\Phi^n\) if and only if \(U\) identically turns into \(0\) on \(B^n\).

1. According to A. N. Kolmogorov \((^6)\), the theory of the constructive solution of problems contains propositional logic. Naturally, the language of this theory must also contain more expressive means. The necessity of extending the logical language arises, for example, in the following situation. Let \(A\) and \(B\) be problems in the sense of A. N. Kolmogorov. It may happen that we have managed to find some object \(a\) that has a relation to the solution of problem \(A\), and an object \(b\) that has a relation to the solution of problem \(B\), and at the same time to establish that the statement “\(a\) is not a solution of \(A\) and \(b\) is not a solution of \(B\)” is false. To express this situation it is convenient to regard the pair \((a,b)\) as serving as a solution of the weak disjunction \(A \sqcup B\) of the problems \(A\) and \(B\).

In the case of finitary problems, what has been said can be given an exact meaning. Let \(\mathfrak A_1\) and \(\mathfrak A_2\) be finitary problems, with
\(\varphi(\mathfrak A_1)=F_1,\ \varphi(\mathfrak A_2)=F_2,\ \chi(\mathfrak A_1)=X_1,\ \chi(\mathfrak A_2)=X_2\).
Define a problem \(\mathfrak A\), which we shall call the weak disjunction of the problems \(\mathfrak A_1\) and \(\mathfrak A_2\) and denote by \(\mathfrak A_1 \sqcup \mathfrak A_2\), by the agreements:
\(F=\varphi(\mathfrak A)=F_1 \times F_2,\ \chi(\mathfrak A)=X\), where \(x=(f_1,f_2)\in F\) belongs to \(X\) if and only if it is not true that \(f_1\in X_1\) and \(f_2\in X_2\). The concept of finite universal validity extends in the obvious way to the case of formulas containing the new connective \(\sqcup\). In particular, the formula
\(((x \sim u)\ \&\ (y \sim v)) \supset ((x \sqcup y)\sim(u\sqcup v))\) turns out to be finitely universally valid (\(a\sim b\) denotes the conjunction \((a\supset b)\ \&\ (b\supset a)\)). This shows the “correctness” of the operation of weak disjunction. Here are some other examples of finitely universally valid formulas:
\(x\supset(x\sqcup y),\ y\supset(x\sqcup y),\ ((x\vee y)\sqcup z)\supset((x\sqcup z)\vee(y\sqcup z)),\)
\((\neg x)\sqcup(\neg\neg x)\).

The operation of weak disjunction can also be defined in a correct way for mass problems in the sense of the works \((^7,^8)\).

1. We extend the concept of finite universal validity to the class of formulas of the narrow predicate calculus. Under the usual interpretation of such formulas in the case of a finite domain \(D\), containing \(k\geq 1\) individuals, universal quantifiers are considered as \(k\)-term conjunctions, existential quantifiers as \(k\)-term disjunctions. It then turns out that every closed formula \(W\) is content-equivalent to a certain formula \(U\) of the propositional calculus (the variables of the formula \(U\) are the predicate symbols from \(W\), supplied with indices—the elements of \(D\)). Taking \(D\) to be the set of natural numbers \(1,2,\ldots,k\), we shall denote the operation of passing from \(W\) to \(U\) by the symbol \(\Gamma_k\), so that \(U=\Gamma_k(W)\). A formal description of the operation \(\Gamma_k\) can be found, for example, in \((^9)\).

Definition 6. A closed formula \(W\) of the narrow predicate calculus is called finitely universally valid if for all \(k\geq 1\)

the formula \(\Gamma_k(W)\) of the propositional calculus is finitely universally valid.

Theorem 3. If a closed formula \(W\) of the restricted predicate calculus is derivable in the intuitionistic predicate calculus, then \(W\) is finitely universally valid.

As a nontrivial example of finitely universally valid formulas not derivable intuitionistically, we indicate the distributive law for the universal quantifier:
\[ (x)(A(x)\vee B)\supset ((x)A(x)\vee B), \]
where \(A(x)\) and \(B\) are closed formulas.

Theorem 4. There is no algorithm recognizing finite universal validity of closed formulas of the restricted predicate calculus.

This result is obtained with the aid of the following theorem, which is also of independent interest:

Theorem 5. In order that a formula of the propositional calculus of the form \(\neg U\) be finitely universally valid, it is necessary and sufficient that it be classically true (i.e., derivable in the classical propositional calculus).

Theorem 4 is now obtained as follows. By Theorem 5, the finite universal validity of the closed formula \(\neg\neg W\) of the restricted predicate calculus is equivalent to the fact that, for every \(k\geqslant 1\), the formula
\[ \Gamma_k(\neg\neg W)=\neg\neg \Gamma_k(W) \]
is classically true, i.e., the formula \(\Gamma_k(W)\) is classically true for every \(k\). The latter is equivalent to saying that \(W\) belongs to the class \(\Omega\) of closed formulas classically identically true in every finite domain. If there existed an algorithm recognizing finite universal validity, then there would thereby also exist an algorithm recognizing membership of formulas in the class \(\Omega\). However, B. A. Trakhtenbrot proved that such an algorithm is impossible \({}^{(10)}\).

Let us note in conclusion that the notion of finite universal validity extends in an obvious way to the class of formulas containing, besides the usual connectives \(&,\vee,\neg,\supset\), universal quantifiers \((x)\) and existential quantifiers \((Ex)\), also the connective \(\sqcup\) and the corresponding “weak existential quantifier” \([x]\).

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

Received
14 X 1965

REFERENCES

1. Yu. T. Medvedev, DAN, 142, No. 5, 1015 (1962).
2. Yu. T. Medvedev, DAN, 148, No. 4, 771 (1963).
3. J. C. C. McKinsey, A. Tarski, Ann. Math., 45, No. 1, 141 (1944).
4. G. Birkhoff, Lattice Theory, N. Y., 1952.
5. J. C. C. McKinsey, A. Tarski, Ann. Math., 47, No. 1, 122 (1946).
6. A. N. Kolmogoroff, Math. Zs., 35, No. 1, 58 (1932).
7. Yu. T. Medvedev, DAN, 104, No. 4, 501 (1955).
8. Yu. T. Medvedev, Dissertation, Moscow State University, 1955.
9. S. C. Kleene, Introduction to Metamathematics, N. Y.—Toronto, 1952.
10. B. A. Trakhtenbrot, DAN, 70, No. 4, 569 (1950).