保存拡大のソースを表示

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

より形式的に言い直すと、 もし <math>T_1</math>によるいかなる定理も <math>T_2</math>による定理であり、 <math>T_2</math>によるいかなる定理の <math>T_1</math>における表現も既に <math>T_1</math>の定理であるのならば、理論 <math>T_2</math> は[[証明論]]的に理論 <math>T_1</math>の保存拡大になっていると言える<ref>[[新井敏康]]:「第２章と第５章」 http://fe.math.kobe-u.ac.jp/Movies/cm/2007-04-kiso-a-note1.pdf の定義2.9 pp.12-13. {{Accessdate|2023-02-15}}</ref>。

より一般的には、 <math>\Gamma</math> を<math>T_1</math> and <math>T_2</math>の共通言語における[[論理式 (数学)|論理式]]の集合とした時、 <math>T_2</math>で証明できる <math>\Gamma</math>のいかなる論理式も <math>T_1</math>で証明できるならば、<math>T_2</math> は <math>T_1</math> に対して <math>\Gamma</math>'''保存''' （{{Lang-en|<math>\Gamma</math>-conservative}}）であると表現できる<ref>日本語でも、照井一成「直観主義論理への招待」（数学基礎論サマースクール 2013 講義資料 https://www.kurims.kyoto-u.ac.jp/~terui/summer2013.pdf {{Accessdate|2023-02-15}}）の定理 5.10において、<math>\Pi_2^0</math>論理式の集合に対する保存拡大を「<math>\Pi_2^0</math>保存拡大」と呼んでいる。</ref>。

[[無矛盾]]な理論の保存拡大は無矛盾性を維持する。保存拡大が無矛盾性を維持しないと反実仮想すると、{{仮リンク|爆発律|en|principle of explosion}}により <math>T_2</math> の言語で書き得るあらゆる論理式は真になる、つまり <math>T_2</math> の定理になり、それにより <math>T_1</math>の言語で書き得るあらゆる論理式も <math>T_1</math>の定理になるので <math>T_1</math>が無矛盾でなくなってしまう（背理法）。このように保存拡大は矛盾をもちこむ危険性が無い。この手続きは大きな理論を記述し、構成する方法論とも捉えることができる。つまり、無矛盾であると知られて（もしくは仮定されて）いる理論 <math>T_0</math> から出発して、その保存拡大 <math>T_1</math>, <math>T_2</math> …を構成していくことで、無矛盾な大きな理論を構成することができる。

近年、保存拡大は[[オントロジー (情報科学)|オントロジー]]のモジュールを定義する際に使われるようになってきている<ref>例: 博物資料の記述に用いるオントロジ CIDOC CRM のドキュメント（7.1.2版） https://www.cidoc-crm.org/sites/default/files/cidoc_crm_version_7.1.2.pdf において Extensions of CIDOC CRM の節でそのような説明がされている。</ref>。形式論理としてのオントロジにおいて、その理論がある部分理論の保存拡大になっているとき、部分理論はモジュールとみなすことができる。

==脚注==
{{脚注ヘルプ}}
{{Reflist}}

== 関連項目 ==
* [[フォン・ノイマン＝ベルナイス＝ゲーデル集合論]]: [[ツェルメロ＝フレンケル集合論|選択公理を含むツェルメロ＝フレンケル集合論]]の保存拡大

{{デフォルトソート:ほそんかくたい}}
[[Category:証明論]]
[[Category:モデル理論]]
[[Category:数理論理学]]
[[Category:数学に関する記事]]