数理解析研究所講究録
1021 巻 1997 年 70-85

70

On some one variable axioms over intuitionistic S4.
志村立矢 (日本大学理工)はじめに. (–変数公理と SSP とその拡張)

1

細井は古典命題論理
ことを指摘した.

$\mathrm{C}=\mathrm{H}+p\vee\neg p$

Lemma 1 (細井) 論理式

$B$

に対し,

および $l\bm{1}+\neg p\vee\neg\neg p$ の公理は次のような性質を持つ$\mathrm{v}\mathrm{a}r(B)$で $B$ に現れる命題変数全体の集合を表す.

このとき次が成り立つ.

1.

$\mathrm{H}\vdash(\bigwedge_{\not\in \mathrm{v}\mathrm{a}\mathrm{r}(B)}p\vee\neg p)\supset(B\vee\neg B)$

2.

$\mathrm{H}\vdash(\bigwedge_{\not\in \mathrm{v}\mathrm{a}\mathrm{r}(B)}\neg p\vee\neg\neg p)\supset(\neg B\neg\neg B)$,

Proof.)$B$.
Q.E.D.

の構成に関する帰納法による.

Corollary 2 (細井) 論理式 $B$ に対し, 次が成り立つ.

1.

$\mathrm{C}\vdash B$

if and only if$\mathrm{H}\vdash$$( \wedge p\neg p)\supset B$,$\mathrm{p}\in \mathrm{v}\mathrm{a}\mathrm{r}\langle B)$2.

$\mathrm{H}+\neg p\neg\neg p\vdash B$

if and only if$\mathrm{H}\vdash$$( \wedge \neg p\vee\neg\neg p)\supset B$.

$p\in \mathrm{v}\mathrm{a}\mathrm{r}(B)$

この系の性質は後に simple substitution property (SSP) と名付けられ, 佐々木により多変数の場合も含めて研究されている.
小野は–変数公理が SSP を持つならば, それにより公理化される論理では Craig の補間定理が成立することを指摘した.

Leamm $ 命題変数として のみを含むような論理式
では Craig の補間定理が成立する.
$P$$A\zeta p$) が $SSP$ を持つならば,したがって, -変数公理で $SSP$ を持つものは細井による例しかない.

Proof.)$\mathrm{H}+A(p)\vdash B\supset c$$\mathrm{H}\vdash$$\wedge$斥

1$(B\supset C)$とする. このとき, SSP により$A(p)\supset(B\supset C)$$\mathrm{H}+A\zeta P$)

71が成り立つ. したがって$\mathrm{H}\vdash$$(B\wedge \wedge A(p).)\supset( \wedge A(p)\supset C)$$\not\in \mathrm{v}\mathrm{a}\mathrm{r}(C)$$\not\in \mathrm{v}\mathrm{a}\mathrm{r}(B)$となるが,$\mathrm{H}$では Craig の補間定理が成立するので,$\mathrm{v}\mathrm{a}r(D)\subseteq \mathrm{v}\mathrm{a}r(B)\cap \mathrm{v}\mathrm{a}r(C)$であるような

論理式 $D$ で$\mathrm{H}\vdash$$(B\wedge \wedge A(p))\supset D$,$p\in \mathrm{v}\mathrm{a}\mathrm{r}(B)$$\mathrm{H}\vdash D\supset( \wedge A(p)\supset C)$$\not\in \mathrm{v}\mathrm{a}r(C)$が成立するものが存在する. したがって,$\mathrm{H}+A(p)\vdash B\supset D$,$\mathrm{H}+A(p)\vdash D\supset C$

Q.E.D.

となりこれは $\mathrm{H}+A(p)$ で Craig の補間定理が成立することを示している.

様相論理においても SSP を考えることができ, 中間論理のときと同様に–変数論理式が SSPを持つならばこれにより公理化可能な論理では Craig の補間定理が成立することがわかる. これは,Maksinmva [5] が指摘している.

Lemma 4 (Maksimova)$\mathrm{S}4+$

口◇ P\supset ◇口 P および S4+ 口◇ P$\equiv$◇

P は $SSP$ を持つ.

$\square$

したがって, これらの論理では Craig の補間定理が成立する.
では, 細井によって SSP が示された論理式の$\mathrm{M}\mathrm{c}\kappa\dot{\mathrm{g}}\mathrm{s}\mathrm{e}\mathrm{y}$-Tarski translation を考えたとき SSPは成立するであろうか. この答は否定的である (例えば $\mathrm{S}5=\mathrm{S}4+T(P^{}-p)$ の場合は佐々木により示されている).
だが, これらの論理での Craig の補間定理の成立を示すためには, SSP よりも弱い次の性質
で十分である.

