GL.3の完全性
わかりやすい証明が
G. Boolos; "The Logic of Provability"
のp.174に書いてある．
大雑把に言う
$ \bf GL.3
のカノニカルモデル
$ M_\mathbf{GL.3}
は推移的かつpw.connectedになる（非反射的にはならない）
$ \mathbf{GL.3} \nvdash A
から
$ M_\mathbf{GL.3},x \nvDash A
が言える．この
$ x
を起点として，
$ M_\mathbf{GL.3}
から適当に点を抽出して
$ M
を作る．
つまり
Selective Filtration
（用語合ってるのか？）っぽいことをする．