保存拡大

保存拡大（ほぞんかくだい、テンプレート:Lang-en）は数理論理学において、形式言語による理論同士の関係の一つであり、定理の証明を便利にするかもしれないが、決して元の理論が原理的に証明できる定理の範疇を超えないような、理論の拡張を指す。同様に、非保存拡大（ひほぞんかくだい、テンプレート:Lang-en）あるいは「真の拡大」（テンプレート:Lang-en）により拡張された理論は、元の理論より多くの定理を証明できる能力を持つ。

より形式的に言い直すと、 もし $T_1$によるいかなる定理も $T_2$による定理であり、 $T_2$によるいかなる定理の $T_1$における表現も既に $T_1$の定理であるのならば、理論 $T_2$ は証明論的に理論 $T_1$の保存拡大になっていると言える。

より一般的には、 $\mathrm{\Gamma }$ を$T_1$ and $T_2$の共通言語における論理式の集合とした時、 $T_2$で証明できる $\mathrm{\Gamma }$のいかなる論理式も $T_1$で証明できるならば、$T_2$ は $T_1$ に対して $\mathrm{\Gamma }$保存 （テンプレート:Lang-en）であると表現できる。

無矛盾な理論の保存拡大は無矛盾性を維持する。保存拡大が無矛盾性を維持しないと反実仮想すると、テンプレート:仮リンクにより $T_2$ の言語で書き得るあらゆる論理式は真になる、つまり $T_2$ の定理になり、それにより $T_1$の言語で書き得るあらゆる論理式も $T_1$の定理になるので $T_1$が無矛盾でなくなってしまう（背理法）。このように保存拡大は矛盾をもちこむ危険性が無い。この手続きは大きな理論を記述し、構成する方法論とも捉えることができる。つまり、無矛盾であると知られて（もしくは仮定されて）いる理論 $T_0$ から出発して、その保存拡大 $T_1$, $T_2$ …を構成していくことで、無矛盾な大きな理論を構成することができる。

近年、保存拡大はオントロジーのモジュールを定義する際に使われるようになってきている。形式論理としてのオントロジにおいて、その理論がある部分理論の保存拡大になっているとき、部分理論はモジュールとみなすことができる。

関連項目

• フォン・ノイマン＝ベルナイス＝ゲーデル集合論: 選択公理を含むツェルメロ＝フレンケル集合論の保存拡大