Fact 5 論理式 $B$ の部分論理式全体の集合を Sub $(B)$ で表す. このとき, 次が成り立つ.

1.

$\mathrm{S}5\vdash B$

if and only if$\mathrm{S}4\vdash$$( \wedge \square C\square \neg\square C)\supset B$

口 C\epsilon Sub

2.

$\mathrm{S}4.2\vdash B$

if and only if$\mathrm{S}4\vdash$

,

$(B)$

$( \wedge \square \neg\square c\vee\square \text{◇}\square c)\supset B$

口 C\epsilon Sub

.

$(B)$

このような性質を持つ–変数論理式により公理化される論理は他に次のようなものがある.
$\mathrm{R}i\mathrm{v}$$=$$\mathrm{S}4+p\supset\square p$$\mathrm{S}4\mathrm{G}\mathrm{r}\mathrm{Z}$$=$$\mathrm{S}4+\square (\square (p\supset\square p)\supset P)\supset P$$=$$\mathrm{S}4+\square (\square (p\supset\Pi p)\supset p)\supset(\square \text{◇}\square P\supset p)$

S4.1.4.

本稿では直観主義様相論理上で類似の性質を持つ–変数論理式の例を与え, これらにより公理化される論理での Craig の補間定理や丘 mite model property の成立を示す.

72

2

直観主義様相論理の semantics と sequent style system.
われわれが考察する論理は, 前原 [4] と Prawitz-Malmni [7] に現れたものであるが, これは

小野 [6] により Lo と名付けられ深く研究されている.

Defimltion 6(直観主義様相命題論理 intS4 ロ) intS4 ロは論理記号として
言語
上の公理及び推論規則として次のものを持つ論理である.

$\supset,$$\wedge,$$\vee,$$\square$$\neg,$を持つ$\mathcal{L}0$の公理,$\bullet$

直観主義命題論理$\bullet$$(K)\square (A\supset B)\supset(BoxA\supset\square B)$$\mathrm{H}$,,$\bullet(T)\square A\supset A$$\bullet(4)\square A\supset$$\bullet$$\bullet$$\bullet$

口口 A,

modus ponens,

necessitation rule,
substitution rule.

intS4 ロの拡張で modus ponens,
式の集合を直観主義様相論理と呼ぶことにする.

$\mathrm{n}\mathrm{e}\infty \mathrm{S}\mathrm{i}\mathrm{t}\mathrm{a}\mathrm{t}\mathrm{i}\mathrm{o}\mathrm{n}$直観主義論理上では◇ A を$\neg\square \neg A$

および substitution について閉じている論理で定義することはできない.

Definltion 7 (直観主義様相 fraxne (小野 fraxne) [6])き, 直観主義様相 frame という.
$\bullet\leq$

は $M$ 上の半順序である.

$R$

は $M$ 上の擬順序である.

$R$は$\bullet$$\bullet$$\leq$$\mathrm{M}=\langle M, \leq, R\rangle$

が次の条件を満たすとの拡張である. すなわち $a\leq b$ ならば $aRb$ となる.

直観主義様相 frameの元 $a\in M$ が与えられたとき, a 湯となる $b\in M$ 全体はと $R$ の制限により直観主義様相丘 ame となる. これを が生成する部分 frame と呼ぶ. ある $a\in M$ が生成する部分 frame が自身となるとき,は rooted であるという.
$\mathrm{M}$$\leq$$a$$\mathrm{M}$$\mathrm{M}$Definltion 8(直観主義様相 model) 直観主義様相丘 ame
命題変数

$P$

の関係

$a\models p,$$a\models p$

が$\mathrm{M}$上の付値であるとは$a\leq b\Rightarrow b\models p$が成立することをいう.
は次のようにして $a\in M$ と$\models$$\mathrm{M}=\langle M, \leq, R\rangle$$\mathcal{L}0$

論理式 $A$ との関係に拡張できる.

