a proof of distributivity from symmetry
□, ◇ の単調性
- if p → q then □p → □q
- if p → q then ◇p → ◇q
と、axiom B に相当する公理の組*1
- p → ◇□p
- ◇□p → p
から intuitionistic reasoning で distributivity law ◇(p∨q) → ◇p∨◇q が導けることに気がついたので証明をメモ。
- p → □◇p from the axiom
- □◇p → □(◇p ∨ ◇q) from monotonicity of □
- p → □(◇p ∨ ◇q) by transitivity
- q → □(◇p ∨ ◇q) in a similar way
- p∨q → □(◇p ∨ ◇q) from 3 and 4
- ◇(p∨q) → ◇□(◇p ∨ ◇q) from monotonicity of ◇
- ◇□(◇p ∨ ◇q) → ◇p∨◇q from the axiom
- ◇(p∨q) → ◇p∨◇q by transitivity using 6, 7
直観主義様相論理に関する論文では distributivity は公理に入ってるか証明できないかの二つのパターンしか見たことがありません。必要なら明示的に公理として追加するのが普通で、そうしなければ出ないように思っていたので、B のような有名な公理から出てくるのはやや意外です。
an observation
結論の式には □ がないけど証明の途中では □ を使っています。これは何を意味するのだろうと思って証明をもう一度見てみたら、◇ と □ が adjoint になるんですね。だから left adjoint であるところの ◇ は colimit の一例である ∨ を保存する、ということ。
それに気付いてから証明の後半をもう一度見ると、よくある unit/counit から hom-set definition を導く方法と同じことをやっていますね。
