Fandom

巨大数研究 Wiki

コメント0

ペアノ算術とその部分体系

自然数は次の5条件を満たす。

1. 自然数 0 が存在する。
2. 任意の自然数 a にはその後者 (successor)、suc(a) が存在する(suc(a) は a + 1 の "意味")。
3. 0 はいかなる自然数の後者でもない(0 より前の自然数は存在しない)。
4. 異なる自然数は異なる後者を持つ:a ≠ b のとき suc(a) ≠ suc(b) となる。
5. 0 がある性質を満たし、a がある性質を満たせばその後者 suc(a) もその性質を満たすとき、すべての自然数はその性質を満たす。

5 は数学的帰納法

これらの条件を述語論理で表し形式的に扱えるようにする。述語論理による表現を解釈することで構造が生まれる。定数記号、関数記号、述語記号の解釈からなる構造を L-構造とよぶ。(純粋に形式的な表現を言語と言いそれに意味を与える解釈を構造という。)

ペアノ算術の言語

\(\mathcal{M}=(0,s,<,=)\)

ここではあえて関数記号 s を使わない方法で試してみる。

後者関数の公理

\(∀x∃y(u=x\leftrightarrow v=y)\)

2と4を満たすことと同値

0の公理

\(¬∃x(u=x\leftrightarrow v=0)\)

1と3を満たすことと同値

ほかに論理的な公理を採用する。

推論規則についてはまずモダスポーネンスを採用し、一般化に関する推論は徐々に解禁してゆく形で採用してゆくものとする。

関数のエンコードの帰納的な定義

有限個の引数をとる任意の1階の述語φに対し、

\(∀m∀n∀z∀x∃y((f=m\to(u=x\leftrightarrow v=y))∧(f=0\to(u=y\leftrightarrow v=z))\)

\(\land(f=0\to(u=m\leftrightarrow v=n))\to(f=n\to(u=x\leftrightarrow v=z)))\)

ペアノ算術の公理と直接関係しないが、任意の論理的帰結を表すのに必要となる。

f=0 について、任意の m についてある n が存在し \(u=m→v=n\) が成り立つだけであれば、ある \(m'\not= m\) が存在し \((u=m\to v=n)\land(u=m'\to v=n)\) が成り立ってしまい無限ループが発生してしまうことも考えうる。またそのモデルの1階部分は 0 に f を何度か適用させて得られるため、関係 < について推移律が成り立たず自然数の世界にはならない、そして 0 はいかなる数の後者ではないと公理によって保証されているため Z/nZ の世界にもならない。

補足

任意のxについてφ(x)が成り立つならば任意のxについてψ(x)が成り立つ、は、

\(∀xφ(x)→∀xψ(x)\)

紛らわしいので普通は右か左をα変換した形、

\(∀xφ(x)→∀yψ(y)\)

にする、たぶん。この形だと束縛する変数をまとめて頭に持ってくることができる。

\(∀x∀y(φ(x)→ψ(y))\)

任意のxについて、φ(x)が成り立つならばψ(x)が成り立つ、は、

\(∀x(φ(x)→ψ(x))\)

\(\text{IΔ}_0\) で \(\omega\) 、乗法の公理を追加して \(\omega^2\) 、\(\text{IΔ}_0 (exp)\) (初等関数算術)で \(\omega^3\)

\(\text{IΣ}_1\) は・・・

任意の m について、

1.後者に関する公理から普遍例化で

\(∃y(f=0→(u=0\leftrightarrow v=y))\) ;帰納法の φ(0) の証明

2.仮定

\(∃y(f=m\to (u=m\leftrightarrow v=y))\)

3.存在例化で

\(f=m→(u=m\leftrightarrow v=b)\)

4.後者に関する公理から普遍例化で

\(∃y(f=0→(u=b\leftrightarrow v=y))\)

5.4に存在例化で

\(f=0→(u=b\leftrightarrow v=c)\)

6.後者に関する公理から普遍例化で

\(∃y(f=0→(u=m\leftrightarrow v=y))\)

7.6に存在例化で

\(f=0→(u=m\leftrightarrow v=n)\)

8.3,5,7から

\((f=m→(u=m\leftrightarrow v=b))∧(f=0→(u=b\leftrightarrow v=c))∧(f=0\to (u=m\leftrightarrow v=n))\)

9.関数のエンコードの定義にいろいろ例化

\((f=m→(u=m\leftrightarrow v=b))∧(f=0→(u=b\leftrightarrow v=c))∧(f=0\to(u=m\leftrightarrow v=n))\)

\(→(f=n\to(u=a\leftrightarrow v=c))\)

10.8,9からモダスポーネンスで

\(f=n→(u=a\leftrightarrow v=c)\)

11.10に存在汎化と普遍汎化で

\(∀x∃z(f=x\to(u=x\leftrightarrow v=z))\)

存在例化の際にはその論理式の中ですでに使われていない名前の変数をつかうこと。すでに使われている名前をつかった例化は一般的に妥当な推論ではない。代入やα変換についても同様。普遍例化は適宜に。

