Abstract
Full Text
MATHEMATICS
F. L. VARPAKHOVSKII
ON THE UNREALIZABILITY OF THE DISJUNCTION OF UNREALIZABLE FORMULAS OF PROPOSITIONAL LOGIC
(Presented by Academician P. S. Novikov, November 14, 1964)
The notion of realizability of logical-arithmetical formulas was introduced by Kleene \((^{1,2})\). On the basis of this notion one defines the class of realizable formulas of propositional logic. Namely: a formula of propositional logic is considered realizable if every formula obtained from it by substituting formulas of arithmetic for propositional variables is realizable. It is known that all formulas derivable in Heyting’s intuitionistic calculus are realizable \((^3)\); Rose constructed the first example of a realizable formula not derivable in Heyting’s calculus \((^4)\).
For Heyting’s calculus the following assertion holds: if the formula \(\mathfrak A_1 \vee \mathfrak A_2\) is derivable, then at least one of the formulas \(\mathfrak A_1, \mathfrak A_2\) is derivable. In connection with Rose’s result, the question arises whether the analogous assertion is true for realizable formulas, i.e., whether the realizability of the formula \(\mathfrak A_1 \vee \mathfrak A_2\) implies the realizability of at least one of the formulas \(\mathfrak A_1, \mathfrak A_2\). It turns out that the question posed in this (classical) form is answered in the affirmative.
We introduce the following notation. The expression \(\mathfrak A(a_1,\ldots,a_n)\) (abbreviated \(\mathfrak A(a_i)\)) denotes a formula of propositional logic that contains no propositional variables other than \(a_1,\ldots,a_n\). Capital Latin letters with or without indices denote formulas of arithmetic. An expression of the form \(A(x_1,\ldots,x_m)\) denotes a formula of arithmetic that contains no free variables other than \(x_1,\ldots,x_m\). The result of substituting the arithmetic formulas \(A_i\) for the propositional variables \(a_i\) in the formula \(\mathfrak A(a_i)\) is written in the form \(\mathfrak A(A_i)\). The expression
\[ kr\mathfrak A(A_i(x_1,\ldots,x_m))(\varphi(x_1,\ldots,x_m))r\mathfrak A(A_i(x_1,\ldots,x_m)) \]
means that the number \(k\) (the general-recursive function \(\varphi(x_1,\ldots,x_m)\)) realizes the formula \(\mathfrak A(A_i(x_1,\ldots,x_m))\).
Definition. A set of formulas of arithmetic \(\{A_1,\ldots,A_n\}\) is called a refutation of the formula \(\mathfrak A(a_1,\ldots,a_n)\) of propositional logic, and the formula \(\mathfrak A(a_1,\ldots,a_n)\) is called refutable, if the formula \(\mathfrak A(A_1,\ldots,A_n)\) is unrealizable.
Theorem. The disjunction of refutable formulas is refutable.
Let us briefly consider the construction used and the course of the proof of the theorem.
- Let the formulas \(\mathfrak A_1(a_i)\), \(\mathfrak A_2(a_i)\) be refutable and let \(\{A_{1i}\}\), \(\{A_{2i}\}\) be their refutations. We may assume that the formulas of the set \(\{A_{1i}\}\) contain freely no more than one variable, the same one for all formulas \(A_{1i}\), and analogously for the set \(\{A_{2i}\}\). We may further assume that the free variables of the sets \(\{A_{1i}\}\) and \(\{A_{2i}\}\) are distinct from one another; let these be the variables \(x_1, x_2\). By the definition of refutation, for the sets \(\{A_{1i}(x_1)\}\), \(\{A_{2i}(x_2)\}\) and arbitrary general-recursive \(g\) and \(h\)
\[ \neg g(x_1)\ r\ \mathfrak{A}_1(A_{1i}(x_1)), \tag{1} \]
\[ \neg h(x_2)\ r\ \mathfrak{A}_2(A_{2i}(x_2)). \tag{2} \]
2. A formula \(R(x)\) is constructed which expresses, in the logical-arithmetical language, the following meaningful predicate: “\(x\) is the Gödel number of a partial-recursive function \(\varphi\) of one variable and \(\varphi(x)=0\).” It is proved that for all \(x\) the truth of the indicated predicate is equivalent to the realizability of \(R(x)\).
3. As a refutation of the formula \(\mathfrak{A}_1(a_i)\vee \mathfrak{A}_2(a_i)\) one takes the set
\[ \{A_{1i}(x_1)\ \&\ \neg R(x)\ \vee\ A_{2i}(x_2)\ \&\ \neg R(x)\} \]
(abbreviated as \(\{M_i(x_1,x,x_2)\}\)), where the variable \(x\) is chosen distinct from the variables \(x_1,x_2\).
4. Suppose now that the formula \(\mathfrak{A}_1(M_i)\vee \mathfrak{A}_2(M_i)\) is realizable, i.e., for some general-recursive function \(f\)
\[ f(x_1,x,x_2)\ r\ \mathfrak{A}_1(M_i(x_1,x,x_2))\vee \mathfrak{A}_2(M_i(x_1,x,x_2)). \tag{3} \]
From the definition of realizability of disjunction \((^1)\) it follows that
\[ f(x_1,x,x_2)=2^{f_0(x_1,x,x_2)}3^{f_1(x_1,x,x_2)}, \]
and both functions \(f_0,f_1\) are general-recursive.
5. Two partial-recursive functions \(\rho_1(a)\) \((\rho_2(a))\) are constructed having the following properties: if \(a\) realizes the formula \(\mathfrak{A}_1(M_i(x_1,x,x_2))\) (the formula \(\mathfrak{A}_2(M_i(x_1,x,x_2))\)) and the formula \(R(x)\) is realizable (unrealizable), then \(\rho_1(a)\) \((\rho_2(a))\) is defined and realizes the formula \(\mathfrak{A}_1(A_{1i}(x_1))\) (the formula \(\mathfrak{A}_2(A_{2i}(x_2))\)). In constructing the functions \(\rho_1(a)\), \(\rho_2(a)\), one uses a well-known consequence of Nelson’s theorem, according to which, for every formula \(\mathfrak{A}(a_i)\) of propositional logic derivable in Heyting’s calculus, one can indicate a number \(k\) such that \(k\ r\ \mathfrak{A}(A_i)\) for any \(A_i\) \((^1)\).
6. Next, let
\[ (Ex_2)(x_1)f_0(x_1,\psi(x_1,x_2),x_2)=0, \tag{4} \]
where \(\psi(x_1,x_2)\) is a primitive-recursive function such that, for arbitrary fixed \(x_1^*,x_2^*\), \(\psi(x_1^*,x_2^*)\) gives the Gödel number of the general-recursive function \(f_0(x_1^*,x,x_2^*)\) of one variable \((^1)\). If \(x_2^*\) is chosen in accordance with (4) so that
\[ (x_1)f_0(x_1,\psi(x_1,x_2^*),x_2^*)=0, \]
then, as is proved, the function
\[ \rho_1\bigl(f_1(x_1,\psi(x_1,x_2^*),x_2^*)\bigr) \]
is general-recursive and realizes \(\mathfrak{A}_1(A_{1i}(x_1))\), in contradiction with (1). Therefore from (1), (2), (3) it follows that
\[ \neg(Ex_2)(x_1)f_0(x_1,\psi(x_1,x_2),x_2)=0. \tag{5} \]
7. Condition (5) is transformed into the condition
\[ (x_2)(Ex_1)f_0(x_1,\psi(x_1,x_2),x_2)=1. \tag{5′} \]
From (5′) it follows that the function
\[ \chi(x_2)=\mu x_1\bigl(f_0(x_1,\psi(x_1,x_2),x_2)=1\bigr) \]
is general-recursive. In this case, as is not difficult to prove, the function
\[ \rho_2\bigl(f_1(\chi(x_2),\psi(\chi(x_2),x_2),x_2)\bigr) \]
is general-recursive and realizes \(\mathfrak{A}_2(A_{2i}(x_2))\). The contradiction obtained proves the theorem.
In passing from (5) to (5′) the Leningrad principle is used.
Received
14 XI 1964
CITED LITERATURE
- S. K. Kleene, Introduction to Metamathematics, Moscow, 1957.
- S. C. Kleene, J. Symbolic Logic, 10, 109 (1945).
- D. Nelson, Trans. Am. Math. Soc., 61, 307 (1947).
- G. F. Rose, Trans. Am. Math. Soc., 75, 1 (1953).