に対し,$a\in M$と73$\bullet$$a\models A\wedge B\Leftrightarrow$( $a\models A$ かつ $a\models B$ ),$\bullet$$a\models A\vee B\Leftrightarrow$( $a\models A$ または $a\models B$ ),$a\models A\supset B\Leftrightarrow\forall b$$\bullet$(( $a\leq b$ かつ$b\models A)\Rightarrow b\models B$$\bullet$$a\models\neg A\Leftrightarrow\forall b$( $a\leq b$ ならば $b\# A$),$\bullet$$a\models\square A\Leftrightarrow\forall b$($aRb$ ならば $b\models A$ ).

直観主義様相丘 ame
上の任意の付値$\mathrm{M}$といい,$\mathrm{M}\models\dot{A}$$\mathrm{M}$$\models$),の組を直観主義様相 model という.とその上の付値
で valid であると任意の $a\in M$ に対し $a\models A$ となるとき, $A$ は$\models$$\mathrm{M}$と記す.

$L(\mathrm{M})=\{A|\mathrm{M}\models A\}$と定義する.
この semantics は中間論理や様相論理のときと同様に次の性質を持つことがわかる.

Fact 9 (小野 [6])1. $a\leq b$ かつ

2.

$\mathrm{M}_{a}$を$a$$a\models A$$L(\mathrm{M})$を直観主義様相加 me,$\models$を$\mathrm{M}$上の付値とする.

ならば $b\models A$ .

が生成する

$a\models A$

3.

$\mathrm{M}$$\mathrm{M}$の部分 Pame,

if and $mly$ if$a\models’A$$\models’$を$\models$の $M_{a}$ への制限とするとき,.

は直観主義様相論理となる.

Defimltion 10

直観主義様相論理$\mathrm{L}$は直観主義様相 frame の族$\mathrm{M}$が存在して,$\mathrm{L}=\cap L(\mathrm{M}_{i})$と表すことができるとき, 完全であるという. さらに各は finite model property を持つという.
き,$\mathrm{M}$が有限なものをとることができると$\mathrm{L}$Theorem 11 (Ono [6])$\mathrm{i}\mathrm{n}\mathrm{t}\mathrm{S}40$

はこの semantics に関し完全であり,

finite model pr\rho pe 吻を持つ.

この定理は canonical model の存在と filtration method により示すことができるが, sequentcalculus と Kripke type semantics との関連で証明することもできる.

Lemma 12 (前原 [4], cf. Prawits-Malmn\"as [7])の$\mathrm{L}\mathrm{J}’$に次の推論規則を付け加えて得ることができる.

$\mathrm{i}\mathrm{n}\mathrm{t}\mathrm{S}40$

は Gentzen’s の$\mathrm{L}\mathrm{J}$

または前原

74

$A,\Gammaarrow\ominus$$(\square arrow)$$\square A,\Gammaarrow\Theta$$\square \Gammaarrow A$$(arrow\square )$$\square \Gammaarrow\square A$

これらの体系をそれぞれ$\mathrm{G}\mathrm{i}\mathrm{n}\mathrm{t}\mathrm{S}4\mathrm{O}$, G’ntS4 口と名付けると, GintS4 ロと G’intS4 口ではともに cut-elimination 法\mbox{\boldmath $\omega$}\mbox{\boldmath $\pi$}m が成立する.

の代わりに LK としたものは S4 に対する cut-丘 ee な形式化であることに注意せよ.
の cut-ehmination と同時に示すことができる.
はの方
ation は Craig の補間定理を導くことが知られている.

$\mathrm{L}\mathrm{J}$$\mathrm{T}\mathrm{h}\infty \mathrm{r}\mathrm{e}\mathrm{m}11$$\mathrm{G}’\mathrm{i}\mathrm{n}\mathrm{t}\mathrm{s}40$$\mathrm{c}\mathrm{u}\mathrm{t}- \mathrm{e}\mathrm{h}\mathrm{m}\dot{\mathrm{i}}$$\mathrm{G}\mathrm{i}\mathrm{n}\mathrm{t}\mathrm{S}40$

Theorem 1$
Proof.)$\mathrm{i}\mathrm{n}\mathrm{t}\mathrm{s}4_{\mathrm{O}}$$\mathrm{t}\mathrm{B}_{\mathrm{o}\mathrm{r}}\mathrm{i}\epsilon \mathrm{i}\acute{\mathrm{C}}[2])$では Crvnig の補間定理が成立する.

では cut-elimination が成立するので前原の方法を用いればよい.

$\mathrm{G}\mathrm{i}\mathrm{n}\mathrm{t}\mathrm{S}40$

Q.E.D.

filtration method

3

まず準備として我々がこの節で扱う –変数公理が直観主義様相 frame で真となるための条件について述べておこう.

Lemma 141.

2.

$\mathrm{M}=\langle M, \leq, R\rangle$$\square p\vee\square \neg\square p$$\mathrm{M}$で真となるための必要十分条件は $R$ が同値関係であることである.

で真となるための必要十分条件は任意のみたす $c\in M$ が存在することである.
$\square \neg\square p\vee\square \neg\square \neg\square p$$aRb_{1},$3.

がを直観主義様相加 me とする.

$\square p\neg\square p$$aRb_{2}$が$a\leq b$$\mathrm{M}$が$\mathrm{M}$$a,$ $b_{1},$ $b_{2}\in M$

