正の関連性論理R+
Ref
Def
正の否定を含まない関連性論理を$ \bf R^+とする．定義を以下に示す． $ \bf R^+の言語$ \mathscr{L}_\mathbf{R^+}は以下．
外延的な論理演算子$ \land, \lor
外延的とは他の世界を参照せずに真理値が確定するの意．
$ \land,\lorはそれぞれ外延的連言と外延的選言という．
内縁的な論理演算子$ \odot, \to
内延的とは他の世界を参照して真理値が確定するの意．
その他は普通の命題論理と考えよ．論理式などもそれに従う．
$ \mathbf{R^+}フレーム$ \lang W,@,R \rangとは以下を満たす．
$ Wは非空集合で，特に$ @ \in Wとする．
$ Rは$ W上の3項関係とし，以下を満たす
ただし$ w_1 \leq w_2 \iff R@w_1w_2と定義する．
単調性: $ Rw_1w_2w_3かつ$ w_1' \leq w_1なら$ Rw_1'w_2w_3 交換律: $ Rw_1w_2w_3なら$ Rw_2w_1w_3 結合律:$ Rw_1w_2xかつ$ Rxw_3w_4な$ x \in Wが存在するなら，ある$ yが存在して$ Rw_1yw_4かつ$ Rw_2w_3 y $ \bf R^+フレーム$ \mathcal{F} = \lang W,@,R \rang上の$ V_0 \colon W \times \mathrm{Prop} \to 2が以下の，直観主義論理のいわゆる遺伝性を満たすとする． $ V_0(x,p) = 1かつ$ x \leq yのとき$ V_0(y,p) = 1
このとき$ V_0を論理演算子について拡張した付値関数$ V \colon W \times \mathrm{Form} \to 2 を以下のように定める． $ V(w, p) = 1 \iff V_0(w,p) = 1
$ V(w,A \land B) = 1 \iff V(w, A) = 1 ~\&~ V(w,B) = 1
$ V(w, A \lor B) = 1 \iff V(w,A) = 1 ~\text{or}~ V(w, B) = 1
$ V(w, A \odot B) = 1
$ \iff$ R xywなる$ x,yが存在し$ R(x,A) = 1 ~\&~ R(y,B) = 1
$ V(w, A \to B) = 1
$ \iff$ R wxyなる任意の$ x,yにおいて$ R(x,A) = 1 \implies R(y,B) = 1
$ \lang \mathcal{F},V \rangまたは$ \lang W,@,R,V \rangを$ \bf{R^+}モデルという．
$ \mathbf{R}^+モデル$ \mathcal{M} = \lang W,@,R,V \rangについて
ある$ w \in Wで，任意の$ \gamma \in \Gammaで$ V(w,\gamma) = 1にも関わらず$ V(w,A) = 0なものが存在するとき
$ \mathcal{M}は前提$ \Gammaから結論$ Aへの推論に対しての反例モデルという．
$ \Gammaから$ Aへの推論に対しての反例モデルが構成出来ないとき
推論は$ \bf R^+において妥当であり$ \Gamma \vDash_\mathbf{R^+} Aと書く．$ \bf R^+は適宜省略
遺伝性は論理式レベルで成立する．すなわち任意の$ \bf R^+モデル$ \lang W,@,R,V \rangについて
$ V(x,A) = 1かつ$ x \leq yのとき$ V(y,A) = 1
proof
構造についての帰納法を回す．
関連含意$ \toについて．背理法で示す．
$ V(y, A\to B) = 0と仮定する．
$ \iffある$ Ryw_1w_2なる$ w_1,w_2において$ V(w_1,A) = 1だが$ V(w_2,B) = 0となるものが存在する
$ x \leq yだから単調性より$ Rxw_1w_2
$ V(x,A \to B) = 1と$ Rxw_1w_2及び$ V(w_1,A) = 1を踏まえるとこの時必ず$ V(w_2,B) = 1である．よって破綻する．
内延的連言$ \odotについて．
Obsv 1.
以下は$ \bf R^+において妥当な推論である．
1. $ B \to C \vDash (A \to B) \to (A \to C)
2. $ (A \to B) \land (A \to C) \vDash A \to (B \land C)
3. $ A \to B \vDash (B \to C) \to (A \to C)
4. $ (A \to B) \land A \vDash B
5. $ A \odot (B \lor C) \vDash (A \odot B) \lor (A \odot C)
証明は反例モデルが存在すると仮定するとおかしくなることを示せば良い．
逆に，以下は$ \bf R^+において妥当ではない推論である．
1. $ B \nvDash A \to B
2. $ A \nvDash B \to B
証明は反例モデルを実際に構成して見せれば良い．
Thm: 世界$ @の性質
論理式$ A,Bに対し，
$ A \vDash_\mathbf{R^+} B$ \iff任意の$ \mathbf{R^+}モデル$ \lang W,@,R,V \rangで$ V(@, A \to B) = 1
Proof
$ \implies
背理法．$ A \vDash Bとし，ある$ \mathcal{M} = \lang W,@,R,V \rangで$ V(@, A \to B) = 0と仮定するとおかしいことを示す． 1. $ V(@,A \to B)より，$ R(@,y,z)なるある$ y,zで$ V(y,A) = 1かつ$ V(z,B) = 0
2. ところで$ R@yzとは$ y \leq zであったことを思い出せば，$ \leqは遺伝性が成り立ったので$ V(z,A) = 1が成り立つ． 3. すなわち$ V(z,A) = 1かつ$ V(z,B) = 0であるためモデル$ \mathcal{M}とは$ A \vDash Bの反例モデルに他ならない． 4. しかし前提より$ A \vDash Bは反例モデルを持たないはずだったのでおかしい．
$ \impliedby
背理法．任意の$ \mathbf{R^+}モデルで$ V(@, A \to B) = 1とし，$ A \vDash Bの反例モデル$ \mathcal{M} = \lang W,@,R,V \rangが構成可能であると仮定するとおかしいことを示す． 1. $ \mathcal{M}は反例モデルであるので，ある$ x \in Wで$ V(x,A) = 1かつ$ V(x,B) = 0である．
2. $ V(@,A \to B) = 1より$ R@yzな任意の$ y,zで$ V(y,A) = 1 \implies V(z,B) = 1が成り立つ．
3. ここで$ \mathbf{R^+}フレームの冪等性より$ Rxxxであったので2より，$ V(x,A)=1 \implies V(x,B) = 1が成り立つ．
4. 1,3より$ V(x,B) = 0かつ$ V(x,B) = 1となっておかしい．
Remark
$ \impliedbyはともかく$ \impliesは$ @の性質に基づいていることに注意．
Remark
$ A \vDash Aであるため$ V(@,A \to A) = 1である．
すなわち，$ A \to Aといった当然成り立ってほしいクラシカルなトートロジーは世界$ @においては必ず妥当である． この性質より$ @は論理的な世界と呼ばれる．
関連性論理においては任意の世界$ wでこのようなクラシカルなトートロジーが常に成り立つわけではない（Obsv1参照）．すなわち$ V(w, A \to A) = 1ではない世界$ wも有り得る．（不可能世界） Thm: $ \topの導入
論理演算子$ \topについて，$ V(x,\top) = 1 \iff @ \leq xと定義する．このとき
$ A \vDash B \iff \top \vDash A \to B
proof
TODO
memo
演繹定理に類する次のことは$ \mathbf{R^+}では成り立たない．（例として$ A \to Aなど） $ A \vDash B \iff \vDash A \to B
ただし$ \topが真であるような世界では真であると言える．
そしてそのような世界は論理的な世界：すなわち$ @である