でるたいーた氏のこのツイート を見て考えてみたところ, 解の存在性が$\ZFC$独立な関数方程式を作れたので紹介します.
まず関数方程式を定義します.
関数方程式とは, (何らかの)$1$変数の関数記号$f_1, \ldots, f_m$, 実定数, 加減乗算, $\sigma$, 不等号を用いた閉論理式のことである.
特に, $$\forall v_1\cdots\forall v_n(F(v_1, \ldots, v_n)=0)$$
という形式($v_1, \ldots, v_n$は何らかの変数)の関数方程式を正規形とよぶ. ここで, $F$は実定数, $v_1, \ldots, v_n$, $1$変数の関数記号$f_1, \ldots, f_m$, 加減乗算, $\sigma$を用いたを用いた項とする.
また, 関数記号$f_1, \ldots, f_m$を用いた関数方程式$\Phi$に対して, $\Phi$を($(\R; +^{\R}, \cdot^\R, \ldots, f_1^\R, \ldots, f_m^\R)$が)充足するような関数$f_1^\R, \ldots, f_m^\R:\R\to\R$を$\Phi$の解とよぶ.
また, 関数方程式に登場する関数記号の種類数$n$を用いて, その関数方程式を$n$関数関数方程式などとよぶ.
本記事では以下を示します.
解が存在することが$\ZFC$独立である正規形の$1$関数関数方程式が存在する.
証明の概略としては, 以下のような言い換えを行います(各用語は後ほど定義します).
正規形の$1$関数関数方程式
$\leftrightarrow$非負正規形の(多関数)関数方程式
$\leftrightarrow$関数記号からなる有限理論
$\leftrightarrow$一般の有限理論
なお, 本記事では最後まで具体的に対応を構築しましたが, 補題4あたりからMRDPに投げるということもできると思います(と言ったらそれまでですが, 本記事の構成のほうが具体的ではあります).
まず, 今回興味があるのは解の存在性だけなので, 以下によって同値性を導入します(ここだけの用語です).
関数方程式$\Phi, \Psi$が可解同値であるとは, $\Phi$に解が存在することと$\Psi$に解が存在することが$\ZFC$において同値であることである. 可解同値性を$\sim$で表す.
$\ZFC$で解の(非)存在性が示せる関数方程式はすべて可解同値です. したがって, 興味があるのは解の存在性が$\ZFC$独立な関数方程式のみです.
関数方程式を可解同値な関数方程式にとりかえて, 正規形を作り出すことを考えます.
関数記号$f_1, \ldots, f_m$についての
$$\forall v_1\cdots\forall v_n(v_1\ge0\land\cdots\land v_n\ge0)\to(F(v_1, \ldots, v_n)=0)\land\bigwedge_{i=1}^m\forall x(x\ge0\to f_i(x)\ge0)$$
という形式の関数方程式を, 非負正規形であるという.
ここで, $F$は非負の実定数, $v_1, \ldots, v_n$, $1$変数の関数記号$f_1, \ldots, f_m$, 加算, 乗算, $\sigma$, $\sigma'$, $(x, y)\mapsto(x-y)^2$を用いた項とする.
非負正規形の関数方程式の解であるかは各関数の定義域$\R$における非負の部分の値にしか依存しません.
まず, 何度か使うツールとして基本的な補題を示します.
(resp. 非負)正規形の関数方程式$\Phi, \Psi$に対して, $\Phi\land\Psi, \Phi\lor\Psi$はいずれも(resp. 非負)正規形の関数方程式に可解同値である.
正規形の場合を示す.
$\Phi\equiv\forall \bar xF(\bar x)=0, \Psi\equiv\forall \bar yG(\bar y)=0$とおくと,
$$\Phi\land\Psi\sim\forall\bar x\forall\bar y(F(\bar x)^2+F(\bar y)^2=0)$$
$$\Phi\lor\Psi\sim\forall\bar x\forall\bar y(F(\bar x)F(\bar y)=0)$$
である. 非負正規形の場合も同様.
流れのところで書いたように, はじめのステップとして非負正規形の関数方程式と正規形の$1$関数関数方程式を結びつけます. ここで非負性は複数の関数を束ねるのに必要な技術的な仮定です.
$\Phi$を非負正規形の関数方程式とする. このとき, $\Phi$はある正規形の$1$関数関数方程式に可解同値である.
$$\Phi\equiv\forall v_1\cdots\forall v_n(v_1\ge0\land\cdots\land v_n\ge0)\to(F(v_1, \ldots, v_n)=0)\land\bigwedge_{i=1}^m\forall x(x\ge0\to f_i(x)\ge0)$$を関数$f_1, \dots, f_m$についての関数方程式とする.
$f$を関数記号とする.
$i=1, \dots, m$に対して$g_i:\R\to\R$を$x\mapsto f(i+\sigma'(x))$の略記とする. さらに, $F$における各$f_i$を$g_i$に書き換えたものを$\tilde F$とする.
このとき, 補題2より関数方程式
$$\forall v_1\cdots\forall v_n(\tilde F(v_1, \ldots, v_n)=0)\land\forall x(f(x)=f(x+n)^2)$$
は正規形であるが, これは$\Phi$に可解同値である. 実際, 解$(f_i)_{i=1}^m$に対して, $[i, i+1)$上で$f_i\mid_{\R_{\ge0}}\circ(\sigma'\mid_{\R_{\ge0}})^{-1}(x-i)\ge0$を返し, $[1, m+1)$以外にも非負に拡張させた関数$f$が対応する.
ここから一般の理論と関数方程式を結びつけていきます. ここでネックになるのは多変数関数を扱うために定義域$M$とその直積$M^k$の間に定義可能な全単射を作るということです. $M$が$\R$とかの場合は難しいので, $\N$の場合に関数方程式で帰着させます.
基本となるのは次の補題です.
$\mathbb N$の定義関数を(負の部分の差を除いて)唯一の解にもつ, 非負正規形の$1$関数関数方程式が存在する.
$(f(x+1)-f(x))^2=0, (f(0)-1)^2=0, f(\sigma(x)/2)=0, f(1+\sigma'(x)/2)=0$
の論理積に補題2を適用する. この解は, 非負の範囲で周期$1$をもち, $f(0)=1$, $(0, 1)$上で$0$となる.
いよいよ両者を結びつける命題を示します. 3つのステップに分けて少しずつ所望の関数方程式に近づけていきます.
任意の有限$(g_1, \ldots, g_n)$-理論$T$に対して, ある正規形の$1$関数関数方程式$\Phi$が存在し, $T$が可算モデルをもつことと, $\Phi$が解をもつことが同値である.
ここで, 各$g_i$は任意アリティの関数記号である.
まず, $\Phi$として一般の関数方程式を認めた場合に主張を示す.
$\chin$を関数記号とする. また, 以下$\chin$の定め方は補題4および
$$\forall x(\chin(-x^2-1)=0\land\chin(-\sigma(x))=0)$$
の論理積とする. したがって, これをみたす解は$\N$の定義関数のみである.
いま, 任意の正整数$k$に対して加減乗算で記述できる全単射$\eta_k:\N^k\to\N$が存在する.
これを用いて, 各$T$に属する論理式を以下のように書き換えたものを$\tilde T$とおく.
| 書き換え前 | 書き換え後 |
|---|---|
| $g_i(t_1, \ldots, t_k)$ | $f_i(\eta_k(t_1, \ldots, t_k))$ |
| $\forall x\phi(x)$ | $\forall x(\chin(x)=1\to\psi(x))$ |
| $\exists x\phi(x)$ | $\forall x(\chin(x)=1\land\psi(x))$ |
このとき, 関数方程式
$$\Phi\equiv\left(\bigwedge_{\phi\in\tilde T}\phi\right)\land\left(\bigwedge_{i=1}^n\forall x(\chin(x)=0\lor \chin(f_i(x))=1)\right)\land(\chin\text{を定める関数方程式})$$
が解をもつことと$T$が可算モデルをもつことは同値である. 実際, $f_i(\N)\subset\N$であり, 関数$f_i\mid_\N\circ\eta_k:\N^k\to\N$を$g_i$の$\N\subset\R$における解釈とすることで$T$の可算モデルを与える. 逆も, $T$の可算モデルの台集合と$\N$の全単射を適当にひとつ固定することで, 所望の関数を得る.
次に, $\Phi$と可解同値な非負正規形の関数方程式を構成する. 論理学の一般論より, $\bigwedge_{\phi\in\tilde T}\phi$は
$$\bigwedge_{\phi\in\tilde T}\phi\equiv Q_1v_1\cdots Q_mv_m\psi$$
という形式であるとして一般性を失わない. ここで, $Q_i$は$\forall$または$\exists$であり特に$Q_1=\forall$, $\psi$は量化子を含まない論理式である.
まず, $\psi$は原始論理式またはその否定のブール和として記述できる. 各原始論理式は$t=s$(いずれも$(g_1, \ldots, g_n)$-項)という形式であるが, これは$(t-s)^2=0$に書き換える. その否定は$\exists x((x(t-s)^2-1)^2=0)$とすることで, $\psi$を否定を含まない論理式にする. さらに,
$$\R \vDash \forall t\forall s(t=0\land s=0)\leftrightarrow (t^2+s^2=0)$$
$$\R \vDash \forall t\forall s(t=0\lor s=0)\leftrightarrow (ts=0)$$
であるので, $\psi$は$t=0$という形式であるとしてよい.
ここで, $Q_i$が$\exists$であるような各$i$に対して, 関数記号$p_i$をとる. また, $k_i\in\N$を$Q_j=\forall$なる$j=1, \dots, i-1$の個数とする.
このようなすべての$i$に対して, $\psi$に登場する$v_i$を$p_i(\eta_{k_i}(v_1, \dots))$(ただし引数は$Q_j=\forall$なる$j=1, \dots, i-1$についての$v_j$たちをとる;$\bigwedge_{\phi\in\tilde T}\phi$の充足性に影響するのは$\vDash\chin(v_1)=1\land\cdots$の場合のみに注意せよ)に置き換えたものを$\tilde\psi$とおく.
このとき,
\begin{align*}
\tilde\Phi\equiv&\forall v_*\forall v_*\cdots\forall v_*\tilde\psi\\
\land&\left(\bigwedge_{i=1}^n\forall x(\chin(x)=0\lor (\chin(f_i(x))-1)^2=0)\right)\\
\land&(\chin\text{を定める関数方程式})
\end{align*}
($*$は$Q_i=\forall$なる$i$を動く)は以下をみたす:
補題3より, Step2で構成した非負正規形の関数方程式は, 正規形の$1$関数関数方程式と可解同値である.
これである程度自在に関数方程式を作れることが分かったので, あとは理論側で準備すればよいです.
次に都合のよい理論を構成します.
有限モデルを持たない任意の有限理論$T$に対して, ある有限$(g_1, \ldots, g_n)$-理論$T'$が存在し, $T$と$T'$がそれぞれ可算モデルを持つことが同値である.
ここで, 各$g_i$は任意アリティの関数記号である.
$T$の言語を$L$とする. $L$は有限集合として一般性を失わず, また$T$において異なることが証明できる$L$の定数記号$c_0, c_1$が存在するとしてよい.
$T'$を構成しよう.
$L$に登場する関数記号はそのまま, 定数記号は$1$変数関数および定値写像であるという公理を$(g_1, \ldots, g_n)$および$T'$に加えればよい. $n$変数述語記号$R$は$n+1$変数関数記号であって$c_0$または$c_1$に値をとり, $R$の定義関数となるようなものを加えればよい.
これらの記号について$T$の各公理に対応する公理を$T'$に加えることで構成される.
有限モデルを持たない有限個の論理式からなる$1$階述語論理の理論であって, 可算モデルを持つことが$\ZFC$独立であるものが存在する.
完全性定理, 健全性定理, Löwenheim-Skolemの定理より, $T$が可算モデルを持つことと$\text{Con}(T)$は同値である.
例えばフォン・ノイマン=ベルナイス=ゲーデル集合論($\mathsf{NBG}$)は$\ZFC$の保存拡大なので([1]), Gödelの不完全性定理より$\text{Con}(\mathsf{NBG})$は$\ZFC$独立である.
ここまでの結果を合わせることで, 主定理を得ることができます.
解が存在することが$\ZFC$独立である正規形の$1$関数関数方程式が存在する.
定理5, 補題6, 補題7より従う.
$\R$上の関数方程式はかなり表現力があると思います. 特に, $\N$の定義関数を解に持つ関数方程式が作れることがクリティカルに効いていて, 理論的に扱うのには構造が複雑すぎるという気持ちになります.
以下は今後の課題です: