ラベル付きシークエント計算から正規様相論理で非反射性が特徴づけられないことを証明する
proof
非反射性を特徴づけるラベル付きシークエント計算のルール$ \text{(irrefl)} = \frac{}{xRx \Rightarrow}は定義できる．
しかし実際には任意の$ \varphiについて$ \vdash_\mathbf{G3K} \varphi \iff \vdash_{\mathbf{G3K} + \text{(irrefl)}} \varphiが成り立つ．
メモ
この証明は純粋に構文論的なアプローチで行ける．
メモ