解釈によって値が変わらないことの証明　まだ完璧でないけど

1階述語論理で考える。
解釈によって関数fの値が変わらないというのは、任意の引数ｘ、任意の閉論理式σにつき、ある自然数bが存在し、
(σ→f(x)=b)∧(¬σ→f(x)=b)
となることをいう。(等号に関する公理をふまえておく)
コンパクト性により無限個の論理式については考えなくて良い。

ペアノの公理系を含む無矛盾で帰納的公理化可能な理論T（と論理公理）
T上で任意のxにつきf(x)の値が決まるとする。このようなTは計算可能であれば存在する。
すると、
それぞれのxにつき、σをTから独立した任意の閉論理式、bを適当な自然数すると、
T⊦σ→f(x)=b　かつ　T⊦¬σ→f(x)=b
よって
T⊦(σ→f(x)=b)∧(¬σ→f(x)=b)

Tが存在する時点で証明がほぼ終わるしこっちが証明の本懐となる

・・・もしかして、ある人の後者関数sが別のある人のビジービーバー関数かもしれない、
というレベルの話？