ここから、ハイパー論理に
前回の弱ＡＣ関連の話題として登場した
ＺＦ外で、ＺＦ＋弱ＡＣ内の新命題（論理式）
（∃ｘ）ψ（ｘ）・・・（１）
ですが。
今更、
「そんなものが必ずあるという保証は？」
なんぞというレベルの懐疑を抱くようでは話にならないの。
弱ＡＣはＺＦから独立なので、少なくとも、ＺＦ外でＺＦ＋弱ＡＣ内の閉論理式
Ψ
があるわけで。
Ψが（１）の形式になるかどうかの保証を気にするのでしょうが。
そういうレベルの話じゃないのよ、あの抽象化伏線は。
Ψは閉論理式だから、少なくとも（１）か
（∀ｘ）ψ（ｘ）・・・（２）
のどちらかの形式的表現になるはずですが。