>>718
述語論理の完全性定理なら選択公理より少し弱いもので足りる。

選択公理のようなものが必要なことは、
LKの証明図を逆にたどる方法での証明を考えてみよう。
木の存在を要求してるだろう。