利用者:Sillycrown/sandbox3

内的集合論（英: internal set theory、IST）は集合論に基づく超準解析の公理化のひとつである。エドワード・ネルソンによって開発された。大雑把に言えばZFCの超準モデルの振る舞いを公理化したものである。

概要

詳細は「超準解析」を参照

超準解析の標準的なモデル論的アプローチでは、十分に多くの数学的対象を含むユニバース$\mathbb {U}$を固定し、十分な飽和性と初等拡大性（有界論理式に制限されることがある）を満たす超準モデル$^{\ast }\mathbb {U}$を構成する。超準宇宙$^{\ast }\mathbb {U}$に属す集合は内的集合と呼ばれる。

エドワード・ネルソンは、シグネチャ$(2,1)$の構造$({}^{\ast }\mathbb {U} ;{}^{\ast }\in ,\mathbb {U} )$（$\mathbb {U}$はZFCの標準モデル、$^{\ast }\mathbb {U}$は$|\mathbb {U} |$-飽和的な初等拡大）の公理化を与え、これを内的集合論$\mathrm {IST}$と名付けた。ISTはInternal Set Theoryの頭文字であるが、後述するIdealization・Standardization・Transferという三つの公理型の頭文字でもある。

公理

形式的体系$\mathrm {IST}$は古典論理上の等号付き一階述語論理の理論である。（等号を除く）非論理記号としては次のものを持つ。

1. 二項述語記号 $\in$
2. 単項述語記号 $\operatorname {st} (x)$ これは「標準的」と読む

ここでは関数記号や他の述語記号を含まない体系を考えているが、標準的な集合論におけると同様に定義による拡大によって空集合記号（定数記号）、冪集合記号（単項関数記号）、関数適用記号（二項関数記号）などを導入できるから、最初からそれらの語彙を含んでいるとしても構わない。

$\mathrm {IST}$は次の4種類の公理からなる。

1. $\mathrm {ZFC}$の公理全て
2. 理想化（英: Idealization）の公理型
3. 標準化（英: Standardization）の公理型
4. 移行（英: Transfer）の公理型

最初の群の公理は、内的集合（議論領域の対象）全体が$\mathrm {ZFC}$の公理を全て満たす、ということを述べている。ただし、$\mathrm {ZFC}$の公理図式に代入できる論理式は∈-論理式のみである。つまり$\operatorname {st} (x)$を含む論理式は公理図式に代入できない。とくに置換公理（ないし分出公理）を使って、（内的）集合$A$に対し

$A^{\sigma }=\{x\in A\mid \operatorname {st} (x)\}$

のような部分集合を作ることはできない。この制限はモデル論的な超準解析において$A^{\sigma }$の形の集合が必ずしも内的にならないという事実と対応している。

理想化公理は飽和性に対応する。これにより標準的でない内的集合が豊富に存在することが導かれる。モデル論的な超準解析では飽和原理と呼ばれているものである。

標準化公理は、標準的集合を超準的に定義できる、ということを述べている。例えば、モデル論的な超準解析においては、標準集合$X$の有限部分集合全体は

$P_{fin}(X)=\{A\subseteq X|\forall x\in {}^{\ast }{A}(\operatorname {st} (x))\}$

と記述できる。この右辺の定義をISTの言語で記述するには述語「標準的」を用いる必要があることから、ISTの枠内ではZFCの分出公理を適用できない。このように超準的な論理式を使って標準的な集合を構成することを可能とするのが標準化原理である。

移行公理は初等拡大性に対応する。これにより内的集合全体と標準集合全体が∈-論理式に関する限り同一の振る舞いをするということである。このことと、内的集合全体がZFCの各々の公理を満たすことから、標準集合全体もZFCの各々の公理を満たすことが導かれる。モデル論的な超準解析では移行原理と呼ばれているものである。

還元アルゴリズム

概要

$\mathrm {IST}$は$\mathrm {ZFC}$の保存的拡大であることから、$\mathrm {IST}$で標準的な（∈-論理式で書かれた）定理を証明すれば、$\mathrm {ZFC}$でも証明可能であることが得られる。とくに、前者からの形式的証明が与えられたならば、$\mathrm {ZFC}$の中で保存的拡大性の証明の流れを形式化してやることで、$\mathrm {ZFC}$からの形式的証明が得られる。

上記の方法は$\mathrm {IST}$で得られる証明は、単に具体的な超準モデルの中で超準的証明を遂行するという形（つまりモデル論的な超準解析に基づく証明）になっており、我々が「標準的証明」と言って期待されるところの証明になってはいない。ネルソンは、超準的証明が与えられたときに、そこから純粋に構文論的な仕方で標準的証明を得るアルゴリズムを与え、これを還元アルゴリズム（reduction algorithm）と呼んだ。

限界

内的集合論でオブジェクトとして扱えるのは内的集合のみである。外的集合はクラス（論理式の略記）として扱う必要がある。したがって、外的集合を積極的に用いる議論については、内的集合論の枠内では限界があり、様々なトリックを利用する必要がある。

このような限界に対処するために外的集合も扱えるように改良された理論が色々と提案されている。