完全性定理は選択公理（というかそのfragmentの素イデアル定理だったっけ）
に依存するから、完全性定理によりφの証明が存在する、という主張も
ACとかBPIに依存することになる。
だから、この場合、
メタなレベルで本物の論理式を相手にしているのではなくて
φ自体も形式的対象であると考えるか、
或いは（根拠はともかく、）メタレベルで幾ばくかの集合論と選択公理が
成り立っていると仮定する必要がある。