risk = nil;

今回は，過去を示す演算子である．引き続き教科書 ¹から例をとる．ただ，記号が特殊でテキストでは書きづらいので，記号は，KAOS教科書にあるものを使う．このあたりの記号の豊富さが，絵文字に仲間意識を感じるように，魅力的なところかもしれない．

「前(Previous)」演算子　●

未来の○に対応する．

(σ, j) ⊧ ● p iff    j>0 and (σ, j – 1) ⊧ p.

下記は「前」演算子の真理値である．ゼロから１に変化する場所を示す．「次」演算子も合わせて示している．なお，真になるためには，j>0の条件があるので，最初（j=0）では，無条件で偽になる．

「以前(Has-alwasy-been)」演算子 ■

(σ, j) ⊧ ■p   iff   (σ, k) ⊧ p for all k, 0 ≤ k ≤ j.

未来の□に対応する．「ずっと，pであった」ということを意味する．

以下に例を示す．

時刻2までは，式が成立している．

「かつて(Once)」演算子 ◆

(σ, j) ⊧ ◆p   iff   (σ, k) ⊧ p for some k, 0 ≤ k ≤ j.

「pで真あったことがある」という意味である．

「以来(Since)」S 演算子

(σ, j) ⊧ p S q   iff   0 ≤ k ≤ j となる k があり，(σ, k) ⊧ q が成り立つ．かつ，k < i ≤ j で，全ての i において (σ, i) ⊧ p.

かつて q に出会った．それ以降は p であった．q p … p という列を考えている．

次は，(x ≤ 6) S (x = 3) の例である

「（よわい）以来(Back-to)」B 演算子

(σ, j) ⊧ p B q   iff   (σ, j) ⊧ p S q  or  (σ, j) ⊧ ■p.

基本的には，Sと同じである．ただ，q に出会わなくても良い．その場合は，p が続いていた．

ちょうど，U に対するWと同様の関係にある．

次の真理を考える．(x ≠ 4)  B  (x = 6)

前半の真の部分は，■ p による．後半は，p S q が機能している．

他にも過去の演算子はあるが，基本的なものは上記になる．

(nil)

演算子の続きである．

「以後(henceforth)」演算子 □

(σ, j) ⊧ □p   iff   (σ, k) ⊧ p for all k ≥ j.

これといった訳語がない．「ずっと p である」といった意味になる．

この記号は，様相論理では，「必然」であった．必然ということばは，「〜して当然」という含意もあり，その解釈はさまざまであった．時相論理における□には，そういうややこしさはない．

次に，□ (x > 3) の真理値表を考えてみる．今回も，時間経過を示す j と x を混同しないようにというのが注意である．

時間 7 以降も，x は 4 より大きいとしている．

「いつか(eventually)」演算子 ◇

(σ, j) ⊧ ◇p   iff   (σ, k) ⊧ p for some k ≥ j.

「いつかは p になる」という意味である．

様相論理では，「可能」という意味であった．

「まで」U (until) 演算子

(σ, j) ⊧ p U q   iff   k ≥ j となる k があり，(σ, k) ⊧ q が成り立つ．かつ，全ての i において，j ≤ i < k で，(σ, i) ⊧ p.

どこかで q に出会う．それまで p が続く．p … p q という列を考えている．

次は，(3 ≤ x ≤ 5) U ( x = 6) の例である

「（よわい）まで」W (Unless, Waiting-for) 演算子

(σ, j) ⊧ p W q   iff    (σ, j) ⊧ p U q or (σ, j) ⊧ □p.

基本的には，Uと同じである．ただ，q に出会わなくても良い．その場合は，p が続く．

訳語が難しく，ここでは，「（よわい）まで」とした．

次の真理を考える．[(3 ≤ x ≤ 5)  ∨  (x ≥ 8)] W ( x = 6)

表をおいかけるのは面倒だが，対象とする命題の真偽が，時間によって変わるのが実感できる．

なお，ここまでにでてきた演算子は，お気づきの通り，「未来」に関するものである．次回は，幾つかの例をみてから，簡単に過去の時制演算子を見ることにしたい．