ならば $b_{l}Rc$ , h 五 b.

で真となるための必要十分条件は

ならば

$bRn$

が成立することである.

4.

$p\supset\square p$が$\mathrm{M}$で真となるための必要十分条件は $\leq=R$ が成立することである.

に対し次を

75

5. $P^{\neg}P$ が6.

$\mathrm{M}$で真となるための必要十分条件は$\leq$

が同値関係であることである.

で真となるための必要十分条件は任意の$c\in M$ が存在することである.
$\neg p\vee\neg\neg p$が$a\leq b_{1},$$\mathrm{M}$$a\leq b_{2}$ならば$b_{1}\leq c,$$b_{2}\leq c$$a,$ $b_{1},$ $b_{2}\in M$

に対し次をみたす.

以下の証明は ffltration method に基づくものである.

Lemma 15
口 pV

を次の論理式のいつれかとする.

$A(p)$$\square$\neg$\square$p,$\square \neg\square p\vee\square \neg\square \neg\coprod p,$$\square p\vee\neg\square p$

.

このとき,
$\mathrm{i}\mathrm{n}\mathrm{t}\mathrm{S}4_{\mathrm{O}}+A(p)\vdash B\Leftrightarrow \mathrm{i}\mathrm{n}\mathrm{t}\mathrm{S}40\vdash( \wedge.

.

A(C))\supset B$

ロ C\epsilon sub(B)が成立する.

Proof.)

を示せば十分であるから対偶を示す.

$\Rightarrow$$\mathrm{i}\mathrm{n}\mathrm{t}\mathrm{S}4_{\mathrm{O}}\forall$$( \wedge \square A(C))\supset B$

口 C\epsilon Sub(B)と仮定する.
$\langle M, \leq, R\rangle$$\mathrm{i}\mathrm{n}\mathrm{t}\mathrm{S}40$

上の model$\mathrm{O}\models\square A(C),$$0\# B$$\bullet$$A(p)$の丘 nite model property により次の条件をみたす有限 rooted frmoe$\langle \mathrm{M}, \models\rangle$$\mathrm{M}=$が存在する.

,$(\square C\in \mathrm{S}\mathrm{u}\mathrm{b}(B))$.

が$\square p\vee\square \neg\square _{P}$$\mathrm{M}’=\langle M’, \leq’, R’\rangle$

のとき.

と

$\models’$を次のように定める.

$M’=M,$ $\leq’=\leq,$ $R’=M\mathrm{x}M$,$a\models’p\Leftrightarrow a\models p$.

躍は同値関係なのでときを考えれば) は$A\omega$

intS4 ロ $+A(p)\psi B$を示すことができる.

claim$D\in \mathrm{S}\mathrm{u}\mathrm{b}(B)$に対し,$\mathrm{M}’$で真となる. よって次の claim を示し, $D$ が $B$ 自身の

76$a\models’D$$D$がif and only if $a\models D$ .

の形のときを調べれば十分である. 舟は$\square C$$a\models’D$

ならば $a\models D$

は明らか.

逆に $a\#’\square C$ と仮定する.

$b\in M$ が存在し,$b\#’C$となるので帰納法の仮定より,.

$b\# C$O 湯であるから$0\#\square C$

であり,$\mathrm{O}\models A(C)$より,.

$0\models\square \neg\square C$

したがって$a\models\neg\square C$となり, 特に.

$a\#\square C$$\bullet$$A(p)$

が$\square \neg\square p\square \neg\square \neg\square p$のとき.

$a\in M$ が $R$ に関する極大元であるということを$aRb$ ならば $bRa$

