UDC 517.11

MATHEMATICS

V. A. YANKOV

ON THE FINITE GENERAL VALIDITY OF FORMULAS OF A SPECIAL FORM

(Presented by Academician P. S. Novikov on 22 VI 1966)

1. Yu. T. Medvedev in [1] gave a definition of the general validity of formulas of the propositional calculus on finite problems, which in the present paper is called simply finite general validity. We consider formulas of the propositional calculus that are constructed with the aid of four logical operators \((\&, \vee, \supset, \neg)\), starting not from propositional variables, but from formulas of the form \(\neg a, \neg b, \ldots\), where \(a, b, \ldots\) are propositional variables. It is proved that for this class of formulas finite general validity is equivalent to derivability in a certain calculus. At the same time an algorithm is constructed for recognizing finite general validity for such formulas, operating by means of their equivalent transformation (although, of course, there exists a trivial enumeration algorithm solving the same problem). The author knows that an analogous result has been obtained by Yu. Levin.

2. It is easy to see that the formula

\[ K \overset{\mathrm{def}}{=} (\neg a \supset b \vee c) \supset (\neg a \supset b) \vee (\neg a \supset c), \]

where \(a, b, c\) are propositional variables, is finitely generally valid. Adjoining this formula as an axiom to the intuitionistic propositional calculus (in which substitution is a rule of inference), we obtain a calculus \(I^*\), in which all derivable formulas are finitely generally valid. Derivability in this calculus will be denoted by the symbol \(\vdash_*\), and derivability in the ordinary intuitionistic calculus by the symbol \(\vdash\).

2, 1. If \(\vdash A \sim B\) (\(A\) and \(B\) are formulas), then the formulas \(A\) and \(B\) are simultaneously finitely generally valid or finitely refutable (i.e. not finitely generally valid).

3. In this and the following sections we shall fix an arbitrary nonempty set of formulas of the propositional calculus \(A_1,\ldots,A_k\). By \(\Phi(A_1,\ldots,A_k)\) we shall henceforth mean the formula

\[ \&_{i \ne l} \neg (A_i \& A_l) \& \neg \neg \left(\bigvee_{i=1}^{k} A_i\right). \]

Let \(a=(i_1,\ldots,i_l)\) be some, possibly empty, subset of the segment of the natural-number series from \(1\) to \(n\), specified by enumeration. In the case when \(a\) is empty, we assign to it \(F_a \overset{\mathrm{def}}{=} \neg(b \supset b)\), where \(b\) is some propositional variable. In the opposite case we assign to it \(F_a \overset{\mathrm{def}}{=} \neg\neg(A_{i_1} \vee \ldots \vee A_{i_l})\).

For any \(a\), we shall call the formula \(F_a\) an elementary standard formula. A nonempty set of subsets of the segment \((1,\ldots,n)\) will be called standard if none of its elements is a subset of another. To a standard set we assign correspondingly

a standard formula which is a disjunction of the elementary standard formulas assigned to the elements of the set.

3.1. From \(a \subseteq b\) it follows that \(\vdash F_a \vee F_b \sim F_b\).

3.2. \(\vdash \Phi(A_1,\ldots,A_k) \supset (F_a \& F_b \sim F_{a\cap b})\).

3.3. \(\vdash (F_a \supset F_b) \sim \neg(\neg F_a \vee \neg F_b)\)

since \(F_a\) and \(F_b\) begin with negation.

Using (3.1), we prove

3.4. If \(F\) and \(G\) are standard formulas, then \(\vdash F \vee G \sim H\), where \(H\) is some standard formula.

Using (3.1) and (3.2) (as well as the distributive laws), we prove:

3.5. If \(F\) and \(G\) are standard formulas, then
\[ \vdash \Phi(A_1,\ldots,A_k) \supset (F \& G \sim H), \]
where \(H\) is some standard formula.

3.6. If \(F\) is a standard formula, then
\[ \vdash \Phi(A_1,\ldots,A_k) \supset (\neg F \sim F_a), \]
where \(a\) is the subset of the segment \((1,\ldots,n)\) obtained by discarding from \((1,\ldots,n)\) all numbers occurring in some element of the set to which \(F\) has been assigned.

1. Let us now consider a formula of the form
   \[ F_a \supset F_{a_1} \vee \cdots \vee F_{a_l} \]
   (where \(a,a_1,\ldots,a_l\) are certain subsets of \((1,\ldots,n)\)). Since \(F_{a_l}\) begins with negation, we have
   \[ \vdash (F_a \supset F_{a_1} \vee \cdots \vee F_{a_l}) \sim \bigvee_{i=1}^{l}(F_a \supset F_{a_i}), \]
   and by virtue of (3.3), (3.6), and (3.4) this means that the following holds:

4.1.
\[ \vdash \Phi(A_1,\ldots,A_k) \supset \bigl((F_a \supset F_{a_1}\vee \cdots \vee F_{a_k}) \sim G\bigr), \]
where \(G\) is some standard formula.

Finally, let \(F\) and \(G\) be standard formulas, namely
\[ F \stackrel{\circ}{=} F_{a_1}\vee \cdots \vee F_{a_l}. \]
Then
\[ \vdash (F \supset G) \sim (F_{a_1}\supset G)\& \cdots \& (F_{a_l}\supset G). \]

By virtue of (4.1) and (3.5) we obtain from this:

4.2. If \(F\) and \(G\) are some standard formulas, then
\[ \vdash \Phi(A_1,\ldots,A_k) \supset ((F \supset G)\sim H), \]
where \(H\) is some standard formula.

1. Let \(F\) now be the formula of the special form under investigation, and let \(a_1,\ldots,a_n\) be all its propositional variables. Consider formulas of the form
   \[ \alpha_1 \& \cdots \& \alpha_n, \]
   where each \(\alpha_i\) (\(1\le i\le n\)) is either \(a_i\) or \(\neg a_i\). There will be exactly \(2^n\) such formulas. Number them in some way. These formulas
   \[ A_1,\ldots,A_{2^n} \]
   will play for us the role of \(A_1,\ldots,A_k\) in the two preceding points.

First of all, note that the following holds:

5.1. \(\vdash \Phi(A_1,\ldots,A_{2^n})\).

In addition, the following holds:

5.2.
\[ \vdash \neg a_i \sim \neg\neg\left(\bigvee_{\neg a_i\in A_j} A_j\right), \]
where the disjunction contains those \(A_j\) whose conjunctive term is \(\neg a_i\).

1. By induction on the number of logical operators in \(F\) (apart from the initial negations of propositional variables), we prove the following lemma:

6.1. Every subformula of the formula \(F\) (except for the subformulas \(a_1,\ldots,a_n\)) is equivalent in \(I^*\) to some standard formula in \(A_1,\ldots,A_{2^n}\).

As the basis we use (5.2). In the induction step we use (3.4) in the case of disjunction; (3.5) and (5.1) in the case of conjunction; (3.6), (5.1) in the case of negation; and (4.2), (5.1) in the case of implication.

1. The desired algorithm works as follows. We replace in \(F\) all subformulas of the form \(\neg a_i\) by the equivalents according to (5.2), and then, using lemma (6.1), by transformations equivalent in \(I^*\), we reduce \(F\) to \(G\), some standard formula in \(A_1,\ldots,A_{2^n}\).

Consider two cases:

A. \(G\) is an elementary standard formula corresponding to a subset of \((1,\ldots,2^n)\). Then \(G\) is \(\neg\neg\displaystyle\bigvee_{i=1}^{2^n} A_i\), and therefore \(\vdash G\), i.e. \(G\) is finitely valid, and by virtue of (2.1) so is \(F\).

B. The opposite case. We shall prove that in this case \(G\) (and hence also \(F\)) is finitely refutable.

Indeed, if \(a\) is a proper subset of \((1,\ldots,2^n)\), then \(F_a\) is classically equivalent to the disjunctive normal form of some non-valid function of \(a_1,\ldots,a_n\). Therefore \(F_a\) is classically refutable, and hence finitely refutable. And since \(G\) is a disjunction of finitely refutable elementary standard formulas, \(G\) is finitely refutable in view of their finite refutability (see (1)).

1. We have proved the following theorem.

Theorem. A formula of the propositional calculus of our special form is finitely valid if and only if it is derivable in \(I^*\).

\(I^*\), however, does not contain all finitely valid formulas. Indeed, the formula

\[ \mathfrak{B} \equiv ((\neg\neg a \supset a)\supset a\vee \neg a)\supset \neg\neg a\vee \neg a, \]

where \(a\) is a propositional variable, is finitely valid but is not derivable in \(I^*\) (the latter follows from the fact that \(K\) is valid on the implicative structure \(\Gamma(\Gamma(J_0)\times J_0)\) (see (2)), while \(\mathfrak{B}\) is refutable on it).

Moscow Institute of Physics and Technology

Received
9 VI 1966

CITED LITERATURE

\(^{1}\) Yu. T. Medvedev, DAN, 142, No. 5, 1015 (1962).
\(^{2}\) V. A. Yankov, DAN, 151, No. 5, 1035 (1963).