ラヨ数
この定義文は、ルール違反を避けるために以下のように置き換えられた。
数の正式の定義は以下の二階論理の式で定義された関数Sat([φ(x1)],s)を利用する。[φ]はゲーデルコード化(ゲーデル数によるナンバリング)された式であり、sは代入変数である。
{任意の(コード化された)式 [ψ] と任意の代入変数 t (R( [ψ],t) ↔ ( ([ψ] = `x_i ∈ x_j' ∧ t(x_1) ∈ t(x_j)) ∨ ([ψ] = `x_i = x_j' ∧ t(x_1) = t(x_j)) ∨ ([ψ] = `(∼θ)' ∧ ∼R([θ],t)) ∨ ([ψ] = `(θ∧ξ)' ∧ R([θ],t) ∧ R([ξ],t)) ∨ ([ψ] = `∃x_i (θ)' と、いくつかのtのxi変形t', R([θ],t')) )} →
この式Sat([φ(x1)],s)を用いて、ラヨ数は次の様に定義された。
厳密には、公理系が明示的に書かれていないため、定義が不完全である。