>>621
弱ケーニッヒとACやBPIでは非構成さのレベルが全然違うだろｗ

弱ケーニッヒを使う程度ならまだ具体的と言うこともできるわけで、
むしろ完全性定理の（通常の）証明で
ヘンキンの補題「証明不可能なら反例モデルが存在する」から
背理法により証明の存在を導く部分の方が問題だろう。