戸田山『論理学をつくる』は終盤で様相論理について簡潔な解説をしている。そこで「対応理論」という用語がでてくる（p.315）。様相論理の式とそれが妥当になるフレームの到達可能性関係の対応をあつかう理論、といったところだろうか。そこで著者が紹介しているのは、例えば
- □P→□□P
という式（図式）が妥当になるフレームは推移的だとか
- □P→P
が妥当になるフレームは反射的だとかそういったことである。
正直なところ、これを証明するのはかなり簡単なので、この程度のことで「理論」とか大げさだなと思っていた。しかし、次のような例をみると、「理論」というだけのありがたみを感じられる。
- ◊h□iA → □j◊kA
□iというのは□をi個並べるということ。◊についても同様である。こういう一般的な図式に対して、それが妥当になるフレームの到達可能性関係を一般的な形で定式化できるとエレガントである。答えは
- wRhv ＆wRju ⇒ ∃x (vRix＆ uRkx)
となる。そういう定理がレモンとスコットにより証明されている*1。ちょっとばかり確認してみよう。例えば、最初に提示した
- □P→□□P
は、h = 0, i = 1, j = 2, k = 0の場合の特殊ケースとみなせる。これの到達可能性関係は
- wR0v ＆wR2u ⇒ ∃x (vR1x＆ uR0x)
ただし、w, v, uには全称量化がかかっている。これはつまり
- w = v ＆ ∃y(wRy ＆ yRu) ⇒ ∃x (vRx＆ u = x)
ということであり、さらに簡略化すると
- ∃y(wRy ＆ yRu) ⇒ wRu
となる。これはRが推移的だと言っているので、正しい結果が得られたことになる。□P→Pについても同じことが言える。
