ラヨ関数の定義で、都合の悪いものはすべて除外されると考えるのは正しいのだろうか。

Sat([φ],s)の定義では、
任意の[ψ],tについてR([ψ],t)が命題ψ(t)と同値になるようなRを考えている。
つまり、∀[ψ],t: ...の部分の式は、
∀[ψ],t: R([ψ],t)⇔ψ(t)　…(＊)
と同値と考えられる。
任意の[ψ],tについて考えるということは、FOSTの任意の命題の真偽を考えるということであり、
ここでは都合の悪い命題を除外して考えることはできない。
もし、FOSTで表現可能だが証明できない命題があれば、Sat([φ],s)の真偽も証明できないと思われる。

Sat([φ(x_1)],s)からRayo(n)を定義するときには、
異なるx_1を持つ変数設定s,tについてSat([φ(x_1)],s), Sat([φ(x_1)],t)が真となるような[φ(x_1)]や
Sat([φ(x_1)],s)が真となる変数設定sが存在しない[φ(x_1)]は一つの数を定義しないとして除外される。
ラヨ数の定義式[φ(x_1)]を10^100文字以内で書いても[φ(x_1)]は一つの数を定義せずに除外されるという根拠は、
[φ(x_1)]が一つの数を定義すれば矛盾するということと思われる。

このとき、FOSTを拡張して神託式を用いた異なるラヨ数の定義式[φ'(x_1)]を書いても、
φ(x_1)とφ'(x_1)が同値である限りSat([φ(x_1)],s)とSat([φ'(x_1)],s)は同値で、
[φ(x_1)]も[φ'(x_1)]も一つの数を定義しないのではないかと思う。(>>43)
神託式であるという理由で[φ'(x_1)]が一つの数(ラヨ数)を定義するというのならば、
φ(x_1)とφ'(x_1)は同値でなく、φ(x_1)はラヨ数の定義式でないことになる。

そもそも、ラヨ数の定義式[φ(x_1)]が一つの数を定義しないというのは、もし(＊)式を満たすRが存在すれば
「ラヨ数=nを満たす自然数nが存在しないか複数存在する」という命題が
ラヨ数を扱う形式体系で証明できるということになり、
ラヨ数は一意に定まらないということにならないのだろうか。
もしそうだとすれば、Rayo(n,L)の定義式が形式言語Lを用いてn文字以内で表せる限り
Rayo(n,L)は一意に定まらないことになってしまう。
ラヨ関数が定義できないのであれば、ラヨ関数の神託式を導入しても機能しないことにも納得がいく。
ただ、本当にラヨ関数が定義できないのかは厳密な議論をしないと分からないだろう。