「形式言語」と「形式体系」の区別がついていないことも混乱の元のように思われるので
付け焼刃の知識で説明すると、形式言語は表現可能な式(記号列)を定める。
ただし、形式言語だけでは式の真偽を判定(証明)することはできない。
形式体系は形式言語に加えて公理や推論規則を含んでおり、
形式体系が十分強力であれば式の真偽を証明できる。
ラヨ関数の定義では、形式言語としてのFOSTを用いており、
ラヨ関数を定義する(値を定める)ための形式体系は非常に強いものでなくてはならない。
もし形式言語FOSTの中でラヨ関数の定義式を表すことができるのならば、
FOST'の形式言語としての強さは、FOSTと変わらないことになる。
FOST'を用いればFOSTの式と同値な式をより短く表せることがあるので、
FOST'のラヨ関数はFOSTのラヨ関数より若干大きくなるが、劇的な変化にはならないはずである。

もう一つの疑問は、ラヨ関数を定義できる十分強力な形式体系として
「自然な」ものが本当に一意に定まるのかということである。
例えば、連続体仮説は現代数学の標準的な公理系で真偽を決定できず、
連続体仮説を真とする公理系も偽とする公理系も作れるそうだが、
ラヨ数についてもその値が異なるような複数の「自然な」公理系が作れてしまわないかと疑問に思う。
これは素人が考えてもどうしようもないので専門家に任せるしかなさそうだ。
"Big Number Duel"でgoogle検索しても23件しか出てこないので、
ラヨ数について複数の専門家による十分な検証はされていない気もする。