定義による拡張

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

において、すなわちすべての, ...,に対して、となる唯一のy が存在する。新しい- 項関数記号、記号を含む論理公理、および新しい公理 を追加することで、から新しい一階の理論を形成する。${\displaystyle T}$ ${\displaystyle x_{1}}$ ${\displaystyle x_{n}}$ ${\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}$

を の任意の原子式とする。の式を以下のように再帰的に定義する。新しい記号が に現れない場合、 をとする。そうでない場合、の項に現れないにおけるの出現を選び、その出現を新しい変数 に置き換えることでから が得られるとする。すると、は におけるよりも 1回少ない回数で現れるので、式は既に定義されているので、 とする。 ${\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}$ ${\displaystyle t_{i}}$ ${\displaystyle \chi }$ ${\displaystyle \psi}$ ${\displaystyle z}$ ${\displaystyle f}$ ${\displaystyle \chi }$ ${\displaystyle \psi}$ ${\displaystyle \chi^{\ast}}$ ${\displaystyle \psi^{\ast}}$

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

（ に現れる変数が に束縛されないように、必要であれば の束縛変数を変更します）。一般的な式 の場合、式 は、原子部分式のすべての出現を に置き換えることによって形成されます。このとき、次の式が成り立ちます。 ${\displaystyle \phi }$ ${\displaystyle 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 項関数シンボルとして見ることができる定数にも適用されます。

定義による拡張

上記のように関係記号と関数記号を順に導入することでから得られる一階理論は、の定義による拡大と呼ばれます。すると はの保存的拡大となり、 の任意の式に対しての式（から への変換と呼ばれる）を形成することができ、 がで証明可能となります。このような式は一意ではありませんが、その任意の2つはTにおいて同値であることが証明できます。 ${\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'}$

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

例

• 伝統的に、一階集合論ZFは（等式）と（所属）を唯一の基本関係記号として持ち、関数記号は持ちません。しかし、日常の数学では、二項関係記号、定数、単項関数記号P（べき乗集合演算）など、他の多くの記号が用いられます。これらの記号はすべて、ZFの定義により拡張に属します。${\displaystyle =}$ ${\displaystyle \in}$ ${\displaystyle \subseteq }$ ${\displaystyle \emptyset }$
• を、二項積×のみを原始記号とする群の第一階理論とする。Tにおいて、任意のxに対してx  ×  y  = y  ×  x  = x を満たす唯一の元y が存在することを証明できる。したがって、 Tに新しい定数eを加えると、公理が成り立つ。${\displaystyle T}$

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

そして、の定義による拡張が得られる。すると、 において、任意のxに対して、 x  ×  y  = y  ×  x  = eを満たす唯一のyが存在することが証明できる。したがって、から得られる一階の理論は、単項関数記号と公理を 追加することによって得られる。${\displaystyle T'}$ ${\displaystyle T}$ ${\displaystyle T'}$ ${\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}}$

参照

• 保守的な拡張
• 明確な説明
• イプシロン計算
• 新しい定数名と関数名による拡張

参考文献

• SC Kleene (1952)、メタ数学入門、D. Van Nostrand
• E. メンデルソン(1997). 『数理論理学入門』（第4版）, チャップマン＆ホール.
• JRショーンフィールド（1967年）『数学論理学』アディソン・ウェズリー出版社（2001年にAKピーターズ社より再版）