保存拡大

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

より形式的に言い直すと、 もし ${\displaystyle T_{1}}$によるいかなる定理も ${\displaystyle T_{2}}$による定理であり、 ${\displaystyle T_{2}}$によるいかなる定理の ${\displaystyle T_{1}}$における表現も既に ${\displaystyle T_{1}}$の定理であるのならば、理論 ${\displaystyle T_{2}}$ は証明論的に理論 ${\displaystyle T_{1}}$の保存拡大になっていると言える^[2]。

より一般的には、 ${\displaystyle \Gamma }$ を${\displaystyle T_{1}}$ and ${\displaystyle T_{2}}$の共通言語における論理式の集合とした時、 ${\displaystyle T_{2}}$で証明できる ${\displaystyle \Gamma }$のいかなる論理式も ${\displaystyle T_{1}}$で証明できるならば、${\displaystyle T_{2}}$ は ${\displaystyle T_{1}}$ に対して ${\displaystyle \Gamma }$保存 （英語: ${\displaystyle \Gamma }$-conservative）であると表現できる^[3]。

無矛盾な理論の保存拡大は無矛盾性を維持する。保存拡大が無矛盾性を維持しないと反実仮想すると、爆発律により ${\displaystyle T_{2}}$ の言語で書き得るあらゆる論理式は真になる、つまり ${\displaystyle T_{2}}$ の定理になり、それにより ${\displaystyle T_{1}}$の言語で書き得るあらゆる論理式も ${\displaystyle T_{1}}$の定理になるので ${\displaystyle T_{1}}$が無矛盾でなくなってしまう（背理法）。このように保存拡大は矛盾をもちこむ危険性が無い。この手続きは大きな理論を記述し、構成する方法論とも捉えることができる。つまり、無矛盾であると知られて（もしくは仮定されて）いる理論 ${\displaystyle T_{0}}$ から出発して、その保存拡大 ${\displaystyle T_{1}}$, ${\displaystyle T_{2}}$ …を構成していくことで、無矛盾な大きな理論を構成することができる。

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