多様相論理GLPとBeklemishevの虫

\(\newcommand{\card}[1]{\mathrm{card}(#1)} \newcommand{\Pow}[1]{\mathcal{P}(#1)} \newcommand{\Powfin}[1]{\mathcal{P}_\mathrm{fin}(#1)} \newcommand{\inepsilon}{\,\epsilon\,} \newcommand{\notinepsilon}{\not\!\epsilon\,} \newcommand{\range}[1]{\mathrm{ran}(#1)} \newcommand{\field}[1]{\mathrm{field}(#1)} \newcommand{\Nat}{\mathbb{N}} \newcommand{\rnk}[1]{\mathrm{rnk}\mleft(#1\mright)} \newcommand{\numeral}[1]{\underline{#1}} \newcommand{\standardmodel}{\mathbb{N}} \newcommand{\otyp}[1]{\mathrm{otyp}(#1)} \newcommand{\conjunct}{\bigwedge} \newcommand{\disjunct}{\bigvee} \newcommand{\struc}[1]{\left\langle #1\right\rangle} \newcommand{\sequence}[1]{\left\langle #1\right\rangle} \newcommand{\autid}{\mathsf{Aut}(\mathsf{ID})_0} \newcommand{\Cl}[2]{\mathsf{Cl}_{#1}(#2)} \newcommand{\IT}[2]{\mathsf{IT}_{#1}(#2)} \newcommand{\ITs}{(\mathsf{ITA})} \newcommand{\SIGMA}{\mathbf{\Sigma}} \newcommand{\PI}{\mathbf{\Pi}} \newcommand{\DELTA}{\mathbf{\Delta}} \newcommand{\club}[1]{\mathrm{Club}_{#1}} \newcommand{\stat}[1]{\mathrm{Stat}_{#1}} \newcommand{\nonstat}[1]{\mathrm{NS}_{#1}} \newcommand{\Rat}{\mathbb{Q}} \newcommand{\Real}{\mathbb{R}} \newcommand{\cut}{(\mathsf{cut})} \newcommand{\RobR}{\mathsf{R}} \newcommand{\RobQ}{\mathsf{Q}} \newcommand{\PAmin}{\mathsf{PA}^{-}} \newcommand{\IOpen}{\mathsf{IOpen}} \newcommand{\IDeltazero}{\mathsf{I}\Delta_0} \newcommand{\PA}{\mathsf{PA}} \newcommand{\KP}{\mathsf{KP}} \newcommand{\KPomega}{\mathsf{KP}\omega} \newcommand{\ZFC}{\mathsf{ZFC}} \newcommand{\code}[1]{\ulcorner #1\urcorner} \newcommand{\numdot}[1]{\dot{#1}} \newcommand{\prf}[3]{\mathsf{Prf}_{#1}\mleft( #2, #3 \mright)} \newcommand{\prov}[2]{\mathsf{Pr}_{#1}(#2)} \newcommand{\bprov}[1]{\mathord{\Box}_{#1}} \newcommand{\drov}[1]{\mathord{\Diamond}_{#1}} \newcommand{\consis}[1]{\mathsf{Con}(#1)} \newcommand{\nprov}[3]{#1\text{-}\mathsf{Pr}_{#2}(#3)} \newcommand{\nbprov}[2]{[#1]_{#2}} \newcommand{\ndprov}[2]{\langle #1\rangle_{#2}} \newcommand{\nconsis}[2]{#1\text{-}\mathsf{Con}(#2)} \newcommand{\lrfn}[1]{\mathsf{Rfn}(#1)} \newcommand{\urfn}[1]{\mathsf{RFN}(#1)} \newcommand{\plrfn}[2]{\mathsf{Rfn}_{#1}(#2)} \newcommand{\purfn}[2]{\mathsf{RFN}_{#1}(#2)} \newcommand{\necessary}{\mathord{\Box}} \newcommand{\possible}{\mathord{\Diamond}} \newcommand{\nnecessary}[1]{[#1]} \newcommand{\npossible}[1]{\langle #1\rangle} \newcommand{\GLP}{\mathbf{GLP}}\)

Beklemishevの虫は多様相論理の算術的解釈に背景を持つ。以下ではその視点から解説していく。

定義1.1 多様相論理\(\GLP\)

\(\GLP\)の論理式は以下のように帰納的に定義される。 \(\bot\)は論理式である。 \(\top\)は論理式である。 命題変数\(p,q,r,\ldots\)は論理式である。 論理式\(\varphi,\psi\)に対し\(\varphi\to\psi\)は論理式である。 論理式\(\varphi\)、自然数\(n\)に対し\(\nnecessary{n}\varphi\)は論理式である。 また論理式の略記を以下のように定める。 \(\lnot\varphi:\equiv\varphi\to\bot\) \(\varphi\lor\psi:\equiv\lnot\varphi\to\psi\) \(\varphi\land\psi:\equiv\lnot(\varphi\to\lnot\psi)\) \(\varphi\leftrightarrow\psi:\equiv(\varphi\to\psi)\land(\psi\to\varphi)\) \(\npossible{n}\varphi:\equiv\lnot\nnecessary{n}\lnot\varphi\) \(\GLP\)の公理は以下からなる。 全ての命題論理於いて真な論理式 各\(n\in\Nat\)に対し以下を公理として持つ。 \(\nnecessary{n}(\varphi\to\psi)\to\nnecessary{n}\varphi\to\nnecessary{n}\psi\)。 \(\nnecessary{n}(\nnecessary{n}\varphi\to\varphi)\to\nnecessary{n}\varphi\)。 \(\nnecessary{n}\varphi\to\nnecessary{n}\nnecessary{n}\varphi\)。 \(m\leq n\)に対し\(\nnecessary{m}\varphi\to\nnecessary{n}\varphi\)である。 \(m<n\)に対し\(\npossible{m}\to\nnecessary{n}\npossible{m}\varphi\)である。 \(\GLP\)の推論規則はモーダスポネンスのみとする。 \(\GLP\vdash\varphi\leftrightarrow\psi\)ならば\(\GLP\vdash\nnecessary{n}\varphi\leftrightarrow\nnecessary{n}\psi\)であるから論理式の間の同値関係\(\varphi\equiv\psi\)を\(\GLP\vdash\varphi\leftrightarrow\psi\)で定め、商を取ることができ、その商によって導入される代数構造をJaparidze代数という。