効果的なトポス

数学において、マーティン・ハイランド(1982)によって導入された有効トポスは、 カテゴリー理論の枠組み内で有効性 という数学的な考え方を捉えています。 ${\displaystyle {\mathsf {Eff}}}$

意味

予選

クリーネ実現可能性

トポスは、クリーネの第一代数によって与えられた部分組合せ代数 に基づいています。クリーネの再帰的実現可能性の概念では、任意の述語に実現数、すなわちの部分集合が割り当てられます。極値命題はと で、これらはとによって実現されます。しかし、一般に、このプロセスは命題に二項真理値だけでなく、より多くのデータを割り当てます。 ${\displaystyle {\mathcal {K}}_{1}}$ ${\displaystyle {\mathbb {N} }}$ ${\displaystyle \top}$ ${\displaystyle \bot}$ ${\displaystyle {\mathbb {N} }}$ ${\displaystyle \{\}}$

自由変数を含む式は、対応する実現子のサブセットの値を 持つマップを生成します。${\displaystyle k}$ ${\displaystyle ({\mathcal {P}}{\mathbb {N} })^{{\mathbb {N} }^{k}}}$

実現可能性トポイ

${\displaystyle {\mathsf {Eff}}}$ 実現可能性トポスの代表的な例である。これらは直観主義的な内部論理を持ち、ある種の従属的選択を満たす基本トポスのクラスである。一般にグロタンディーク・トポスではない。

特に、有効なトポスは である。他の実現可能性トポスの構築は、ここで が果たすいくつかの側面を抽象化すると言える。 ${\displaystyle {\mathsf {RT}}({\mathcal {K}}_{1})}$ ${\displaystyle {\mathbb {N} }}$

Effの説明

オブジェクトは、における対称的かつ推移的な関係を持つ集合のペアであり、一種の等式述語を表しますが、 の部分集合となる値を取ります。が自身とどのように関係するかを表す、いわゆる存在述語を表すために、引数を1つだけ用いて記述します。これは空であってもよく、関係は一般に反射的ではないことを表します。矢印は、定義された等式を適切に尊重する関数関係の同値類に相当します。 ${\displaystyle \langle X,E_{X}\rangle }$ ${\displaystyle ({\mathcal {P}}{\mathbb {N} })^{X\times X}}$ ${\displaystyle \mathbb {N} }$ ${\displaystyle E_{X}(x)}$ ${\displaystyle x}$

分類子はとなる。ペア（または、表記法 の乱用により、その根底にあるべき集合）は と表記される。上の含意関係により、これはHeyting の前代数となる。このような文脈により、適切な格子状の論理構造を定義することが可能となり、論理演算は実現子集合の演算によって与えられ、ペアと計算可能関数が用いられる。 ${\displaystyle {\mathcal {P}}{\mathbb {N} }}$ ${\displaystyle \オメガ}$ ${\displaystyle \vdash _{X}}$ ${\displaystyle {\mathcal {P}}{\mathbb {N} }^{X}}$

終端オブジェクトは、自明な存在述語（すなわち、 と等しい）を持つシングルトンです。有限積は等式を適切に尊重します。分類子の等式は、その格子内の同値性によって与えられます。 ${\displaystyle \langle \{*\},E_{\{*\}}\rangle }$ ${\displaystyle {\mathbb {N} }}$ ${\displaystyle E_{{\mathcal {P}}{\mathbb {N} }}}$

プロパティ

集合との関係

いくつかのオブジェクトは、集合の等式関係「」の妥当性のみに依存する、むしろ自明な存在述語を示す。そのため、有効な等式は最上位集合 に写像され、否定される等式は に写像される。これにより、集合 のカテゴリから、有限極限保存大域切断関数を左随伴として持つ、完全かつ忠実な関数が生じる。 これは、有限極限保存、完全かつ忠実な埋め込み を介して因数分解される。${\displaystyle =}$ ${\displaystyle \mathbb {N} }$ ${\displaystyle \{\}}$ ${\displaystyle \nabla \colon {\mathsf {Sets}}\to {\mathsf {Eff}}}$ ${\displaystyle \Gamma}$ ${\displaystyle \omega }$ ${\displaystyle {\mathsf {Sets}}\to {\mathsf {Eff}}}$

NNO

トポスは単に という自然数オブジェクト を持ちます。 について真である文は、まさにハイティング算術の再帰的に実現された文です。 ${\displaystyle N=\langle {\mathbb {N} },E_{\mathbb {N} }\rangle }$ ${\displaystyle E_{\mathbb {N} }(n)=\{n\}}$ ${\displaystyle N}$ ${\displaystyle {\mathsf {HA}}}$

