UDC 51.01.164

MATHEMATICS

F. A. KABAKOV

ON MODELING BY REALIZABILITY OF PSEUDO-BOOLEAN ALGEBRAS

(Presented by Academician P. S. Novikov on 30 X 1969)

In the study of questions of realizability of propositional formulas, it is sometimes necessary (see, for example, ((^{1,2}))) to construct systems of arithmetical formulas that stand in a relation to certain pseudo-Boolean algebras which, in a definite sense, may be called a modeling relation. In the present note some properties of one kind of such modeling are established.

We consider propositional formulas constructed in the usual way from the propositional connectives (\&,\ \vee,\ \supset) and (\neg), propositional variables (p_1,p_2,\ldots), and parentheses ((,\ )). By an arithmetical example of a propositional formula (\mathfrak A) we mean any arithmetical formula obtained as the result of substituting closed arithmetical formulas in (\mathfrak A) in place of the propositional variables (under the condition that in place of all occurrences in (\mathfrak A) of one and the same propositional variable one and the same arithmetical formula is substituted). By arithmetical formulas we shall mean formulas of the language of the logico-arithmetical calculus from ((^3)), and by intuitionistic arithmetic we shall understand the intuitionistic variant (S) of this calculus. To this same book of Kleene’s we refer the reader for all necessary information from realizability theory, including D. Nelson’s theorem on the realizability of formulas derivable in (S).

A propositional formula (\mathfrak A(p_1,\ldots,p_n)) is called realizable if there exists an algorithm that transforms every (n)-term sequence (F_1,\ldots,F_n) of closed arithmetical formulas into a realization, in Kleene’s sense, of the arithmetical formula (\mathfrak A(F_1,\ldots,F_n)). For abbreviated notation of the judgments “the number (e) realizes the formula (F),” “the formula (F) is realizable,” and “the formula (F) is derivable in intuitionistic arithmetic,” we use respectively the expressions (e r F), (rF), and (\vdash F). In addition, for abbreviated notation of meaningful judgments we shall use (without danger of misunderstanding) the symbols of logical operations belonging to the language (S), in their usual meaningful sense. If (F_1) and (F_2) are formulas, then (F_1 \equiv F_2) denotes the formula ((F_1 \supset F_2)\ \&\ (F_2 \supset F_1)).

Let (A=\langle {a_1,\ldots,a_m}, <A\rangle) be a finite pseudo-Boolean algebra with elements (a_1,\ldots,a_m), partial-order relation (<_A), greatest element (\mathcal V_A), and with the operations (\&_A,\ \vee_A,\ \supset_A,\ \neg_A) defined in the usual way. A propositional formula (\mathfrak A(p_1,\ldots,p_n)) is called identically true on the algebra (A) if, upon replacing in (\mathfrak A) the connectives (\&,\ \vee,\ \supset), and (\neg) respectively by the operations (\&_A,\ \vee_A,\ \supset_A), and (\neg_A), and under any substitution of elements of the algebra (A) for the propositional variables (when one and the same element of the algebra is substituted in place of all occurrences of one and the same propositional variable), the value of the expression (\mathfrak A_A(a)) thus obtained, computed in accordance with the definition of the operations (\&},\ldots,a_{i_nA,\ \vee_A,\ \supset_A), and (\neg_A), is equal to (\mathcal V_A). If, however, there exists such an assignment of values of the propositional variables: (p_1=a) <_A \mathcal V_A), then the formula (\mathfrak A) is called refutable on the algebra (A). The set},\ldots,p_n=a_{i_n}), for which (\mathfrak A_A(a_{i_1},\ldots,a_{i_n

(\mathscr L(A)) of all propositional formulas designated on a given finite pseudo-Boolean algebra (called the finite logic determined by the algebra (A)), is, as is known, an intermediate logic, i.e., it consists of classically true formulas, contains all the axioms of Heyting’s intuitionistic propositional calculus (H), and is closed under the rules of inference: modus ponens and the rule of substitution (see, for example, ((^4))). A sequence (A_1, A_2, \ldots) of finite pseudo-Boolean algebras is called characteristic for the set (I) of all formulas derivable in Heyting’s intuitionistic propositional calculus if

[
I=\prod_n \mathscr L(A_n).
]

It is known that such sequences for (I) exist (see, for example, ((^1))).

Basic definition.

I. We shall say that a system of arithmetical formulas (F_1(x), \ldots, F_m(x)) (with the single free variable (x)) models by realizability the finite pseudo-Boolean algebra

[
A=\langle {a_1,\ldots,a_m}, <_A\rangle,
]

if:

1) (rF_i(x)) if and only if (a_i=\mathcal U_A);

2) (r[F_i(x)\oplus F_j(x)\equiv F_k(x)]) and (r[\neg F_s(x)\equiv F_t(x)]) every time that (a_i\oplus_A a_j=a_k) and (\neg_A a_s=a_t), where each of the symbols (\&, \vee, \supset).

II. A pseudo-Boolean algebra is called modeled by realizability if there exists a system of arithmetical formulas modeling this algebra by realizability.

The following proofs are constructive in character. The principle of constructive selection (see ((^5))) is assumed.

Lemma 1. If a system of arithmetical formulas (F_1(x),\ldots,F_m(x)) models by realizability the finite pseudo-Boolean algebra

[
A=\langle {a_1,\ldots,a_m}, <_A\rangle,
]

then for every propositional formula (\mathfrak A(p_1,\ldots,p_n)) from (\mathfrak A_A(a_{i_1},\ldots,a_{i_n})=a_s) it follows that

[
r[\mathfrak A(F_{i_1}(x),\ldots,F_{i_n}(x))\equiv F_s(x)].
]

Proof. Of course, the construction of a realization of the formula

[
\mathfrak A(F_{i_1}(x),\ldots,F_{i_n}(x))\equiv F_s(x)
]

(since realizations of formulas from condition 2) in the basic definition are given) may turn out to be technically cumbersome; however, the principled possibility of such a construction is easily traced by induction on the logical length of the formula (\mathfrak A).