により定義する.
$\mathrm{M}’=\{M’,$ $\leq’,$ $ff\rangle$と$\models’$を次のように定める.

$M’=M,$ $\leq’=\leq$ ,$aR’b\Leftrightarrow$( $aRb$ または$b$

は $R$ に関する極大元),$R$よりも強いので

77.

$a\models’p\Leftrightarrow a\models p$

先ほどと同様に次を示せばよい.

claim$D\in \mathrm{S}\mathrm{u}\mathrm{b}(B)$$a\models^{J}D$

$D$

に対し,

if and only if $a\models D$ .

が口 C の形のときを調べれば十分である. 舟は $R$ よりも強いので$a\models’D$

ならば $a\models D$

は明らか.

逆に $a\#’\square C$ と仮定する.

$aHb$$b\#^{J}C$となるので帰納法の仮定より,$b\# C$.

am ならば$a\#\square C$

である.

方

$b$

が $R$ に関し極大ならば$b\#\neg\square \neg\square C$

なので$\mathrm{O}\models A(C)$$0\models\square \neg\square C$

したがって$a\models\neg\square C$となり, 特に.

$a\#\square C$.

より,となる $b\in M$ が存在し,

78$\bullet$

$A[p$

) が

$\square pV\neg\square p$$\mathrm{M}’=\langle M^{j}, \leq’,R\rangle$$M’=M,$
$H=$

{

のとき.
と

$\models’$を次のように定める.

,$\leq^{J}=\leq$$(a,$ $b)|aRb$

または $b\leq a$ } の推移閉包.

$a\models’p\Leftrightarrow a\models p$

claimと $a\leq b$ に対し,$\square C\in \mathrm{S}\mathrm{u}\mathrm{b}(B)$$b\models\square C$.

$a\models\square C$とすれば $a\#\neg\square C$ なので$b\models\square C$

clalm

ならば

$\square C\in \mathrm{S}\mathrm{u}\mathrm{b}(B)$ならば$a\models’\square C$$a\#’\square C$$a\models\square c_{V\neg\square }C$より$a\models\square C$

.

に対し,

.

$a\models\square C$と仮定すれば $aKb$ かつ $b\#’C$ となる$b$が存在する. したがって句,$c_{1},$$\ldots,$$c_{n}\in M$が存在し,$a=c_{0}SC_{1}s\cdots S\text{ら}=b$となるが前の claim を用いて

( $S=R$ または$n$$\leq^{-1}$)に関する帰納法で $a\#\square C$ を示すことができる.

Q.E.D.

Lemma 16
$p\supset$$A(p)$

を次の論理式とする.

口 p.

このとき,
intS4 ロ)$+A\mathrm{C}P$.

$\vdash B\Leftrightarrow \mathrm{i}\mathrm{n}\mathrm{t}\mathrm{S}4_{\mathrm{O}}\vdash( \wedge \square A\omega))\supset B$$\not\in \mathrm{v}\mathrm{a}\mathrm{r}(B)$が成立する.

Proof.)$\mathrm{i}\mathrm{n}\mathrm{t}\mathrm{S}40\forall$$( \wedge \square A(p))\supset B$$\not\in \mathrm{v}\mathrm{a}\mathrm{r}(B)$79と仮定する.
$\langle$$M,$ $\leq,$ $R)$$\mathrm{i}\mathrm{n}\mathrm{t}\mathrm{S}40$の finite model

上の model が存在する.
$(p\in \mathrm{v}\mathrm{a}\mathrm{r}(B))$$\mathrm{O}\models\square A\zeta p),$pr.operty により次の条件をみたす有限 rooted 会 oe$\mathrm{M}=$,$0\# B$

このとき, 同値関係$\sim$

を

a\sim b\Leftrightarrow \Leftrightarrow (aB ち力 l つ $bRa$ )により定め,$M’=M/\sim$

とおき,$a\in M$ の属する同値類を$\overline{a}$で表す. このとき

I と-b\Leftrightarrow \Leftrightarrow aR\sim$R’,$
は順序関係であり,) は直観主義様相丘 ame となる.
次の claim が成立することは容易に示され, これより Lemma の主張が得られる。
$R^{r}$$\mathrm{M}’=\langle M’,$claim$\mathrm{M}’$

上の付値

を

$\models’$$\overline{a}\models’p\Leftrightarrow a\models p$により定めることができ,$a\models’D$$D\in \mathrm{S}\mathrm{u}\mathrm{b}(B)$に対し, 次が成り立つ.

if and only if $a\models D$ .
Q.E.D.

Lemma 17$A(p)$

を次の論理式のいつれかとする.

$p\vee\neg p,$ $\neg p\mathrm{v}\neg\neg p$

.

このとき,
$\mathrm{i}\mathrm{n}\mathrm{t}\mathrm{S}4_{\mathrm{O}}+A\mathrm{C}p)\vdash B\Leftrightarrow \mathrm{i}\mathrm{n}\mathrm{t}\mathrm{S}4_{\square }\vdash( \wedge \square A(p))\wedge( \wedge \square A(\square C))\supset B$$\mathrm{p}\in \mathrm{v}\mathrm{a}r(B)$口 C\epsilon sub(B)が成立する.

Proof.)$\Rightarrow$を示せば十分であるから対偶を示す.

$\mathrm{i}\mathrm{n}\mathrm{t}\mathrm{S}40\psi$($\wedge$$p\in \mathrm{v}\mathrm{a}t(B)$$\square A(p)$)$\wedge($$\wedge$$\text{口}c\epsilon \mathrm{s}_{\mathrm{u}}\mathrm{b}(B)$$\square A(C))\supset B$.

