時間的球体系 $ T による充足条件の表現

この節では、時間的球体系$^T によって、条件節と帰結節の基準時が一致しない場合で も、さらにその前件に作用が含まれる場合でも、反事実条件文の充足条件が肌理細かく柔 軟に表現できることを示す。そのために、集合論的な二項関係に対する標準的な演算の記 法を導入する。一般に二項関係R⊆X×Y に対し、A(⊆X)のRによる像 image とは

R[A] ={y∈B | ∃x ∈A (xRy)}

である。A が単元集合{x} ^の場合、R[{x}](= {y ∈ B | xRy})をR[x] と略記する。ま た、一般に二項関係 R ⊆ X ×Y とR^′ ⊆ Y ×Z に対し、RとR^′ の合成 composition とは、

R◦R^′ ={(x, z)∈X ×Z | ∃y∈Y (xRy &yRz)}

により定められる演算である。このときX の部分集合A, Y の部分集合B について、A 上の同一性関係, B上の同一性関係をそれぞれ

Id_A ={(x, x) | x∈A}, Id_B ={(y, y) | y ∈B}, とすれば、二項関係R⊆X×Y に対し、

IdA◦R ={(x, y)∈X×Y | x ∈A & xRy}, R◦IdB ={(x, y)∈X×Y | xRy & y ∈B} が定義できる。したがって、この意味でA◦R, R◦Bを

A◦R =def IdA◦R, R◦B =def R◦IdB

と定義することができる。つまり、関係合成は、この意味で二項関係と集合の間にも自然 に拡張できる。

以上の集合論的二項関係及び集合に対する演算と、すでに構成した時点tにおける時間 的球体系$^T_t により、まず、時点tにおける前件に作用を含まないタイプの反事実条件文 (CS)の充足条件は、

M, g, t|=↓x.P(⟨R⁻₀¹⟩x &

(a) F(⟨R⁻₁¹⟩x & φ& F⟨R⁻₂¹⟩x) &

(b) G(⟨R⁻¹₁ ⟩x→(φ→G(⟨R⁻¹₂ ⟩x→ψ)))) iff

∃t^′ ∈R0[t] (St^′ ∈$^∗_t &

(a) St^′∩(≤ ◦(R1[t]∩JφK)◦ ≤)[t^′]̸=∅ and (b) S_t′∩(≤ ◦(R₁[t]∩JφK)◦ ≤)[t^′]⊆R₂[t]∩JψK)

となる。また、時点tにおける前件に作用を含むタイプの反事実条件文(CSA) の充足条 件は、

M, g, t|=↓x.P(⟨R⁻₀¹⟩x &

(a) F(⟨R⁻₁¹⟩x & ⟨a⟩F⟨R⁻₂¹⟩x) &

(b) G(⟨R⁻¹₁ ⟩x→[a]G(⟨R⁻¹₂ ⟩x→ψ))) iff

∃t^′ ∈R0[t] (St^′ ∈$^∗_t &

(a) St^′∩(≤ ◦R1[t]◦(−→^a )◦ ≤)[t^′]̸=∅ and (b) S_t′∩(≤ ◦R₁[t]◦(−→^a )◦ ≤)[t^′]⊆R₂[t]∩JψK

となる。そしてこれらの時間的球体系$^T_t を用いた充足条件を視覚化したものが以下で ある。

図2.13

ここで、前章で焦点を当てた作用を含む反事実条件文

「水ボタンを押さなかったらコーヒーが買えたのに」

の強い形式化

⟨water⁻¹⟩tt∧[water⁻¹]⟨coffee⟩tt · · ·(MS)

を振り返ってみよう。上の(MS)にも、隠伏的な基準時として、水のボタンを押す前の分 岐時点R0、条件節の基準時R1、帰結節の基準時R2 が存在しているはずである。これら を補って(MS)を再形式化したものが、以下の(MS’)である（ただし、トートロジーを表 すHMLの記法ttはHTLCF の記法⊤^{に書き換えてある）。}

(MS’)

↓x.⟨water⁻¹⟩(⟨R⁻¹₀ ⟩x &

(a) ⟨water⟩(⟨R⁻₁¹⟩x & ⟨water⁻¹⟩F⟨R⁻₂¹⟩x) &

(b) [water](⟨R⁻₁¹⟩x→[water⁻¹]G(⟨R⁻₂¹⟩x→ ⟨coffee⟩⊤))

これを(CSA)の図式 (CSA)

↓x.P(⟨R⁻₀¹⟩x &

(a) F(⟨R⁻₁¹⟩x & ⟨a⟩F⟨R⁻₂¹⟩x) &

(b) G(⟨R⁻₁¹⟩x→[a]G(⟨R⁻₂¹⟩x→ψ)))

と照らし合わせればわかるように、(CSA)で分岐時点R₀に遡行する過去時制演算子P の 役割を(MS’)では⟨water⁻¹⟩^が、(CSA)で条件節の基準時R₁に到達するための未来時制 演算子F, Gの役割を(MS’)では⟨water⟩,[water]が、(CSA)で帰結節の基準時R2に到達 するための作用a^{と未来時制演算子}F, G^の役割を(MS’)^では再び⟨water⁻¹⟩,[water⁻¹] が、それぞれ担っている。これにより、(CSA) でP, F, G の表現する時点の不定性が、

(MS’)では作用waterの遡行時点、完了時点として特定されていることがわかる。

このことを踏まえ、(MS’)の読みはこうである。「水ボタンを押す前の分岐時点R0 に 戻って、そこから始まる分岐時間モデルを考える。すると(a) そこで水ボタンを押してし まった基準時R1 があり、そこで再び水ボタンを押す前に戻ってそれ以降の基準時として R2 がある。さらに (b) 水ボタンを押してしまった基準時R1 が来たとき、そこで再び水 ボタンを押す前に戻ることができれば、それ以降に基準時R₂ が来たとき、そこではまだ コーヒーを買うことが可能であった。」

こうして(MS)を(MS’)で再形式化することにより、前章で焦点を当てた、その前件に

作用の否定を含む反事実条件文「水ボタンを押さなかったらコーヒーが買えたのに」の充 足条件もまた、以下のように時間的球体系によって与えられることになる。

M, g, t|=↓x.⟨water⁻¹⟩(⟨R⁻₀¹⟩x &

(a) ⟨water⟩(⟨R⁻₁¹⟩x & ⟨water⁻¹⟩F⟨R⁻₂¹⟩x) &

(b) [water](⟨R⁻¹₁ ⟩x→[water⁻¹]G(⟨R⁻¹₂ ⟩x→ ⟨coffee⟩⊤)) iff

∃t^′ ∈(R0∩(^water−→⁻¹))[t] (St^′ ∈$^∗_t &

(a) St^′∩((^water−→)◦R1[t]◦(^water−

−→1)◦ ≤)[t^′]̸=∅ and (b) S_t′∩((^water−→)◦R₁[t]◦(^water−

−→1)◦ ≤)[t^′]⊆R₂[t]∩J⟨coffee⟩⊤K ここでは、充足条件の先頭部分∃t^′ ∈(R₀∩(^water−

−→1))[t] (S_t′ ∈$^∗_t · · ·^{に示されるように、}

過去の分岐時点R0に当たるt^′、つまり、考察される反事実的状況の範囲を決定するイン デクスとなる時点 t^′ が、具体的な作用の遡行^water−→⁻¹ によって指定されていることがわ かる。

2.2.10 HTL

の推論上の効用 ——((A ∨ B) € C) → ((A € C ) ∧