(ページの作成:「\(\newcommand{\card}[1]{\mathrm{card}(#1)} \newcommand{\Pow}[1]{\mathcal{P}(#1)} \newcommand{\Powfin}[1]{\mathcal{P}_\mathrm{fin}(#1)} \newcommand{\inepsilon}{\,\epsilon\…」) タグ: ソースの編集 |
編集の要約なし タグ: ソースの編集 |
||
37行目: | 37行目: | ||
\newcommand{\KPomega}{\mathsf{KP}\omega} |
\newcommand{\KPomega}{\mathsf{KP}\omega} |
||
\newcommand{\ZFC}{\mathsf{ZFC}} |
\newcommand{\ZFC}{\mathsf{ZFC}} |
||
− | \newcommand{\code}[1]{ |
+ | \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の虫は多様相論理の算術的解釈に背景を持つ。以下ではその視点から解説していく。 |
Beklemishevの虫は多様相論理の算術的解釈に背景を持つ。以下ではその視点から解説していく。 |
||
43行目: | 62行目: | ||
{| class=wikitable |
{| class=wikitable |
||
− | ! '''定義1.1''' 様相論理 |
+ | ! '''定義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\nneccesary{n}\lnot\varphi\) |
||
+ | |||
+ | \(\GLP\)の公理は以下からなる。 |
||
+ | # 全ての命題論理於いて真な論理式 |
||
+ | # 各\(n\in\Nat\)に対し以下を公理として持つ。 |
||
+ | ## \(\nneccessary{n}(\varphi\to\psi)\to\nnccessary{n}\varphi\to\nneccessary{n}\psi\)。 |
||
+ | ## \(\nneccessary{n}(\nneccessary{n}\varphi\to\varphi)\to\nneccessary{n}\varphi\)。 |
||
+ | ## \(\nneccessary{n}\varphi\to\nneccessary{n}\nneccessary{n}\varphi\)。 |
||
+ | # \(m\leq n\)に対し\(\nneccessary{m}\varphi\to\nneccessary{n}\varphi\)である。 |
||
+ | # \(m<n\)に対し\(\npossible{m}\to\nneccessary{n}\npossible{m}\varphi\)である。 |
||
+ | |||
+ | \(\GLP\)の推論規則はモーダスポネンスのみとする。 |
||
|} |
|} |
||
[[カテゴリ:ブログ記事]] |
[[カテゴリ:ブログ記事]] |
2021年2月3日 (水) 03:04時点における版
\(\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\)の論理式は以下のように帰納的に定義される。
また論理式の略記を以下のように定める。
\(\GLP\)の公理は以下からなる。
\(\GLP\)の推論規則はモーダスポネンスのみとする。 |