>第一ZFCとかを前提とするというのは、それはそれで(1とは別の意味で)
>危うい前提での議論なのでは、とか感じてしまいます。
なんか、ZFC内で表現した算術の命題の選択公理を使う証明は、
選択公理を使わない証明に書き直すことが出来る、
とかそういう結果があるとかないとか

というかメタレベルで、そんなに厳密に公理的な議論する必要無いんじゃないですかね?
必要が無いというか、しても意味が無いというか、
少なくとも形式的にやらないにしても、どういう議論の仕方をしたら矛盾に陥りやすいか、
どういう議論の仕方なら一応安心できるかってのは今ではかなり分かってるわけですし
(どうやったら「絶対に」矛盾しないかってのは分かってないですけど
それは公理論的な集合論でも同じですね)

「そんなこと本に書いてあったっけ」ってのはなんか疑問の持ち方がおかしいと思いますけどね