>>619
>選択公理を仮定した証明の中である選択関数φの存在を推論してよいが、
>証明の結論にφが含まれてはならない。これは述語論理の推論規則の基本ですよ。

それは存在消去の推論規則の話ね
「∃xP(x)　と、P(c)からBへの証明から、Bが証明できる
その際、Bにcが”自由変項として”あらわれてはならない」

整列定理の中にあらかじめφが現れていて、
それが選択公理で存在が保障されたφである
という言い方はもちろんできない

一方、整列定理の証明では集合Sの整列順序を構成している
上記のP(c)からBを導く箇所がそれにあたる

Sの整列順序の構成には
Sの空でない部分集合P(S)-{{}}から
その要素を選ぶ選択関数φを用いている

S0＝S　s0＝φ(S0)
S1＝S0-{s0} s1＝φ(S1)
S2＝S1-{s1} s2＝φ(S2)
…
Sω=∩(n∈ω)Sn sn＝φ(Sω)
…

この系列によって、Sの全ての要素が、順序数に対応づけられ
Sが集合であるかぎりこの対応の上限となる順序数が存在する

実にシンプルな推論

整列定理が存在を主張する整列順序について
「何の情報もない」というならそれはウソである
明らかに証明の中で具体的にφを使って構成しているから

ただφ自体は、選択公理という仮定によって誕生しているから
これについては何の情報もない　そういうこと