ブラケット原理 (bracket principle) はFernández-DuqueとReyes[1]によって与えられたベクレミシェフの虫の拡張であり,\(\mathsf{ATR}_0\) の独立命題となる.この独立命題は非常に速く増大する関数を誘導する.

定義

ブラケット原理の定理を述べるために,用語を定義する.

定義

文字列の集合 \(\mathbb{W}_\mathtt{()}\) を以下のように帰納的に定義する.

  1. \(\top\in\mathbb{W}_\mathtt{()}\) .
  2. \(a,b\in\mathbb{W}_\mathtt{()}\) ならば \(\mathtt{(}a\mathtt{)}b\in\mathbb{W}_\mathtt{()}\) である.

また以下のように \(\top\) に関しての略記を用いる.

  1. \(\mathtt{(}\top\mathtt{)}a\) の代わりに \(\mathtt{()}a\) と表す.
  2. \(\mathtt{(}a_1\mathtt{)}\cdots \mathtt{(}a_k\mathtt{)}\top\) の代わりに \(\mathtt{(}a_1\mathtt{)}\cdots \mathtt{(}a_k\mathtt{)}\) と表す.
定義

論理式(文字列)の集合 \(\mathbb{F}_\mathtt{()}\) を以下のように帰納的に定義する.

  1. \(\top\in\mathbb{F}_\mathtt{()}\) .
  2. \(p\in\mathbb{F}_\mathtt{()}\) .
  3. \(\varphi,\psi\in\mathbb{F}_\mathtt{()}\) ならば \(\varphi\land\psi\in\mathbb{F}_\mathtt{()}\) である.
  4. \(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\) を帰納的に定義する.

  1. \(\varphi\in\mathbb{F}_\mathtt{()}\) に対し \(\varphi\vdash\varphi\) である.
  2. \(\varphi\in\mathbb{F}_\mathtt{()}\) に対し \(\varphi\vdash\top\) である.
  3. \(\varphi,\psi\in\mathbb{F}_\mathtt{()}\) に対し \(\varphi\land\psi\vdash\varphi\) である.
  4. \(\varphi,\psi\in\mathbb{F}_\mathtt{()}\) に対し \(\varphi\land\psi\vdash\psi\) である.
  5. \(\varphi,\psi,\chi\in\mathbb{F}_\mathtt{()}\) に対し \(\varphi\vdash\psi\) かつ \(\varphi\vdash\chi\) ならば \(\varphi\vdash\psi\land\chi\) である.
  6. \(\varphi,\psi,\chi\in\mathbb{F}_\mathtt{()}\) に対し \(\varphi\vdash\psi\) かつ \(\psi\vdash\chi\) ならば \(\varphi\vdash\chi\) である.
  7. \(\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\) である.
  8. \(\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\) である.
  9. \(\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)\) である.
  10. \(a,b\in\mathbb{W}_\mathtt{()}\) に対し \(a\vdash \mathtt{()}b\) または \(a\vdash b\) であるとき \(b\trianglelefteq a\) である.
  11. \(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\}\) を帰納的に定義する.

  1. \(\top\{n\}=\top\) とする.
  2. \(a_1=\top\) であるとき \(\mathtt{(}a_1\mathtt{)}\cdots\mathtt{(}a_k\mathtt{)}\{n\}=\mathtt{(}a_2\mathtt{)}\cdots\mathtt{(}a_k\mathtt{)}\) とする.
  3. もし \(\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|\!\}\) を以下のように帰納的に定める.

  1. \(a\{\!|0|\!\}:=a\) .
  2. \(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\) より速く増大する.

出典

  1. Fernández-Duque, David, and Eduardo Hermo Reyes. "Deducibility and Independence in Beklemishev's Autonomous Provability Calculus." arXiv preprint arXiv:2008.13445 (2020).
特に記載のない限り、コミュニティのコンテンツはCC-BY-SAライセンスの下で利用可能です。