80と仮定する.
$\langle M, \leq, R\rangle$$\mathrm{i}\mathrm{n}\mathrm{t}\mathrm{S}40$の finite model property により次の条件をみたす有限 rooted frame $\mathrm{M}=$上の model が存在する.

$\mathrm{O}\models\square A(p),$$(\rho\in \mathrm{v}\mathrm{a}\mathrm{r}(B))$$\mathrm{O}\models\square A(C),$,,$(\square C\in \mathrm{S}\mathrm{u}\mathrm{b}(B))$$0\# B$$\bullet$$A(_{\sim}p)$$\leq$

が $P^{\neg}P$ のとき.

の拡張となる最小の同値関係を$\sim$とする.

$M’=M/\sim$

とおき,$a\in M$ の属する同値類を「$\overline{a}R$$b\Leftrightarrow\exists c,$$d$$\overline{a}$で表す. このとき,$H$を($a\sim c,$ $b\sim d$ かつ $cRd$)

により定める.

claim

$R’$

は $M’$ 上の擬順序であり,$\mathrm{M}’=(M’,$ $=,$ $R’\rangle$

上の付値$\models^{j}$を$\overline{a}\models’p\Leftrightarrow a\models p$により定義できる. また,$a\models D$$C\in \mathrm{S}\mathrm{u}\mathrm{b}(B)$

if and only if

に対し,$\overline{a}\models’D$が成立する.
となることを用いれば, $a\sim b$ ならはが well-defined でが成立することが確かめられる. これより

$a\leq b$

かつ $b\models P$ ならば $a\models P^{\neg}p$ より$a\models p$

if and only if$b\models p$$a\models P$$\models’$

あることが導かれる.
$D$が口 C の形のときを示す.

が成立することに注意すると,により, $b\models’C$ となり$\overline{a}R^{j}\overline{b}$$a\models’\square C$$\bullet$$A(p)$とする.
ならばが成立する.

$a\models\square C$$a\models\square C\mathrm{v}\neg\square c$$b\models\square C$$(a,$$b)|a,$$b$は$\leq$

を含む最小の同値関係をに関し極大で$\sim$とする.

$c\models\square C$となるので特に $b\models C$ . 帰納法の仮定

が $\neg p\vee\neg\neg p$ のとき.

{

より $a\sim c$ ならば$\exists c(c\leq a,$ $c\leq b)$}

81$M^{f}=M/\sim$

とおき,$a\in M$ の属する同値類を$\overline{a}R^{\Gamma}b\Leftrightarrow\exists c,$$d$$\overline{a}$で表す. このとき, 鳶を( $a\sim C,$ $b\sim d$ かつ $cRd$)

により定める. このとき先ほどと同様に, つぎが成立する.

claim

$H$

は $M’$ 上の擬順序であり,$\mathrm{M}’=\langle M’, =, R’\rangle$

上の付値$\models’$を$\overline{a}\models’p\Leftrightarrow a\models p$により定義できる. また,$a\models D$$C\in \mathrm{S}\mathrm{u}\mathrm{b}(B)$

if and only if

に対し,$\overline{a}\models’D$が成立する.

Q.E.D.
Corollary 18$A(p)$$\square p\vee\square \neg\square p$,を次の論理式のいつれかとする.

$\coprod_{\neg\square p\vee}\square \neg\square \neg\square p_{t}$$p\vee\neg p,$ $\neg p\neg\neg p$$p\supset\square p,$$\square p\vee\neg\square p$,.

このとき, intS4 ロ $+A(p)$ は finite model p\mbox{\boldmath $\pi$}pe 吻を持ち, Craig の補間定理が成立する.

Remark Luppi [3] は直観主義様相論理で Craig の補間定理が成立するための必要十分条件をで Craig の補間定理が成立することを示し
および代数的に与え,$\mathrm{i}\mathrm{n}\mathrm{t}\mathrm{S}4\square +\square p\square \neg\square p$$\mathrm{i}\mathrm{n}\mathrm{t}\mathrm{S}4_{\mathrm{O}}$

ている.

4

cut-free systemsと次の推論規則を付け加えた体系として定義でき, しかもこの体系は cut-丘 oe であることが知られている. ([1])$\mathrm{S}4\mathrm{c}_{\mathrm{r}2}=\mathrm{s}4+\square (\square (p\supset\square p)\supset p)\supset p$$\square \Gamma,$(Grz$arrow\square$)$\square$($A\supset$は$\mathrm{L}\mathrm{K}$に$(\square arrow)$

ロ A)\rightarrow A$\overline{\square \Gammaarrow\square A}$

この体系の cut-elimination の司 mtactical な証明は, LJ にえた体系にも適用できることがわかる. したがって次が得られた.

$(\square arrow)$と$(\mathrm{G}\mathrm{r}\mathrm{z}arrow\square )$

を付け加

82

Lemma 19
えた体系は$A\zeta p$) をとすれば LJ にの cut-free な形式化である.

