保守的な拡張
数理論理学において、保存的拡張とは、定理を証明するのにしばしば便利な理論の超理論であるが、元の理論の言語に関する新たな定理は証明しない。同様に、非保存的拡張、あるいは真拡張とは、保存的ではない超理論であり、元の理論よりも多くの定理を証明できる。
より正式に述べると、 のすべての定理が の定理であり、の言語におけるの任意の定理がすでに の定理である場合、理論は理論の(証明論的な)保存的拡張です。
より一般的には、が との共通言語による式の集合である場合、で証明可能なからのすべての式が においても証明可能であるならば、 はに対して-保存的です。
整合理論の保守的な拡張は整合していることに注意してください。整合していない場合は、爆発の原理により、 の言語におけるすべての式はの定理となり、 の言語におけるすべての式はの定理となり、整合しなくなります。したがって、保守的な拡張は新たな矛盾をもたらすリスクを負いません。これは、大規模な理論を記述および構築するための方法論としても考えられます。整合していることが既知(または仮定)の理論 から始めて、その、 、… を順次、保守的な拡張として構築していきます。
最近、オントロジーのモジュールの概念を定義するために、保守的な拡張が使用されています。オントロジーが論理理論として形式化されている場合、オントロジー全体がサブ理論の保守的な拡張である場合、サブ理論はモジュールです。
例
- は、逆数学で研究される2 階算術のサブシステムであり、 1 階ペアノ算術の保存的な拡張です。
- 2階算術およびの部分系は に対して-保存的である。[ 1 ]
- 部分系はの -保存的拡張であり、(原始再帰演算)上の -保存的である。[ 1 ]
- フォン・ノイマン・バーネイス・ゲーデル集合論( )は、選択公理( )を持つツェルメロ・フランケル集合論の保存的拡張である。
- 内部集合論は選択公理( )を用いたツェルメロ-フランケル集合論の保存的拡張である。
- 定義上、拡張は保守的です。
- 制約のない述語または関数シンボルによる拡張は保守的です。
- ( -式に対してのみ帰納法を用いたペアノ算術の部分系)はの -保存的拡張である。[ 2 ]
- は、ショーンフィールドの絶対性定理によるの -保存的拡張である。[ 3 ]
- 一般化連続体仮説はの-保存的拡張である。[ 4 ]
モデル理論的保存的拡張
モデル理論的手段を用いると、より強い概念が得られる。すなわち、理論の拡張は、のあらゆるモデルがのモデルに拡張できるとき、モデル理論的に保守的である。各モデル理論的保守的拡張は、上記の意味での(証明理論的)保守的拡張でもある。[ 5 ]モデル理論的概念は、証明理論的概念に比べて、使用する言語にそれほど依存しないという利点がある。その一方で、モデル理論的保守性を確立するのは通常難しい。
参照
参考文献
- ^ a b S. G. Simpson, RL Smith, " Factorization of polynomials and -induction " (1986). Annals of Pure and Applied Logic, vol. 31 (p.305)
- ^ Fernando Ferreira, パーソンズの定理の簡単な証明. Notre Dame Journal of Formal Logic, Vol.46, No.1, 2005.
- ^ Michael Rathjen, Power Kripke-Platek 集合論と選択公理. Journal of Logic and Computation, Vol.30, No.1, 2018.
- ^リチャード・プラテック「連続体仮説の排除」『記号論理学ジャーナル』第36巻第1号、1969年。
- ^ホッジス、ウィルフリッド(1997). 『より短いモデル理論』 ケンブリッジ:ケンブリッジ大学出版局. p. 58 演習8. ISBN 978-0-521-58713-6。