数理解析研究所講究録
912 巻 1995 年 82-84

82

A FORMULA SEPARATING TWO THEORIES
Takeshi Yamaguchi(e-mail: y-takesi@is titech .

(山口$\mathrm{a}\mathrm{c}.\mathrm{j}_{\mathrm{P})}$武志)(東工大・情報理工)

Abstract

is incomplete, then there is a formula such that
If theory, Rosser sentence of is a separating formula.
. In special case$\mathrm{T}+\neg\psi$$\varphi$$\psi=\mathrm{C}\mathrm{o}\mathrm{n}(\mathrm{T})$$\varphi\subset\wedge \mathrm{T}+\psi$$0$$\mathrm{T}\subseteq \mathrm{T}+$$\mathrm{T}$. Preliminaries

We consider only forlnulas in Arithlnetic. A theory is a set of sentences that contains
isdenotes the least theory which contains
all of its logical consequences.
sentence).
isatheory,ameans “ is provable in ”$\mathrm{T}\mathrm{U}\{\varphi\}(\mathrm{T}$$\mathrm{T}+\varphi$$\varphi$$\mathrm{T}$$\mathrm{T}\vdash\varphi$$\varphi$

1. A formula separating two theories
be theories.
Definition LetA sentence separates from$\mathrm{T},$$\mathrm{S}$$\mathrm{T}$$\mathrm{s}\mathrm{g}_{\mathrm{T}}\mathrm{f}\subseteq \mathrm{T}+\varphi\subset\wedge \mathrm{S}$$\varphi$

Lemma 1 Let be a theory,on are equivalent.
$\mathrm{T}$$\psi$

be a sentence, and$\mathrm{T}\subset\wedge \mathrm{T}+\psi$. The following conditions$\varphi$1.

$\varphi$2.

separates

(i)
(ii)

Proof)$\mathrm{T}\mu_{\varphi}$from$\mathrm{T}+\psi$

.

, and

$\mathrm{T}\vdash\psiarrow\varphi,$$\mathrm{T}\subseteq \mathrm{T}+\varphi$

Remarktheory.)$\mathrm{T}$$\mathrm{T}\mu_{\varphi}arrow\psi$.

is equivalent to (i).

$\mathrm{T}+\varphi\subset\wedge \mathrm{T}+\psi$is equivalent to (ii).

$\mathrm{T}\subseteq \mathrm{T}+\varphi\subseteq \mathrm{T}+\psi\Leftrightarrow \mathrm{T}+\neg\psi\subseteq \mathrm{T}+\neg\varphi\subset\wedge$$\square$Incon. (Incon is the inconsistent83

is incomplete, then there is a formula separating froln
Theorem Ifbecause
andsuch thatProof) There is a sentence. It is easily verified that satisfy the conditions of theincolnplete. Let.
remark. So this is a separating sentence from$\mathrm{T}+\psi$$\mathrm{T}$$\mathrm{T}+\urcorner\psi$$\varphi$$\varphi\underline{=}\varphi’\vee\psi$$\mathrm{T}+\neg\psi$$\mathrm{T}+\neg\psi\mu\neg\varphi’$$\mathrm{T}+\urcorner\psi^{\mu}\varphi’$$\varphi’$.

is$\varphi$$\mathrm{a}\mathrm{b}\mathrm{o}\mathrm{v}_{\square }\mathrm{e}$$\mathrm{T}+\psi$$\mathrm{T}$$\varphi$Con(T) by second
is a consistent primitive rec.ursive theory, thenis a consistent primitive recursive theory,
incompleteness theorem [2]. So
is incomplete by Rosser’s theoreln [2]. So there is atoo. We have thattheory between and T+Con(T) by above theoreln.

Remark If$\mathrm{T}\mu$$\mathrm{T}$$\mathrm{T}+\neg \mathrm{C}_{0}^{l}\mathrm{n}(\mathrm{T})$$\mathrm{T}+\neg \mathrm{C}\mathrm{o}\mathrm{n}(\mathrm{T})$$\mathrm{T}$

