定義による拡張

数理論理学、より具体的には一階述語論理の証明論において、定義による拡張は、定義によって新しい記号を導入することを形式化する。例えば、素朴集合論では、記号を導入することが一般的である。${\displaystyle \emptyset }$要素を持たない集合の場合。一階理論の形式的な設定では、これは理論に新しい定数を追加することによって実現できます。${\displaystyle \emptyset }$そして新しい公理${\displaystyle \forall x(x\notin \emptyset )}$つまり、「すべてのxに対して、xはメンバーではない」という意味です。${\displaystyle \emptyset }$。そうすることで、定義から当然予想されるように、古い理論に本質的に何も追加されないことが証明できる。より正確に言えば、新しい理論は古い理論の保守的な拡張である。

させて${\displaystyle T}$一次理論であり、${\displaystyle \phi (x_{1},\dots ,x_{n})}$式​​${\displaystyle T}$そのため${\displaystyle x_{1}}$、...、${\displaystyle x_{n}}$は区別され、変数も自由に含まれる${\displaystyle \phi (x_{1},\dots ,x_{n})}$新しい一次理論を構築する${\displaystyle T'}$から${\displaystyle T}$新しいものを追加することで${\displaystyle n}$-項関係記号${\displaystyle R}$記号を特徴とする論理公理${\displaystyle R}$そして新しい公理

${\displaystyle \forall x_{1}\dots \forall x_{n}(R(x_{1},\dots ,x_{n})\leftrightarrow \phi (x_{1},\dots ,x_{n}))}$、

定義公理と呼ばれる${\displaystyle R}$。

もし${\displaystyle \psi }$は、${\displaystyle T'}$、 させて$\displaystyle \psi ^{\ast }}$の式である${\displaystyle T}$から入手${\displaystyle \psi }$あらゆる出現箇所を置き換えることによって${\displaystyle R(t_{1},\dots ,t_{n})}$による${\displaystyle \phi (t_{1},\dots ,t_{n})}$（バインド変数を変更する）${\displaystyle \phi }$必要に応じて、変数が$t_i$拘束されていない${\displaystyle \phi (t_{1},\dots ,t_{n})}$) すると、次のことが成り立つ。

1. ${\displaystyle \psi \leftrightarrow \psi ^{\ast }}$証明可能${\displaystyle T'}$、 そして
2. ${\displaystyle T'}$保守的な拡張である${\displaystyle T}$。

事実${\displaystyle T'}$保守的な拡張である${\displaystyle T}$定義公理は${\displaystyle R}$新しい定理を証明するために使用することはできません。$\displaystyle \psi ^{\ast }}$翻訳と呼ばれる${\displaystyle \psi }$の中へ${\displaystyle T}$意味論的には、この式は$\displaystyle \psi ^{\ast }}$と同じ意味です${\displaystyle \psi }$しかし、定義されたシンボル${\displaystyle R}$削除されました。

させて${\displaystyle T}$1階理論（等号付き）であり、${\displaystyle \phi (y,x_{1},\dots ,x_{n})}$式${\displaystyle T}$そのため${\displaystyle y}$、${\displaystyle x_{1}}$、...、${\displaystyle x_{n}}$は区別され、変数も自由に含まれる${\displaystyle \phi (y,x_{1},\dots ,x_{n})}$証明できると仮定します

${\displaystyle \forall x_{1}\dots \forall x_{n}\exists !y\phi (y,x_{1},\dots ,x_{n})}$

で${\displaystyle T}$つまり、すべての${\displaystyle x_{1}}$、...、${\displaystyle x_{n}}$一意のyが存在し、${\displaystyle \phi (y,x_{1},\dots ,x_{n})}$新しい一次理論を構築する${\displaystyle T'}$から${\displaystyle T}$新しいものを追加することで${\displaystyle n}$-項関数記号${\displaystyle f}$記号を特徴とする論理公理${\displaystyle f}$そして新しい公理

${\displaystyle \forall x_{1}\dots \forall x_{n}\phi (f(x_{1},\dots ,x_{n}),x_{1},\dots ,x_{n})}$、

定義公理と呼ばれる${\displaystyle f}$。

させて${\displaystyle \psi }$の任意の原子式である${\displaystyle T'}$式を定義します$\displaystyle \psi ^{\ast }}$の${\displaystyle T}$再帰的に次のようにします。新しいシンボルが${\displaystyle f}$発生しない${\displaystyle \psi }$、 させて$\displaystyle \psi ^{\ast }}$なれ${\displaystyle \psi }$それ以外の場合は、次の出現を選択します。${\displaystyle f(t_{1},\dots ,t_{n})}$で${\displaystyle \psi }$そのため${\displaystyle f}$用語には含まれません$t_i$、そして${\displaystyle \chi }$から入手できます${\displaystyle \psi }$その出現箇所を新しい変数に置き換えることによって${\displaystyle z}$それで、${\displaystyle f}$発生する${\displaystyle \chi }$より1回少ない${\displaystyle \psi }$式$\displaystyle \chi ^{\ast }}$すでに定義されており、$\displaystyle \psi ^{\ast }}$なれ

${\displaystyle \forall z(\phi (z,t_{1},\dots ,t_{n})\rightarrow \chi ^{\ast })}$

（バインド変数を変更する）${\displaystyle \phi }$必要に応じて、変数が$t_i$拘束されていない${\displaystyle \phi (z,t_{1},\dots ,t_{n})}$一般的な式については${\displaystyle \psi }$式$\displaystyle \psi ^{\ast }}$原子部分式の出現箇所すべてを置き換えることによって形成されます${\displaystyle \chi }$による$\displaystyle \chi ^{\ast }}$すると、以下のことが成り立つ。

1. ${\displaystyle \psi \leftrightarrow \psi ^{\ast }}$証明可能${\displaystyle T'}$、 そして
2. ${\displaystyle T'}$保守的な拡張である${\displaystyle T}$。

式$\displaystyle \psi ^{\ast }}$翻訳と呼ばれる${\displaystyle \psi }$の中へ${\displaystyle T}$関係記号の場合と同様に、式$\displaystyle \psi ^{\ast }}$と同じ意味です${\displaystyle \psi }$しかし新しいシンボル${\displaystyle f}$削除されました。

この段落の構成は定数にも適用でき、定数は0項関数記号とみなすことができます。

一次理論${\displaystyle T'}$から入手${\displaystyle T}$上記のように関係記号と関数記号を順次導入することによって定義される拡張は、${\displaystyle T}$。 それから${\displaystyle T'}$保守的な拡張である${\displaystyle T}$、また任意の数式について${\displaystyle \psi }$の${\displaystyle T'}$公式を形成できます$\displaystyle \psi ^{\ast }}$の${\displaystyle T}$翻訳と呼ばれる${\displaystyle \psi }$の中へ${\displaystyle T}$、したがって${\displaystyle \psi \leftrightarrow \psi ^{\ast }}$証明可能${\displaystyle T'}$このような式は一意ではないが、それらの任意の 2 つはTにおいて同等であることが証明できる。

実際には、定義による拡張${\displaystyle T'}$Tの式は元の理論Tと区別されません。実際、${\displaystyle T'}$これらは、翻訳をTに省略したものと考えることができる。これらの省略形を実際の式として操作することは、定義による拡張が保守的であるという事実によって正当化される。

• 従来、一階集合論ZFは${\displaystyle =}$（平等）そして${\displaystyle \in }$（メンバーシップ）を唯一の基本関係記号とし、関数記号は使用しない。しかし、日常の数学では、二項関係記号など、他にも多くの記号が使用される。${\displaystyle \subseteq }$定数${\displaystyle \emptyset }$、単項関数記号P (冪集合演算) など。これらの記号はすべて、実際には ZF の定義による拡張に属します。
• させて${\displaystyle T}$Tは、唯一の原始記号が二項積 × である群の一次理論である。T では、すべてのxに対してx × y = y × x = xとなるような一意の元yが存在することを証明できる。したがって、 Tに新しい定数eと公理を追加することができる。      

${\displaystyle \forall x(x\times e=x\land e\times x=x)}$、

そして、定義による拡張が得られる。${\displaystyle T'}$の${\displaystyle T}$.それから${\displaystyle T'}$任意のxに対して、 x × y = y × x = eとなる一意のyが存在することを証明できます。したがって、一階理論は      ${\displaystyle T''}$から入手${\displaystyle T'}$単項関数記号を追加することによって${\displaystyle f}$そして公理

${\displaystyle \forall x(x\times f(x)=e\land f(x)\times x=e)}$

定義による拡張${\displaystyle T}$。 いつもの、${\displaystyle f(x)}$と表記される${\displaystyle x^{-1}}$。

• 保守的な拡張
• 明確な記述
• イプシロン微積分
• 新しい定数名と関数名による拡張

• S.C. クリーネ(1952)、『メタ数学入門』、D. ヴァン・ノストランド
• E.メンデルソン（1997）。数理論理学入門（第4版）、チャップマン＆ホール。
• JR ショーエンフィールド(1967).数理論理学、アディソン・ウェスリー出版（2001年にAK ピーターズにより復刻）