feat(Modal/Kripke): Add Kripke Completeness of Grz.2

[SnO2WMaN]

close #263

[SnO2WMaN]

どう証明すればよいかは分かっているが上手く形式化が出来ていない．忘れないようにメモだけ書いておく．

今 $y_0 = y$ とする．
任意のterminal point $t$ に対して $y_0 \not\prec t$ として矛盾を導く．
このとき $\prec$ の反射性より $y_0$ はterminal pointではない．したがって $y_1 \neq y_0$ が存在して $y_0 \prec y_1$．
前提より $y_1$ もterminal pointではないから同様に $y_1 \prec y_2$ で $y_2 \neq y_1$ が取れる．このとき $y_2 = y_0$ とすると $\prec$ の反対称性より $y_1 = y_0$ が言えてしまいおかしいので $y_2 \neq y_0$ ．
前提より $y_2$ もterminalではないのでやはり $y_2 \prec y_3$ が取れ，同様の議論で $y_3 \neq y_i$ ($i < 3$) であり $y_3$ もterminalではない．
これを繰り返せば $y_0$ から始まる $\prec$-の無限 $\prec$-鎖: $y_0 \prec y_1 \prec \cdots$ が取れて $i \neq j$ なら $y_i \neq y_j$．しかしそもそもフレームは有限なのでこれはありえない．
よってある terminal point $t$ が存在し $y \prec t$．