ここで、矢印は全再帰関数として理解でき、これは についても内部的に成り立ちます。後者は、全再帰関数と、のコード集合となる関係によって与えられるペアです。後者は自然数のサブセットですが、同じ再帰関数を計算するインデックスが複数あるため、単なるシングルトンではありません。したがって、ここではオブジェクトの2番目の要素が実現データを表します。 ${\displaystyle N\to N}$ ${\displaystyle N^{N}}$ ${\displaystyle \mathrm {TR} }$ ${\displaystyle E_{\mathrm {TR} }(f)}$ ${\displaystyle e\in {\mathbb {N} }}$ ${\displaystyle f}$

から および への関数と、有限積 を形成する際の等式関係の簡単な規則を用いることで、遺伝的に有効な演算をより広く定義できるようになりました。ここでも、 の関数は添え字によって与えられ、それらの等式は同じ関数を計算するオブジェクトによって決定されると考えることができます。この等式は明らかに に制約を課します。なぜなら、これらの関数は、その定義域において前述の等式を適切に遵守する計算可能関数のみとなるからです。などなど。一般的な の場合、定義域と像における等式（ の意味で）は遵守されなければなりません。 ${\displaystyle N}$ ${\displaystyle \times }$ ${\displaystyle N^{N}}$ ${\displaystyle N^{(N^{N})}}$ ${\displaystyle \langle X,E_{X}\rangle \to \langle Y,E_{Y}\rangle }$ ${\displaystyle E}$

特性と原理

これにより、マルコフ原理 と拡張チャーチ原理（およびその二次変種）を検証できます。これらは、または のようなオブジェクトに関する単純な命題に帰着します。これらは、 と が前提 から独立していることを意味します。 ${\displaystyle {\mathrm {MP} }}$ ${\displaystyle {\mathrm {ECT} }_{0}}$ ${\displaystyle N^{N}}$ ${\displaystyle (1+1)^{N}}$ ${\displaystyle {\mathrm {CT} }_{0}}$ ${\displaystyle {\mathrm {IP} }_{0}}$

ブラウワーの弱連続性に関連する選択原理は成り立たない。任意の対象から への矢印は可算個しかない。 は一様性原理を満たす。 は のコピーの可算な余積ではない。このトポスは層の圏ではない。 ${\displaystyle N^{N}}$ ${\displaystyle N}$ ${\displaystyle \Omega^{N}}$ ${\displaystyle N}$ ${\displaystyle 1}$

分析

この対象は形式的な意味で有効であり、そこから計算可能なコーシー列を定義できる。商を通して、トポスは非自明な決定可能な部分対象を持たない実数対象を持つ。選択により、デデキント実数の概念はコーシー実数の概念と一致する。 ${\displaystyle \langle {\mathbb {Q} }^{\mathbb {N} },E_{{\mathbb {Q} }^{\mathbb {N} }}\rangle }$

特性と原理

ここでの解析は、構成主義の再帰学派に相当する。この学派は、すべての実数に対して成立するであろう主張を否定する。中間値定理の定式化は成り立たず、実数から実数へのすべての関数は連続であることが証明されている。スペッカー列が存在する場合、ボルツァーノ＝ワイエルシュトラスの法則は成立しない。 ${\displaystyle x\leq 0\lor 0\leq x}$ ${\displaystyle x}$

参照

• カテゴリカルロジック

参考文献

• ハイランド、JME (1982)、「効果的なトポス」(PDF)、AS 州トロエルストラ; Dalen, D. van (編)、LEJ Brouwer Centenary Symposium (Noordwijkerhout、1981)、 Studies in Logic and the Foundations of Mathematics、vol. 110、アムステルダム: 北オランダ、pp.  165–216、doi :10.1016/S0049-237X(09)70129-6、ISBN 978-0-444-86494-9、MR  0717245
• Kleene, SC (1945). 「直観主義的数論の解釈について」. Journal of Symbolic Logic . 10 (4): 109– 124. doi :10.2307/2269016. JSTOR  2269016. S2CID  40471120.
• Phoa, Wesley (1992). ファイブレーション、トポス理論、実効トポス、そしてモデスト集合への入門（技術レポート）. エディンバラ大学コンピュータサイエンス基礎研究所. CiteSeerX  10.1.1.112.4533 . ECS-LFCS-92-208.
• バーナデット、アレクシス。グラハム・ラングラン、ステファン（2013）。 「効果的なトポスの簡単なプレゼンテーション」。arXiv : 1307.3832 [cs.LO]。
• Corfield, David; Ramesh, Sridhar; Schreiber, Urs; Bartels, Toby; Škoda, Zoran; Shulman, Mike; Trimble, Todd; Roberts, David; Holder, Thomas (2023年1月22日) [2009年7月10日], effective topos (19 ed.), nLab