$(\square arrow)$$\square (\square (p\supset\square p)\supset p)\supset p$$\mathrm{i}\mathrm{n}\mathrm{t}\mathrm{S}40+A(p)$と$(\mathrm{G}\mathrm{r}\mathrm{z}arrow\square )$を付け加Lemma 20.

$\mathrm{i}\mathrm{n}\mathrm{t}\mathrm{S}4_{\mathrm{O}}+A(p)\vdash B\Leftrightarrow \mathrm{i}\mathrm{n}\mathrm{t}\mathrm{S}40\vdash( \wedge \square A(C))\supset B$$\mathrm{o}c\epsilon \mathrm{s}_{\mathrm{u}\mathrm{b}(B})$

を示せば十分である.
の cut-free な証明を考えると次のような弱い形の subformula property が成立することが証明の構成に関する帰納法で示せる.

Proof.)$\Rightarrow$$B$

証明中に positive に現れる
したがって, 証明中のの形の論理式は $B$ に positive に現れる.

$\square C$の principal formula$(\mathrm{G}\mathrm{r}\mathrm{z}arrow\square )$$\square C$

はすべて $B$ の subformula である. これより補題の主張がただちに従う.

Lemma 21 (cf. [8])ぞれ$\bullet$$\bullet$$\mathrm{G}\mathrm{i}\mathrm{n}\mathrm{t}\mathrm{S}4\mathrm{O}$$\mathrm{L}$を$\mathrm{i}\mathrm{n}\mathrm{t}\mathrm{S}4\square$

Q.E.D.

の normal dension とする.

$V(\mathrm{L})$および$V’(\mathrm{L})$はそれに次の形の始式を付け加えて得られる体系とする.

$V(\mathrm{L})\Gammaarrow$, ただし$V’(\mathrm{L})\square \Gammaarrow$$\mathrm{L}\vdash\Gammaarrow$

, ただし

,

$\mathrm{L}\vdash\square \Gammaarrow$.

このときこれらの体系は cut-Fee となる.

Proof.)

志村 [8] のLemma 22$A(p)$$\mathrm{i}\mathrm{n}\mathrm{t}\mathrm{S}4_{\mathrm{O}}\vdash($$V(\mathrm{L})$をの証明と同様.

$\square \neg\neg p\supset\neg\neg\square p$$\square A(C))\supset\neg B$$\wedge$

Q.E.D.

とする.

$\mathrm{S}4\vdash\neg B$

ならば.

ロ C\epsilon Sub(B)Proof.)
よる.

S4 に対する cut-free な体系における$\neg B$の cut-free な証明の構成に関する帰納法に

Q.E.D.

Lemma 23$\mathrm{i}\mathrm{n}\mathrm{t}\mathrm{S}40\vdash$$A(p)$を$\square \neg\square \neg p\supset\neg\square \neg\square p$$( \wedge \square A(C))\supset\neg B$とする.

$\mathrm{I}\mathrm{r}\mathrm{i}\mathrm{v}\vdash\neg\square B$

ならば.

$\mathrm{o}c\in s_{\mathrm{u}}\mathrm{b}(B)$Proof.)
による.

Thiv に対する cut-&ae な体系におけるCorollary 24$\neg\square B$の$\mathrm{c}\mathrm{u}\mathrm{t}_{-}\Re_{\mathrm{e}}$な証明の構成に関する帰納法

Q.E.D.

83,$V(\mathrm{S}4)=\mathrm{i}\mathrm{n}\mathrm{t}\mathrm{S}40+\square \neg\neg p\supset\neg\neg\square p$$V’(\mathrm{I}\mathrm{r}\mathrm{i}\mathrm{v})=\mathrm{i}\mathrm{n}\mathrm{t}\mathrm{S}4\square +\square \neg\square \neg p\supset\neg\square \neg\square p$

であり,

.

) を

$A\mathrm{C}\mathrm{P}$$\square \neg\neg p\supset\neg\neg\square p$,$\square$\neg 口\neg p\supset \neg$\square$p\neg $\square$のいつれかとすれば$\mathrm{i}\mathrm{n}\mathrm{t}\mathrm{S}40+A(p)\vdash B\Leftrightarrow \mathrm{i}\mathrm{n}\mathrm{t}\mathrm{S}4_{\mathrm{O}}\vdash( \wedge \square A(\square C))\supset B$.

$\mathrm{o}c\epsilon \mathrm{s}\mathrm{u}\mathrm{b}(B)$が成立する.

