忍者ブログ
記述を自己完結にするために前回説明できなかったシーケント規則のルールを補足しておく。

まずは、前回も登場した、論理演算子にかかわらない規則を再掲する。なお、太字で書かれたヘディングはルール名、ルールのあとのカッコ内はそのルールの略称を表す。

薄め:$\cfrac{\Gamma \rightarrow \Theta}{\mathfrak{D},\Gamma \rightarrow \Theta} (WL) \quad \cfrac{\Gamma \rightarrow \Theta}{\Gamma \rightarrow \Theta,\mathfrak{D}} (WR)$

縮約:$\cfrac{\mathfrak{D},\mathfrak{D},\Gamma \rightarrow \Theta}{\mathfrak{D},\Gamma \rightarrow \Theta} (CL) \quad \cfrac{\Gamma \rightarrow \Theta,\mathfrak{D},\mathfrak{D}}{\Gamma \rightarrow \Theta,\mathfrak{D}} (CR)$

交換:$\cfrac{\Delta,\mathfrak{D},\mathfrak{E},\Gamma \rightarrow \Theta}{\Delta,\mathfrak{E},\mathfrak{D},\Gamma \rightarrow \Theta} (IL) \quad \cfrac{\Gamma \rightarrow \Theta,\mathfrak{E},\mathfrak{D},\Lambda}{\Gamma \rightarrow \Theta,\mathfrak{D},\mathfrak{E},\Lambda} (IR)$

カット:$\cfrac{\Gamma \rightarrow \Theta, \mathfrak{D} \quad \mathfrak{D}, \Delta \rightarrow \Lambda}{\Gamma, \Delta \rightarrow \Theta, \Lambda} (Cut)$

さて、以下に、前回も登場した論理演算子 $\supset$ のそれも含めて、すべての論理演算子の導入ルールをあげる。

否定:$\cfrac{\Gamma \rightarrow \Theta,\mathfrak{A}}{\neg\mathfrak{A},\Gamma \rightarrow \Theta} (\neg L) \quad \cfrac{\mathfrak{A},\Gamma \rightarrow \Theta}{\Gamma \rightarrow \Theta, \neg \mathfrak{A}} (\neg R)$

連言:
$\cfrac{\mathfrak{A},\Gamma \rightarrow \Theta}{\mathfrak{A}\&\mathfrak{B},\Gamma \rightarrow \Theta} (\&L_1) \cfrac{\mathfrak{B},\Gamma \rightarrow \Theta}{\mathfrak{A}\&\mathfrak{B},\Gamma \rightarrow \Theta} (\&L_2) \cfrac{\Gamma \rightarrow \Theta,\mathfrak{A} \quad \Gamma \rightarrow \Theta,\mathfrak{B}}{\Gamma \rightarrow \Theta,\mathfrak{A}\&\mathfrak{B}} (\&R)$

選言:
$\cfrac{\mathfrak{A},\Gamma \rightarrow \Theta \quad \mathfrak{B},\Gamma \rightarrow \Theta}{\mathfrak{A}\vee\mathfrak{B},\Gamma \rightarrow \Theta} (\vee L) \cfrac{\Gamma \rightarrow \Theta,\mathfrak{A}}{\Gamma \rightarrow \Theta,\mathfrak{A}\vee\mathfrak{B}} (\vee R_1) \cfrac{\Gamma \rightarrow \Theta,\mathfrak{B}}{\Gamma \rightarrow \Theta,\mathfrak{A}\vee\mathfrak{B}} (\vee R_2)$

含意:$\cfrac{\Gamma \rightarrow \Theta,\mathfrak{A} \quad \mathfrak{B},\Delta \rightarrow \Lambda}{\mathfrak{A}\supset\mathfrak{B},\Gamma,\Delta \rightarrow \Theta,\Lambda} (\supset L) \quad \cfrac{\mathfrak{A},\Gamma \rightarrow \Theta,\mathfrak{B}}{\Gamma \rightarrow \Theta,\mathfrak{A}\supset\mathfrak{B}} (\supset R)$

これらのルールを用いて、前回示した排中律と同様に、矛盾律は以下のように示される。

$\cfrac{\cfrac{\cfrac{\cfrac{\cfrac{\cfrac{A \rightarrow A}{\neg A,A \rightarrow}}{A \& \neg A,A \rightarrow}}{A,A \& \neg A \rightarrow}}{A \& \neg A,A \& \neg A \rightarrow}}{A \& \neg A \rightarrow}}{\rightarrow \neg (A \& \neg A)}$

(使われているルールは上から $\neg L, \& L, IL, \& L, CL, \neg R$ となる)