2. On a formula separating$\mathrm{T}$from$\mathrm{T}+\mathrm{C}\mathrm{o}\mathrm{n}(\mathrm{T})$In the previous section, we showed that there is a theory between and T+Con(T),is consistent and primitive recursive). Actually, let be a Rosser sentence ofare separating sentences. In this section, we show thatandthenRosser sentence of itself is a sentence separating from T+Con(T). We will use certain
results on the provability predicate. See [1], [2].
$\mathrm{T}$$(\mathrm{T}$$\mathrm{T}+\neg \mathrm{C}\mathrm{o}\mathrm{n}(\mathrm{T})$$\varphi$$\varphi\vee \mathrm{C}_{\mathrm{o}\mathrm{n}}(\mathrm{T})$$\urcorner\varphi\vee \mathrm{C}^{\mathrm{t}}\mathrm{o}\mathrm{n}(\mathrm{T})$$\mathrm{T}$$\mathrm{T}$Definition
Rosser sentence$\varphi$of$\mathrm{T}$is a sentence such that(1)$\mathrm{T}\vdash\varphirightarrow\urcorner \mathrm{P}\mathrm{r}^{*}(\ulcorner\urcorner\varphi)$where$\mathrm{P}\mathrm{r}^{*}(x)\underline{=}\exists y(\mathrm{p}\mathrm{r}\mathrm{o}\mathrm{v}\mathrm{T}(X, y)$A.

$\forall z\leq y(\urcorner \mathrm{P}\mathrm{r}\mathrm{o}\mathrm{v}_{\mathrm{T}}(\mathrm{n}\mathrm{o}\mathrm{t}(X), z)))$Theorem Rosser sentence is a sentence separatingProof) We show (i)implies that is the separating sentence.
(i)
is well-known as Rosser’s theorem.
(ii) By (1), we have$\mathrm{T}$$\varphi$$\mathrm{T}\mu_{\varphi},$$(\mathrm{i}\mathrm{i})\mathrm{T}\vdash \mathrm{C}\mathrm{o}\mathrm{n}(\mathrm{T})arrow\varphi,$from T+Con(T).
Con(T), and then lemma 1$(\mathrm{i}\mathrm{i}\mathrm{i})\mathrm{T}\mu_{\varphi}arrow$$\varphi$$\mathrm{T}\mu_{\varphi}$$\mathrm{T}+\neg\varphi\vdash\exists y(\mathrm{P}\mathrm{r}\mathrm{o}\mathrm{v}_{\mathrm{T}}(\ulcorner\urcorner\varphi, y))$.

That is$\mathrm{T}+\urcorner\varphi\vdash \mathrm{P}\mathrm{r}(\ulcorner\urcorner\varphi)$(2).

On the other hand, we have$\mathrm{T}\vdash \mathrm{C}\mathrm{o}\mathrm{n}(\mathrm{T})arrow\neg \mathrm{P}\mathrm{r}(\ulcorner\urcorner\varphi)$$\mathrm{T}\vdash \mathrm{C}\mathrm{o}\mathrm{n}(\mathrm{T})arrow\urcorner \mathrm{P}\mathrm{r}(\ulcorner_{\neg\varphi^{\urcorner}})$

(3)

.
.

by formalized Rosser’s theorem. Frolll (2) and (3), we have$\mathrm{T}+\urcorner\varphi\vdash_{\neg}\mathrm{c}^{1}\mathrm{o}\mathrm{n}(\mathrm{T})$$\mathrm{T}\vdash\neg\varphiarrow\neg \mathrm{C}\mathrm{o}\mathrm{n}(\mathrm{T})$,,$\mathrm{T}\vdash \mathrm{C}\mathrm{o}\mathrm{n}(\mathrm{T})arrow\varphi$

.

(4)

84

(iii) Assume that
, we havepredicate$\mathrm{T}\vdash\varphiarrow \mathrm{C}_{\mathrm{o}\mathrm{n}}(\mathrm{T})$. By the derivability conditions of the provabiity$\mathrm{P}\mathrm{r}()$$\mathrm{T}\vdash \mathrm{P}\mathrm{r}(\ulcorner_{\neg \mathrm{C}\mathrm{o}\mathrm{n}(\mathrm{T}})arrow\neg\varphi^{\urcorner})$,$\mathrm{T}\vdash \mathrm{P}\mathrm{r}(\ulcorner_{\neg \mathrm{C}\mathrm{o}\mathrm{n}()^{\urcorner}}\mathrm{T})arrow \mathrm{P}\mathrm{r}(\ulcorner_{\urcorner}\varphi^{\urcorner})$.

(5)

By (4) and (5),$\mathrm{T}\vdash \mathrm{P}\mathrm{r}(\ulcorner_{\neg \mathrm{C}\mathrm{o}\mathrm{n}()^{\urcorner}}\mathrm{T})arrow\urcorner \mathrm{C}\mathrm{o}\mathrm{n}(\mathrm{T})$.

Then we have$\mathrm{T}\vdash\urcorner \mathrm{C}\mathrm{o}\mathrm{n}(\mathrm{T})$by L\"ob’s theorem, and by assumption$\mathrm{T}\vdash\urcorner\varphi$

This contradicts that$\varphi$

is Rosser sentence.

.
$\square$

References[1] G. E. Boolos and R. C. Jeffery. Computability and Logic 3rd ed. . CAMBRIDGE UNIVERSITY PRESS 1989
[2] C. Smorytski. The Incompleteness Theorems, Handbook of Math. Logic (J. Barwiseed.). North-Holland 1977. pp.821-865