ラヨ関数を定義できる形式体系がどのようなものか考えてみた。

ラヨ関数の定義に出てくる式Sat([φ],s)の真偽が判定できなければラヨ関数は定義できない。
Sat([φ],s)の真偽を判定するには、FOSTの式すべての真偽を判定(証明)できなければならない。
FOSTは自然数論を含んでいるので、ゲーデルの不完全性定理の証明から考えると
「自然数論を含む帰納的に記述できる無矛盾な公理系」をどのように選んでも、
その公理系では証明も反証もできない命題がFOSTに含まれていると思われる。
矛盾した公理系でラヨ関数を定義するのは無意味であり、
自然数論を含まない公理系で自然数の関数であるラヨ関数は定義できないので、
帰納的に記述できない公理系でしかラヨ関数は定義できないことになる。

帰納的に記述できない「自然な」公理系が選べて、ラヨ関数は一意に定まるのだろうか。