ブラケット原理 (bracket principle) はFernández-DuqueとReyes[1]によって与えられたベクレミシェフの虫の拡張であり，\(\mathsf{ATR}_0\) の独立命題となる．この独立命題は非常に速く増大する関数を誘導する．
定義[]
ブラケット原理の定理を述べるために，用語を定義する．
| 定義
|
|
文字列の集合 \(\mathbb{W}_\mathtt{()}\) を以下のように帰納的に定義する．
- \(\top\in\mathbb{W}_\mathtt{()}\) ．
- \(a,b\in\mathbb{W}_\mathtt{()}\) ならば \(\mathtt{(}a\mathtt{)}b\in\mathbb{W}_\mathtt{()}\) である．
また以下のように \(\top\) に関しての略記を用いる．
- \(\mathtt{(}\top\mathtt{)}a\) の代わりに \(\mathtt{()}a\) と表す．
- \(\mathtt{(}a_1\mathtt{)}\cdots \mathtt{(}a_k\mathtt{)}\top\) の代わりに \(\mathtt{(}a_1\mathtt{)}\cdots \mathtt{(}a_k\mathtt{)}\) と表す．
|
| 定義
|
|
論理式(文字列)の集合 \(\mathbb{F}_\mathtt{()}\) を以下のように帰納的に定義する．
- \(\top\in\mathbb{F}_\mathtt{()}\) ．
- \(p\in\mathbb{F}_\mathtt{()}\) ．
- \(\varphi,\psi\in\mathbb{F}_\mathtt{()}\) ならば \(\varphi\land\psi\in\mathbb{F}_\mathtt{()}\) である．
- \(a\in\mathbb{W}_\mathtt{()},\varphi\in\mathbb{F}_\mathtt{()}\) ならば \(\mathtt{(}a\mathtt{)}\varphi\in\mathbb{F}_\mathtt{()}\) である．
また\(\mathbf{BC}\)の可証性関係 \(\vdash\) と，\(\mathbb{W}_{\mathtt{()}}\) 上の順序 \(\triangleleft,\trianglelefteq\) を帰納的に定義する．
- \(\varphi\in\mathbb{F}_\mathtt{()}\) に対し \(\varphi\vdash\varphi\) である．
- \(\varphi\in\mathbb{F}_\mathtt{()}\) に対し \(\varphi\vdash\top\) である．
- \(\varphi,\psi\in\mathbb{F}_\mathtt{()}\) に対し \(\varphi\land\psi\vdash\varphi\) である．
- \(\varphi,\psi\in\mathbb{F}_\mathtt{()}\) に対し \(\varphi\land\psi\vdash\psi\) である．
- \(\varphi,\psi,\chi\in\mathbb{F}_\mathtt{()}\) に対し \(\varphi\vdash\psi\) かつ \(\varphi\vdash\chi\) ならば \(\varphi\vdash\psi\land\chi\) である．
- \(\varphi,\psi,\chi\in\mathbb{F}_\mathtt{()}\) に対し \(\varphi\vdash\psi\) かつ \(\psi\vdash\chi\) ならば \(\varphi\vdash\chi\) である．
- \(\varphi,\psi\in\mathbb{F}_\mathtt{()},a,b\in\mathbb{W}_\mathtt{()}\) に対し \(\varphi\vdash\psi\) かつ \(b\trianglelefteq a\) ならば \(\mathtt{(}a\mathtt{)}\varphi\vdash\mathtt{(}b\mathtt{)}\psi\) である．
- \(\varphi,\psi\in\mathbb{F}_\mathtt{()},a,b\in\mathbb{W}_\mathtt{()}\) に対し \(\varphi\vdash\psi\) かつ \(b\trianglelefteq a\) ならば \(\mathtt{(}a\mathtt{)}\mathtt{(}b\mathtt{)}\varphi\vdash\mathtt{(}b\mathtt{)}\psi\) である．
- \(\varphi,\psi\in\mathbb{F}_\mathtt{()},a,b\in\mathbb{W}_\mathtt{()}\) に対し \(b\triangleleft a\) ならば \(\mathtt{(}a\mathtt{)}\varphi\land\mathtt{(}b\mathtt{)}\psi\vdash\mathtt{(}a\mathtt{)}(\varphi\land\mathtt{(}b\mathtt{)}\psi)\) である．
- \(a,b\in\mathbb{W}_\mathtt{()}\) に対し \(a\vdash \mathtt{()}b\) または \(a\vdash b\) であるとき \(b\trianglelefteq a\) である．
- \(a,b\in\mathbb{W}_\mathtt{()}\) に対し \(a\vdash \mathtt{()}b\) であるとき \(b\triangleleft a\) である．
|
| 定義
|
|
\(\mathtt{(}a_1\mathtt{)}\cdots\mathtt{(}a_k\mathtt{)}\in\mathbb{W}_\mathtt{()},n\in\mathbb{N}\)に対し基本列 \(a\{n\}\) を帰納的に定義する．
- \(\top\{n\}=\top\) とする．
- \(a_1=\top\) であるとき \(\mathtt{(}a_1\mathtt{)}\cdots\mathtt{(}a_k\mathtt{)}\{n\}=\mathtt{(}a_2\mathtt{)}\cdots\mathtt{(}a_k\mathtt{)}\) とする．
- もし \(\min_{\triangleleft}\{a_1,\ldots,a_k\}\neq a_1\) であるとき \(l\leq k\) を \(a_l\triangleleft a_1\) が成り立つ最小のものとし，そうでなければ \(l=k+1\) とする．今 \(b=\mathtt{(}a_1\{n\}\mathtt{)}\cdots\mathtt{(}a_{l-1}\mathtt{)},c=\mathtt{(}a_l\mathtt{)}\cdots\mathtt{(}a_k\mathtt{)}\) とする．ここで \(c\) が定まらない場合空列として扱う．このとき \(\mathtt{(}a_1\mathtt{)}\cdots\mathtt{(}a_k\mathtt{)}\{n\}=b^{n+1}c\) とする．ここで \(b^0:=\top,b^{n+1}:=bb^n\) とする．
また \(a\in\mathbb{W}_\mathtt{()},i\in\mathbb{N}\) に対し \(a\{\!|i|\!\}\) を以下のように帰納的に定める．
- \(a\{\!|0|\!\}:=a\) ．
- \(a\{\!|n+1|\!\}:=a\{\!|n|\!\}\{n+1\}\) ．
|
| 定理
|
|
任意の \(a\in\mathbb{W}_\mathtt{()}\) に対し ある \(i\in\mathbb{N}\) が存在し \(a\{\!|i|\!\}=\top\) である．
またこれは \(\mathsf{ATR}_0\) で証明できない．特に，\(a_0:=\top,a_1:=\mathtt{()},a_{n+2}:=\mathtt{(((}a_n\mathtt{)))}\) としたとき，\(F(n):=\min\{i\in\mathbb{N}\mid a_n\{\!|i|\!\}=\top\}\) は \(\mathsf{ATR}_0\) の可証全域関数を支配する．すなわち，\(F\) は \(\alpha<\Gamma_0\) に対してヴェブレン関数の基本列による急増加関数 \(f_\alpha\) より速く増大する．
|
出典[]
- ↑ Fernández-Duque, David, and Eduardo Hermo Reyes. "Deducibility and Independence in Beklemishev's Autonomous Provability Calculus." arXiv preprint arXiv:2008.13445 (2020).