Lemma 2. If an arithmetical formula (F(x)) with one free variable (x) is not realizable, then there cannot fail to exist such a natural number (k) for which the formula (F(k)) is not derivable in intuitionistic arithmetic.

Proof. Let (\neg rF(x)). Suppose that (\neg \exists k\, \neg\vdash F(k)). Then (\forall k\, \neg\neg\vdash F(k)). Hence, contrary to the condition, it follows that (rF(x)). Indeed, the principled possibility of constructing a partially recursive function (\varphi) such that (\forall k\,\varphi(k)\, rF(k)) is clear from the following reasoning. Let (k) be a natural number. With the help of a suitable algorithm we shall construct, one after another, all derivations in (S) until some derivation of the formula (F(k)) is constructed for the first time. Accepting the principle of constructive selection, we believe that this will occur, since the concept “to be a derivation in (S)” is decidable and, according to the supposition made, (\neg\neg\vdash F(k)). Having a derivation of the formula (F(k)) in (S), we shall construct its realization by reproducing, as applied to this derivation, D. Nelson’s proof of the realizability of formulas derivable in (S).

Theorem 1. If a propositional formula is refutable on some finite pseudo-Boolean algebra modeled by realizability, then it is not true that there do not exist arithmetical examples of this formula which are underivable in intuitionistic arithmetic.

Proof. Let the propositional formula (\mathfrak A(p_1,\ldots,) (\ldots,p_n)) be refutable on a finite pseudo-Boolean algebra

[
A=\langle {a_1,\ldots,\ldots,a_m}, <_A\rangle,
]

modeled by realizability by the system of formulas (F_1(x),\ldots)

..., (F_m(x)). For certain (i_1,\ldots,i_n) and (s) we then have
[
\mathfrak A_A(\alpha_{i_1},\ldots,\alpha_{i_n})=\alpha_s <A \mathcal U_A.
]
By Lemma 1,
[
r\bigl[\mathfrak A(F(x)) \equiv F_s(x)\bigr].}(x),\ldots,F_{i_n
]
From (\alpha_s \ne \mathcal U_A) it follows that (\neg rF_s(x)), and therefore we have
[
\neg r\mathfrak A(F_{i_1}(x),\ldots,F_{i_n}(x)).
]
Applying Lemma 2 to the formula (\mathfrak A(F_{i_1}(x),\ldots,F_{i_n}(x))), we obtain
[
\neg\neg \exists k\mid!\sim \mathfrak A(F_{i_1}(k),\ldots,F_{i_n}(k)).
]

Theorem 2. If a finite pseudo-Boolean algebra (A) is modelable with respect to realizability and all arithmetical instances of the propositional formula (\mathfrak A) are derivable in intuitionistic arithmetic, then the formula (\mathfrak A) is universally valid in the algebra (A).

Proof. If the formula (\mathfrak A) were refutable in (A), then, by Theorem 1, there could not fail to exist an arithmetical instance of (\mathfrak A) that is not derivable in (S).

Fig. 1. Diagram

A nontrivial example of a finite pseudo-Boolean algebra modelable with respect to realizability is provided by the algebra represented by the diagram in Fig. 1. The corresponding system of arithmetical formulas for this algebra was constructed by V. A. Yankov in ((^2)). From the main result of J. Rowe in ((^1)) on the incompleteness of the calculus (H) it follows that there also exist finite pseudo-Boolean algebras not modelable with respect to realizability—such is any finite pseudo-Boolean algebra on which some realizable propositional formula is refutable. Therefore, in particular, finite pseudo-Boolean algebras not modelable with respect to realizability occur in every characteristic for (I) sequence (A_1,A_2,\ldots) of such algebras; and if, moreover, (\mathscr L(A_1)\equiv \mathscr L(A_2)\equiv\cdots) (as is the case, for example, for the so-called Jaśkowski matrices (see ((^1)))), then, starting with some point, all these algebras (A_i) are not modelable with respect to realizability.

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

Received
23 X 1969

REFERENCES

(^1) G. Rowe, Trans. Am. Math. Soc., 75, 1 (1953).
(^2) V. A. Yankov, DAN, 151, No. 5 (1963).
(^3) S. K. Kleene, Introduction to Metamathematics, Moscow, 1957.
(^4) H. Rasiowa, R. Sikorski, The Mathematics of Metamathematics, Warszawa, 1963.
(^5) A. A. Markov, Tr. Matem. inst. im. V. A. Steklova AN SSSR, 67, 8 (1962).