Abstract
Full Text
MATHEMATICS
B. Ya. FALEVICH
A NEW METHOD OF PROVING INCOMPLETENESS THEOREMS FOR SYSTEMS WITH CARNAP’S RULE AND ITS APPLICATION TO THE QUESTION OF THE RELATIONSHIP BETWEEN CLASSICAL AND CONSTRUCTIVE ANALYSIS
(Presented by Academician P. S. Aleksandrov, 3 I 1958)
Rosser ($^1$) transferred the incompleteness theorems proved by Gödel to systems with a restricted Carnap rule of rank $<\omega^2$. In § 1 of the present paper these results are extended to systems containing a restricted Carnap rule of very substantial transfinite ranks. In § 2 the possibility of constructing a constructive model of classical analysis is considered.
§ 1. By transfinite induction on $\nu$ we define $S_\nu$—a system with a restricted Carnap rule of rank $\nu$. $S_0$ is a system consisting of the narrow predicate calculus, considered over arithmetic, supplemented by quantifiers over predicates with the corresponding* axioms and rules of inference (but without predicates of predicates), and by the axiom of reducibility—for every formula in the system there exists a predicate equivalent to it. If the system $S_\nu$ has been defined, then a formula $\mathfrak A$ is regarded as derivable in the system $S_{\nu+1}$ if: 1) the formula $\mathfrak A$ is derivable in the system $S_\nu$; 2) the formula $\mathfrak A(a)$ contains a free variable $a$ and the formulas $\mathfrak A(n)$ are derivable in $S_\nu$ for every natural $n$ (Carnap’s rule); 3) the formula is derivable from the formulas indicated in points 1), 2) by a finite number of applications of the rules of inference of the system $S_0$. If $\nu$ is of the second kind, then
\[ S_\nu=\sum_{\beta<\nu} S_\beta . \]
The results of the paragraph may be formulated as follows. Let $x<y$ denote a predicate of the system $S_\nu$ that well-orders the natural series according to the transfinite type $\nu$. Suppose that $\nu$ is a complete** transfinite number and that there exists a transfinite number $\tau$, less than $\nu$, such that in the system $S_\tau$: 1) it is provable that the predicate $x<y$ well-orders the natural series; 2) for any natural numbers $n$ and $m$ either the formula $n<m$ or the formula $\overline{n<m}$ is derivable (the predicate $x<y$ is decidable); 3) it is provable that $\nu$ is a complete transfinite number. Denote by $\delta$ the nearest complete transfinite number greater than $\tau$. Then, if the system $S_\alpha$, $\delta\leqslant\alpha\leqslant\nu$, is consistent, there exists in it a formula such that neither it nor its negation is derivable, and a formula expressing the consistency of the system $S_\alpha$ can be constructed in it, but is in the system $S_\alpha$ an underivable formula.
The simplest and most important case is that in which $x<y$ is a primitive-recursive predicate and $\tau=0$. Then, proceeding only from the assumptions:
I. In $S_0$ it is derivable that the predicate $x<y$ well-orders the natural
* Analogous to the axioms and rules of inference for quantifiers in the narrow calculus.
** A transfinite number $\nu$ is called complete if, for any $\sigma<\nu$, the set of transfinite numbers $\beta$, $\sigma\leqslant\beta<\nu$, and the set of transfinite numbers less than $\nu$, considered as well-ordered sets, are similar.
series, theorem (1) is proved for all systems \(S_\alpha\), \(6 \leq \alpha \leq \nu\). Below, for this simpler case, a complete construction of the provability predicates of the systems \(S_\alpha\) is given, and the most important points of the proof are indicated. All predicates and functions considered below are primitive recursive.
Denote by \(x <_1 y\) a predicate that well-orders the natural-number series according to the transfinite type \(\mu\), for which condition (1) is fulfilled. We shall assume that \((x)[0 \leq_1 x]\). Put*:
\[ \varphi(x)=\left[\frac{x+1}{2^{\operatorname{exp}_0(x+1)}}\right]-1, \]
\[ x <_2 y \equiv (Ez_1)_{z_1 \leq x}(Ez_2)_{z_2 \leq y} \left\{2z_1=x \,\&\, 2z_2=y \,\&\, \left[\frac{x}{2}\right] <_1 \left[\frac{y}{2}\right]\right\}, \]
\[ x <_3 y=\{\varphi(x)<_2 \varphi(y)\vee[\varphi(x)=\varphi(y)\,\&\, \operatorname{exp}_0(x+1)<\operatorname{exp}_0(y+1)]\}. \]
The predicate \(x <_3 y\) well-orders the natural-number series according to the transfinite type \(\nu=\omega\times\mu\), and assertion (1) holds for it; everywhere below the initial system is taken to be \(S_\nu\) and the predicate \(x <_3 y\).
\[ x <_4 y \equiv (Ez_1)_{z_1 \leq x}(Ez_2)_{z_2 \leq y} \left\{2z_1=x \,\&\, 2z_2=y \,\&\, \left[\frac{x}{2}\right] <_3 \left[\frac{y}{2}\right]\right\}. \]
We shall denote the even numbers, ordered by the predicate \(x <_4 y\) according to the transfinite type \(\nu\), by the letters \(\alpha,\beta,\gamma,\ldots\), and use them as indices for denoting systems, for example \(S_\alpha,S_\beta\). The function \(\alpha\oplus 1=4\alpha/2+2\) gives the transfinite number \(\alpha\oplus1\), immediately following \(\alpha\) in the ordering \(\beta <_4 \gamma\). \(f(\alpha)=\alpha\oplus1\), if \(\alpha <_4 \alpha_\omega\); \(f(\alpha)=\alpha\), if \(\alpha_\omega \leq_4 \alpha\), where \(\alpha_\omega\) is the even number playing the role of the transfinite number \(\omega\) in the ordering \(\beta <_4 \gamma\).**
\[ x <_5 y=\{\varphi(x)<_4 \varphi(y)\vee[\varphi(x)=\varphi(y)\,\&\, \operatorname{exp}_0(x+1)<\operatorname{exp}_0(y+1)]\}. \]
The predicate \(x <_5 y\) well-orders the natural-number series according to the transfinite type \(\omega\times\nu\). The even numbers \(\alpha,\beta,\ldots\) play, in this ordering, the role of transfinite numbers of the second kind. The function \(\psi(x)=\operatorname{exp}_0[\operatorname{exp}_0(x+1)]\) will be a function of large span on each set of natural numbers \(M_\alpha=\{n\},\ \alpha \leq_5 n <_5 \alpha\oplus1\).
Let us proceed to the construction of the provability predicates of the systems \(S_\alpha\) and of the system \(S_\nu\). Suppose that an arithmetization has been constructed for the system \(S_0\). We take as known the following predicates and functions. \(A(x)\) is the predicate: the number \(x\) is the number of an axiom of the system \(S_0\); \(F(x,y,z)\) is the predicate: the formula with number \(z\) directly follows, by the inference rules of the system \(S_0\), from the formulas with numbers \(x\) and \(y\); \(s(x,j)\) is the function giving the number of the formula obtained from the formula with number \(x\) by replacing the free variable \(a\) by the number \(j\). Denote
\[ \Delta_1(y)\equiv A[\psi(y)]; \]
\[ \Delta_2(y_1,y_2,y,T)\equiv [y_1 <_5 y \,\&\, y_2 <_5 y \,\&\, \varphi(y_1)=\varphi(y_2)=\varphi(y)\,\&\, T(y_1)\,\&\,T(y_2)\,\& \]
\[ \&\,F(\psi(y_1),\psi(y_2),\psi(y))]; \]
\[ \Delta_3(y',y,j,T)\equiv [\varphi(y')<_5\varphi(y)\,\&\,T(y')\,\&\,\psi(y'')=s(\psi(y),j)]; \]
\[ U(x,T)\equiv(y)\,[y\leq_5 x\to\{T(y)\sim[\Delta_1(y)\vee(Ey_1)(Ey_2)\Delta_2(y_1,y_2,y,T)\vee \]
\[ \vee(j)(Ey'')\Delta_3(y'',y,j,T)]\}]; \]
\[ B(x)\equiv(ET)\,U(x,T)\,\&\,T(x);\qquad B(x,z)\equiv\psi(x)=z\,\&\,B(x); \]
\(B(x,z)\) is the provability predicate of the system \(S_\nu\): the number \(x\) is a proof in \(S_\nu\) of the formula with number \(z\).
* For the functions \(x/y\), \(\operatorname{exp}_n(x)\), and \(\operatorname{long}(y)\), see (4).
** For odd numbers \(x\) one may take \(f(x)=0\).
We define, by transfinite induction on \(\alpha\), the provability predicates of the systems \(S_\alpha\), \(B_\alpha(x,z)\). Put:
\[ D_0(y)\equiv (i)_{i\leq \operatorname{long}(y)} \{[\Delta_1(\exp_i(y))\vee (En)_{n<i}(Em)_{m<i}F(\psi[\exp_n(y)],\psi[\exp_m(y)],\vee[\exp_i(y)])]\ \& \]
\[ \&\ \exp_i(y)<_5 f(0)\}\ \&\ (n)_{n\leq \operatorname{long}(y)}(m)_{m\leq \operatorname{long}(y)} [n<m\to \exp_n(y)<_5\exp_m(y)]; \]
\[ B_0(x)\equiv (Ey)_{y\leq \zeta(x)}[D_0(y)\ \&\ \exp_{\operatorname{long}(y)}(y)=x], \]
where \(\zeta(x)\) is a certain definite function bounding the quantifier;
\[ B_0(x,z)\equiv \psi(x)=z\ \&\ B_0(x). \]
If the predicates \(D_\alpha(y)\), \(B_\alpha(x)\), and \(B_\alpha(x,z)\) have been constructed, then
\[ D_{\alpha\oplus 1}(y)\equiv \]
\[ \equiv (i)_{i\leq \operatorname{long}(y)} \{[\Delta_1(\exp_i(y))\vee (En)_{n<i}(Em)_{m<i}F(\psi[\exp_n(y)],\psi[\exp_m(y)],\psi[\exp_i(y)]) \vee \]
\[ \vee (j)(Ey')\Delta_3(y',\exp_i(y),j,B_\alpha)]\ \&\ f(\alpha)\leq_5 \exp_i(y)<_5 f(\alpha\oplus 1)\}\ \& \]
\[ \&\ (n)_{n\leq \operatorname{long}(y)}(m)_{m\leq \operatorname{long}(y)} [n<m\to \exp_n(y)<_5\exp_m(y)]; \]
\[ B_{\alpha\oplus 1}(x)\equiv B_\alpha(x)\vee (Ey)_{y\leq \zeta(x)} [D_{\alpha\oplus 1}(y)\ \&\ \exp_{\operatorname{long}(y)}(y)=x]; \]
\[ B_{\alpha\oplus 1}(x,z)\equiv \psi(x)=z\ \&\ B_{\alpha\oplus 1}(x). \]
If \(\alpha\) is of the second kind, then
\[ B_\alpha(x,z)\equiv \psi(x)=z\ \&\ B(x)\ \&\ x<_5 f(\alpha). \]
The proof of the theorem is based on the following lemmas:
Lemma 1. In \(S_0'\) the following formulas are derivable:
1) \[ U(x,T_1)\ \&\ U(x,T_2)\to (y)\{y<_5 x\to [T_1(y)\sim T_2(y)]\}; \]
2) \[ U(x,B); \]
3) \[ x<_5 f(\alpha)\to U(x,B_\alpha); \]
4) \[ B_\alpha(x)\sim B(x)\ \&\ x<_5 f(\alpha). \]
Lemma 2. The formula \(B_\alpha(x,z)\) \((B(x,z))\) is decidable in the system \(S_\alpha\) \((S_\nu)\).
Lemma 3. If from the formula with number \(n\) in \(S_\alpha\) (in \(S_\nu\)) without application of Carnap’s rule a formula with number \(m\) is derivable, then in \(S_0\) the formula
\[ (Ex)B_\alpha(x,n)\to (Ex)B_\alpha(x,m) \quad ((Ex)B(x,n)\to (Ex)B(x,m)) \]
is derivable.
Lemma 4. If the number \(r\) is the number of a formula; \(e(z)\) is a function giving the number of the formula that is the negation of the formula with number \(z\), then in \(S_{0\oplus 1}\) the formulas
\[ (Ex)B_\alpha(x,e(r))\to (Ex)B_\alpha(x,e[s(r,y)]), \]
\[ (Ex)B(x,e(r))\to (Ex)B(x,e[s(r,y)]) \]
are derivable.
Lemma 5. In the system \(S_{0\oplus 6}\) (putting \(0\oplus(k+1)=(0\oplus k)\oplus 1\)) for every number \(q\) the formulas
\[ B_\alpha(x,q)\to (Eu)B_\alpha(u,s(r_\alpha,x)),\quad \text{where } r_\alpha \text{ is the number of the formula } B_\alpha(a,q); \]
\[ B(x,q)\to (Eu)B(u,s(r,x)),\quad \text{where } r \text{ is the number of the formula } B(a,q). \]
are derivable.
Lemmas 3, 4, and 5 are, respectively, the 1st, 2nd, and 3rd conditions of applicability of Gödel’s second theorem, indicated by Hilbert and Bernays in \((^2)\). The principal method of proof of the lemmas is transfinite induction.
The proof of the incompleteness theorems themselves for the systems \(S_\alpha\), \(0\oplus 6\leq_5\alpha\), and the system \(S_\nu\), is carried out according to the schemes given by Hilbert and Bernays in \((^2)\).
§ 2. In the present work, as a formalization of classical analysis, the system \(S_0\) described above has been chosen. Such a choice is justified, since, on the one hand, the theory of the continuum can be constructed quite simply in this system by coding real numbers by predicates; on the other hand, set theory is considerably broader than the system \(S_0\). As an example of constructive analysis the system B of Ackermann \((^3)\) is taken. The principal result is the following theorem.
Theorem. In Ackermann’s constructive analysis a proper model of the system \(S_0\) cannot be constructed.
Below we formulate the notion of a proper model and indicate the method of proof of the theorem.
We shall call an axiomatic system \(\widetilde S\) a subsystem of the axiomatic system \(A\) if the sets of terms and formulas of the system \(\widetilde S\) are, respectively, subsets of the sets of terms and formulas of the system \(A\). We shall call a subsystem \(\widetilde S\) of the axiomatic system \(A\) a model of the axiomatic system \(S\) in the system \(A\), if: 1) between the sets of terms and formulas of the system \(\widetilde S\) and, respectively, the sets of terms and formulas of the system \(S\), 2) between the axioms and rules of inference of the systems \(\widetilde S\) and \(S\), one can establish a one-to-one correspondence which is an isomorphism with respect to the rules of inference of the systems \(\widetilde S\) and \(S\).
Suppose that in the system \(S\) there have been constructed: 1) an arithmetization of the system \(S\) and the provability predicate of this system \(B(x,z)\); 2) an arithmetization of the system \(A\) and the provability predicate of the system \(A\), \(B_A(x,z)\); 3) a function \(e_A(n_A)\), which, from the number \(n_A\) of a formula of the system \(A\), gives the number of the formula that is (in the sense of the system \(A\)) its negation.
A model \(\widetilde S\) of the system \(S\) in the system \(A\) is called proper if the following four conditions are fulfilled: 1) in the system \(S\) one can construct the provability predicate of the system \(\widetilde S\), \(\widetilde B(x,z)\), and, for every natural number \(n\), derive the formula \((Ex)\widetilde B(x,n)\to(Ex)B_A(x,n)\); 2) if \(x\) is the number of a formula of the system \(S\), and \(\tilde x\) is the number of the formula corresponding to this formula in the model \(\widetilde S\), then in the system \(S\) there exists a function \(f(x)\) such that \(f(x)=\tilde x\); 3) in the system \(S\) there exists a formula with number \(r\), and in the system \(A\) there exists a derivable formula with number \(t_A\), such that in \(S\) the formulas \((Ex)B_A(x,t_A)\) and \(f(r)=e_A(t_A)\) are provable; 4) if in the system \(S\), for the number \(n\), the formula \((Ex)\widetilde B(x,f(n))\) is derivable, then the formula \((Ex)B(x,n)\) is also derivable.
The proof of the theorem relies only on conditions 1)—4) of the propriety of the model. First of all, in the system \(S_0\) the provability predicate of Ackermann’s system is constructed. Since Ackermann’s constructive analysis is a system with a restricted Carnap rule of a certain transfinite rank, this can be done by the same method by which provability predicates were constructed above for the systems \(S_\nu\). It is then shown that Ackermann’s proof of consistency, given for his system of constructive analysis, can be formally carried out in the system \(S_0\), i.e. that in \(S_0\) a formula expressing the consistency of Ackermann’s system is derivable.
The final stage of the proof is carried out by contradiction. Suppose that there exists a proper model \(\widetilde S_0\) of the system \(S_0\) in Ackermann’s constructive analysis. Then, by the properties of a proper model, from the formula expressing the consistency of Ackermann’s system in \(S_0\), a formula is derivable expressing the consistency of the proper model \(\widetilde S_0\), and from this latter formula a formula is derivable expressing the consistency of the system \(S_0\) itself; and we arrive at a contradiction with the second incompleteness theorem for the system \(S_0\), which asserts that the formula expressing the consistency of the system \(S_0\) is not derivable within this system.
Rybinsk Evening
Institute of Aviation Technology
Received
25 XII 1957
REFERENCES
- B. Rosser, J. Symb. Log., 2, No. 3, 129 (1937).
- D. Hilbert, P. Bernays, Grundlagen der Mathematik, Berlin, 1, 1934; 2, 1939.
- W. Ackermann, Math. Zs., 55, No. 3, 364 (1952); 57, No. 2, 155 (1953).
- R. Peter, Recursive Functions, Moscow, 1954.