2024.11.01
https://gyazo.com/27cb9de8a99e71da55fd88afc1512d08
メモ
これ初めて知ったんだけど証明方法鮮やかすぎてびっくりした．
非反射性を特徴づけるラベル付きシークエント計算のルール$ \text{(irrefl)}は定義できる．
しかし実際には任意の$ \varphiについて$ \vdash_\mathbf{G3K} \varphi \iff \vdash_{\mathbf{G3K} + \text{(irrefl)}} \varphiが成り立つ．