時間論理 ( temporal logic )
時間は、通常は、未来に向かう一方向の流れであり、過去、現在、未来という三つの時制を持つと考えられている。
（現象学的に見れば、我々が体験している時間は現在だけであり、この現在はある程度の幅を持っている。
過去は記憶として現在に留まっており、未来は予期として存在している。
直線として思い描かれた時間は、空間化された時間である。）
可能世界を時点（ある瞬間の世界）と考えれば、可能世界（＝時点）の線的な連続として時間の流れを考えることが出来る。
未来と過去を表す記号として
F （in the Future 未来のある時点において）
P （in the Past 過去のある時点において）
を使う。
命題 q を「彼女は結婚する/している（She gets/is married.）」とすると
q :She gets/is married.
Fq : She will get/be married. Pq :She got/was married.
FFq : She will be going to(!) get/be married. PPq :She had gotten/been
married.
FPq :She will have gotten/been married. PFq :She would get/be married.
（日本語の未来「だろう」は本来は推量、過去「だった」は本来は完了の表現であり、それが時間に転用されている。
しかし英語でも過去以前の過去（＝大過去）を過去完了で表現するように、過去と完了は通底している。）
さらに、
G （未来においてずっと It is always Going to be the case that …）
H （過去においてずっと It Has always been the case that …）
Hq : She has been married.
未来に関して、F と G の関係は、「未来のある一点において」と「未来の全ての時点において」という違いを表す。
（過去における、P と H の関係も同じ。）
つまり、述語論理における、存在記号（∃）と全称記号（∀）、あるいは様相論理における、可能性（◇）と必然性（□）に対応する。
Gq≡¬F¬q
Hq≡¬P¬q （ド・モルガンの法則）
現在と過去/未来との関係については、
現在結婚しているならば、過去の全ての時点で、将来いつか結婚することになる訳だから、
（逆に、過去の全ての時点で、将来いつか結婚することになるとしても、それが現在だという訳ではない。
過去に関しても同様。この関係は、述語論理の ∃x∀yRxy⊃∀y∃xRxy に似ている。）
q⊃HFq
q⊃GPq
これらを書き換えると（対偶法則とド・モルガン）、
PGq⊃q
FHq⊃q
問１ 教師として子供に正しい知識を与えなさい。
「家の子は、叱らないと勉強しないんですよ。先生、何か言ってやって下さい。」
「でもね、先生。「叱る」をA,、「勉強する」をB、だとすると、「叱らないと、勉強しない」は「¬A⊃¬B」ってなりますよね。
その対偶命題「B⊃A」は論理的に常に正しいって先生に教わりました。「勉強すると叱られる」んですよね？
だから僕は、論理的に考えて、勉強しないんです！」
最小時間論理
（Priorの時制論理）
公理
１）命題論理のトートロジー
２）G(q⊃r)⊃(Gq⊃Gr)
H(q⊃r)⊃(Hq⊃Hr) （分配法則 □(q⊃r)(□q⊃□r)）
３）q⊃HFq
q⊃GPq （逆）
４）Gq⊃GGq
Hq⊃HHq (様相論理 S4 □q⊃□□q)
推論規則
１）q, q⊃r →r （MP）
２）q→Gq
q→Hq （時間汎化則）
時間の性質
時間の推移性
Gq⊃GGq
この式は対偶法則とド・モルガンによって、FFq⊃Fq と書き換えられるので、こちらを使うと、
左辺のFFq は、未来のある時点tにおいてFqが成り立つ、よって、tより更に未来の時点t' においてqが成り立つと言っている。
このとき、右辺のFq とは、未来のある時点t' においてqが成り立っていること、則ち、現在からt' に直接到達可能なことを示している。
また逆に、現在からt' に直接到達可能でなければ、Fq は成立しない。
FFq Fq q
現時点→t→t'→
従って、この式は、時間の推移性を表現している。
（この逆の式 Fq⊃FFq (=GGq⊃Gq)は、現時点と未来の時点t'との間に別の時点tが存在すること、
つまり時点間に隙間がないこと（dense稠密性）を表現している。）
時間の非分岐性
■q≡q∧Hq∧Gq
◆q≡q∨Pq∨Fq
■は「いつでも、全ての時点において」という意味であり
◆は「いつか、ある時点において」という意味である。
Fq⊃G◆q
Pq⊃H◆q
上の未来に関する式は、未来において時間が一本の直線状に伸びて枝分かれしていなければ成り立つが、
t と t' に枝分かれしていて、例えばtでqが成立し、t' でqが成立しない場合には、
現時点から見て「いつかq」だからFqは成り立つが、「未来の全ての時点でいつかq」ではないからG◆q は成り立たない。
時間の連続性
(Fq∧◆¬q∧■(q⊃Hq))⊃◆((q∧G¬q)∨(¬q∧Hq))
（続く）
時間論理のモデル
<T, ＜, V>
Tは時点の集合
＜は次のような時点間の到達関係
t1＜t1ではない（非反射関係）
t1＜t2 かつ t2＜t3 ならば t1＜t3 （推移関係）
V は次の付値関数
（→は断定記号の代用 t→pは時点tにおいてqが成り立つということ）
(1) t→¬q ⇔ tにおいてq でない
(2) t→q∧r ⇔ t→q かつ t→r
(3) t→q∨r ⇔ t→q または t→r
(4) t→q⊃r ⇔ t→q ならば t→r
(5)Gq ⇔ t＜t' である全ての t' において t'→q
Hq ⇔ t＞t' である全ての t' において t'→q
推移的だが反射的(T □A⊃A)ではないという関係は、様相論理におけるD+S4である。
（続く）