任意の m について、yの存在についての述語

\(∃y(f=m\to (u=m\leftrightarrow v=y))\)

の否定とペアノ算術(算術のモデルの1階部分)で同値になる論理式はΣ_1の中には存在しない。証明課題

以上で x に関する関数 2x+1 の全域性を証明できた。また、前提を調整して任意の定数 a について 2x+a の全域性を証明できる。

これで \(f_1\) までの関数の全域性を証明できた。ただし加法の全域性はまだ証明できていない。

つぎに後者関数の公理を

\(\forall x\exists y(f_1=0\to(f_0=0\to(u=x\leftrightarrow v=y)))\)

と表現しなおし、関数のエンコードの定義を

\(\forall l\forall m\exists n\forall a\exists b\exists c((f_1=l\to(f_0=m\to(u=a\leftrightarrow v=b)))\)

\(\land(f_1=l\to(f_0=0\to(u=b\leftrightarrow v=c)))\)
\(\land(f_1=0\to(f_0=0\to(u=m\leftrightarrow v=n)))\)
\(\to(f_1=l\to(f_0=n\to(u=a\leftrightarrow v=c))))\)

\(\forall m\exists n\forall x\exists y((f_1=m\to(f_0=x\to(u=x\leftrightarrow v=y)))\)

\(\land(f_1=0\to(f_0=0\to(u=m\leftrightarrow v=n)))\)
\(\leftrightarrow(f_1=n\to(f_0=0\to(u=x\leftrightarrow v=y))))\)

に更新する。上と同様にして、

\(\forall x\exists y(f_1=0\to(f_0=x\to(u=x\leftrightarrow v=y)))\)

すなわち

\(\forall x\exists y(f_1=1\to(f_0=0\to(u=x\leftrightarrow v=y)))\)

が証明可能。以下、IΣ_1 でそれぞれの f_1 の値につき、

\(\forall x\exists y(f_1=l\to(f_0=0\to(u=x\leftrightarrow v=y)))\)

が証明可能だが、すべてのf_1の値について成り立つことを証明することはできない。

ここまで \(f_{\omega}\) までの全域性を証明できた。2変数アッカーマン、3変数のBEAF、上矢印表記、証明論的順序数で \(\omega^{\omega}\) バシク行列で (0)(1)(2) の強さ。

\(I\Sigma_1\) は \(RCA_0\) と \(WKL_0\) の1階部分となっている。また、対偶とモダスポーネンスから \(I\Pi _1\) と同値であることを示すことができる。

\(\displaystyle \frac{u=x \land \frac {u \neq x \gets \forall y \lnot \phi(y)}{u=x \to \exists y \phi(y)}(contraposition)}{\exists y \phi (x,y)}(MP)\)

\(I\Sigma_n (n=1,2,3,...)\) でも同様。\(\Sigma_n\) 論理式の否定が \(\Pi_n\) 論理式になることに関連する。

\(I\Sigma_2\)

\(\psi(0,x,y)\iff f=0\to(u=x\leftrightarrow v=y)\land\psi(n,x,y)\iff f_{\omega^n}=x\to\psi(n-1,x,y)\)

任意の n について、後者に関する公理

\(\forall x\exists y(f_{\omega^n}=0\to(f_{\omega^{n-1}}=0\to\cdots\to(f_0=0\to(u=x\leftrightarrow v=y))\cdots))\)

そんなこんなで \(I\Sigma_2\) で \(\omega ^{\omega ^\omega}\) 、多変数アッカーマン、BEAFの線形配列、バシク行列で \((0)(1)(2)(3)\)

\(I\Sigma_3\) で \(\omega ^{\omega ^{\omega ^\omega}}\) 、多次元配列、\((0)(1)(2)(3)(4)\) 、

・・・

\(I\Sigma _\infty\) 、つまりペアノ算術そのままの強さが \(\epsilon _0\)


述語記号をつかって・・・

\(\forall x\exists !y\phi (x,y)\)

基本となる関数 \(f\) の全域性を証明するのに \(\omega\)

\(\forall x \exists !t_1\exists !y(\phi(x,t_1)\land (\phi(x,t_1)\to \phi(t_1,y)))\)

\(f^2\) で \(\omega \cdot 2\)

\(\forall x\exists !t_2\exists !t_1 \exists y((\text{\(f^2\) の全域性})\land((\phi(x,t_2)\to \phi(t_2,t_1))\to \phi(t_1.y))\)

\(f^3\) で \(\omega\cdot 3\)

\(f_1\) で \(\omega^2\) ・・・

広告ブロッカーが検出されました。


広告収入で運営されている無料サイトWikiaでは、このたび広告ブロッカーをご利用の方向けの変更が加わりました。

広告ブロッカーが改変されている場合、Wikiaにアクセスしていただくことができなくなっています。カスタム広告ブロッカーを解除してご利用ください。

Fandomでも見てみる

おまかせWiki