演習:$A \supset B \equiv \neg A \vee B$ を示せ。

量化子はつぎのように導入される。

全称:$\cfrac{\mathfrak{Fa},\Gamma \rightarrow \Theta}{\forall \mathfrak{x}\mathfrak{Fx},\Gamma \rightarrow \Theta} (\forall L) \quad \cfrac{\Gamma \rightarrow \Theta,\mathfrak{Fa}}{\Gamma \rightarrow \Theta, \forall \mathfrak{xFx}} (\forall R)$

存在:$\cfrac{\mathfrak{Fa},\Gamma \rightarrow \Theta}{\exists \mathfrak{x}\mathfrak{Fx},\Gamma \rightarrow \Theta} (\exists L) \quad \cfrac{\Gamma \rightarrow \Theta,\mathfrak{Fa}}{\Gamma \rightarrow \Theta, \exists \mathfrak{xFx}} (\exists R)$

ここで、$\forall R, \exists L$ にかんしてはとくべつな注意が必要である。つまり、それらにおいて $\mathfrak{x}$ で束縛される $\mathfrak{a}$ は下段に現れてはならない。なぜか? この禁を破るとつぎのような導出ができてしまうからである。

$\cfrac{\cfrac{\cfrac{\mathfrak{Fa} \rightarrow \mathfrak{Fa}}{\exists \mathfrak{xFx} \rightarrow \mathfrak{Fa}}}{\exists \mathfrak{xFx} \rightarrow \forall \mathfrak{xFx}}}{\rightarrow \exists \mathfrak{xFx} \supset \forall \mathfrak{xFx}}$

この終式によれば「(あるドメイン内の)何かが $\mathfrak{F}$ であれば、(そのドメイン内の)すべてが $\mathfrak{F}$ である(ということがいっぱんに成り立つ)」ということになるが、言うまでもなくそんなことは(いっぱんには)成り立たない。こんなことになってしまったのはひとえに、一段目の $\exists L$ 適用が上で述べた禁を犯しているからである。「$\forall R, \exists L$ において $\forall, \exists$ で束縛される変数は下段に現れてはならない」というルールを「固有変数条件 eigenvariable condition」という。

量化子導入を含むシーケント計算の例:

$\cfrac{\cfrac{\cfrac{\cfrac{\cfrac{\mathfrak{Fa} \rightarrow \mathfrak{Fa}}{\mathfrak{Fa} \rightarrow \exists \mathfrak{xFx}}}{\rightarrow \exists \mathfrak{xFx}, \neg \mathfrak{Fa}}}{\rightarrow \exists \mathfrak{xFx}, \forall \mathfrak{x}\neg\mathfrak{Fx}}}{\neg \forall \mathfrak{x}\neg\mathfrak{Fx} \rightarrow \exists \mathfrak{xFx}}}{\rightarrow \neg \forall \mathfrak{x}\neg\mathfrak{Fx} \supset \exists \mathfrak{xFx}}$

(使われているルールは上から $\exists R, \neg R, \forall R, \neg L, \supset R$ となる)

演習:$\rightarrow \exists \mathfrak{xFx} \supset \neg \forall \mathfrak{x} \neg \mathfrak{Fx}$ を導け。
PR
この記事にコメントする
お名前
メールアドレス
URL
コメント
カレンダー
02 2017/03 04
S M T W T F S
1 2 3 4
5 6 7 8 9 10 11
12 13 15 16 17 18
19 20 22 23 24 25
26 27 28 29 30 31
最新トラックバック
メール
ブログ作成者(はやし)に直接訴えたいことがある、という場合は、下のアドレスにメールをどうぞ。

thayashi#ucalgary.ca
(#を@に置換してください)

ブログ内検索
Google
WWW を検索 このブログ内を検索

はやしのブログ内で紹介された
 書籍の検索はこちら
 音盤の検索はこちら
ランダムおすすめ
(忍者ブログに引越してから、うまくうごかなくなってしまいました。いつか、直します)
Randombook
このブログで紹介したことのある本をランダム表示。
Randomusic
このブログで紹介したことのある音をランダム表示。
自分がらみのリンク
はやしのブログ書籍一覧
このブログで言及された書籍の一覧。
はやしのブログ音盤一覧
このブログで言及された音盤の一覧。
最近のおすすめ本
最近のおすすめ音

Copyright © [ はやしのブログ ]
No right reserved except those which belong to someone else.
Special Template : 忍者ブログ de テンプレート and ブログアクセスアップ
Special Thanks : 忍者ブログ
Commercial message : [PR]