Corollary 25$A(p)$を$\square (\square (p\supset\square p)\supset p)\supset p,$$\square \neg\neg p\supset\neg\neg\coprod p,$$\square \neg\square \neg p\supset\neg\square \neg\square p$のいつれかとすれば intS40+A(P) では Cfuig の補間定理が成立する.

Proof.)

前原の方法 (cf. 志村 [8]) によるものと Lemma 20 と Corolary 24 によるものがある.

Q.E.D.

5

補足
直観主義論理上では◇は他の論理記号や様相$\square$とは独立である.

か含んでいないが, ◇も含む場合にはどうなるだろうか.
$\mathrm{G}\mathrm{i}\mathrm{n}\mathrm{t}\mathrm{S}4_{\mathrm{O}}$に◇に関する推論を加える場合は$\Gammaarrow A$$\Gammaarrow\text{◇}A$$A,$ $\square \Gammaarrow\text{◇}\Delta$◇ A,$\square \Gammaarrow\text{◇}\Delta$を考えるのは自然であろう.
方$\mathrm{G}’\mathrm{i}\mathrm{n}\mathrm{t}\mathrm{S}4_{\mathrm{O}}$に対しては$\mathrm{i}\mathrm{n}\mathrm{t}\mathrm{S}40$

は様相として$\square$し84$\Gammaarrow\Delta,$$\Gammaarrow\Delta$

$A$

, ◇A

$A,$ $\square \Gammaarrow\text{◇}\Delta$◇ A,$\square \Gammaarrow\text{◇}\Delta$が考えられる. 共に cut-ehhmination は成立するが, 前者の体系では$\text{◇}(p\mathrm{v}q)\supset\text{◇_{}p}\mathrm{v}\text{◇}q$は証明できないのに対し, 後者では証明可能であるからこれらは真に異なる強さを持つ.

前者には前原の方法が適用できるので次が容易に示せる.

Fact 26$\mathrm{i}\mathrm{n}\mathrm{t}\mathrm{S}4\mathrm{O}+P\supset\text{◇}p+\text{◇◇}p\supset\text{◇}p+\square (p\supset q)\supset(\text{◇_{}p}\supset\text{◇}q)$

では Craig の補間定理が成り立つ.

しかし, この論理に対する semantics は知られていないので, この論理に対し, 3 節の丘 ltration

method が適用できるかどうかは筆者にはわからない.
型の体系には前原の方法が適用できる
逆に後者に対しては semantics は知られているが,かどうか不明なため、 この論理で Craig の補間定理が成立するかどうかはわからない.
. また,◇ P\supset ◇ P のような公理をつけ加えた場合にどうなるかは興味深い問題と思われる.
$\mathrm{L}\mathrm{J}’$$\square$$\square$

参考文献[1] Avron, A., On modal systems having
Logic 49 (1984), 935-942.

$af\dot{\mathrm{y}}thmeti_{Ca\iota}$

interpretations, Journal of Symbolic[.2] Bori\v{c}i\v{c}, B.R., Interpolahon theorem for inbuitionistic , Bull. Sect. of Logic, Pol. Acad.
$s\mathit{4}$Sci. 20 (1991), 2-6.

property of some inhuitionistic modal[3] Luppi, C., On the
Mathematicsl Logic, 35 (1996), 173-189.
$inter\mathrm{p}_{\mathit{0}}lau_{\mathit{0}}n$[4] Maehara, S., Eine Darstellung der intuitionistischen
Mathematical Journal 7 (1954), 45-64.
[5] Maksimova, LL., Interpolation in nomal modal
Neklass Logiki (1987), 40-56, 153.

$lo\dot{\varphi}k$$\iota_{w}icS$, Archives for$\iota_{w}icS$

und der Klassischen, Nagoya, (in Russian) Mat. Issled. 98

85[6] Ono, H., On some intuitionistic modal$l\dot{\wp}c\theta$, Puplications of R.I.M.S. 13 (1977), 55-67.

[7] Prawitz, D., and Malmn\"as, P.-E., A survey of some connections bebveen classical, intuitionistic and minimal logics, in: Contribution to mathematical logic (ed. by A.Schmitt,-Holland(1968), 215-229.
),
K.Sch\"utte and$\mathrm{H}.-\mathrm{J}.\mathrm{T}\mathrm{h}\mathrm{i}\mathrm{e}\mathrm{l}\mathrm{e}$$\mathrm{N}\mathrm{o}\mathrm{r}\mathrm{t}\mathrm{h}$[8] Shimura, T., Cut-fiee systems for some modal
matical Logic 26 (1992), 39-65.

$lo\dot{\wp}CS$

containing$s\mathit{4}$, Reports on Mathe