代入 (論理学)

代入（だいにゅう、テンプレート:Lang-en-short）とは、形式的な表現に対する統語論的な変換である。 ある表現に代入を「適用する」とは、その変数、すなわちプレースホルダーとなる記号を、他の表現によって一貫して置き換えることを意味する。

得られた表現は、元の表現の「代入事例」、あるいは略して「事例」と呼ばれる。

命題論理

定義

ψ と φ が命題論理の論理式を表すとき、ψ が φ の「代入事例」であるとは、φ 中の命題変数に論理式を代入し、同一の変数の出現をすべて同一の論理式の出現で置き換えることによって ψ が得られる場合、かつその場合に限る（if and only if）。例えば、

ψ: (R → S) & (T → S)

は

φ: P & Q

の代入事例である。すなわち、ψ は φ 中の P と Q をそれぞれ (R → S) と (T → S) で置き換えることによって得られる。同様に、

ψ: (A ↔ A) ↔ (A ↔ A)

は次の代入事例である。

φ: (A ↔ A)

なぜなら、ψ は φ 中のそれぞれの A を (A ↔ A) で置き換えることによって得られるからである。

命題論理のための一部の演繹体系では、ある導出の一行が導出の以前の行の代入事例であれば、新たな表現（命題）をその行に記入することができるテンプレート:Failed verification。これは、一部の公理系において新しい行が導入される仕方である。変形規則を用いる体系では、規則がある導出に特定の変数を導入する目的で「代入事例」の使用を含むことがある。

トートロジー

ある命題論理式は、その述語記号のあらゆる付値（あるいは解釈）のもとで真であるならば、トートロジーである。Φ がトートロジーであり、Θ が Φ の代入事例であるならば、Θ もまたトートロジーである。この事実は、前節で説明した演繹規則の健全性を含意している。

一階論理

一階論理において、「代入」とは、変数から項への全域写像 テンプレート:Math である。多くの著者はテンプレート:Rpテンプレート:Rp（ただしすべての著者ではないテンプレート:Rp）、有限個を除くすべての変数 x について σ(x) = x であることをさらに要求する。記法 テンプレート:Mset は、それぞれの変数 x_i（i=1,…,k）を対応する項 t_i に写し、それ以外のすべての変数はそれ自身に写す代入を指す。x_i は互いに相異なっていなければならない。多くの著者はさらに、同じ代入に対する無限に多くの異なる記法を避けるため、それぞれの項 t_i が統語論的に x_i と異なることを要求する。項 t にその代入を「適用する」ことは、後置記法で t テンプレート:Mset と書かれる。これは、t 中のそれぞれの x_i のすべての出現を（同時に）t_i によって置き換えることを意味する。項 t に代入 σ を適用した結果 tσ は、その項 t の「事例」と呼ばれる。 例えば、代入 テンプレート:Mset を項

f(	z	, a, g(	x	), y)	に適用すると
f(	h(a,y)	, a, g(	z	), y)	が得られる。

代入 σ の「定義域」dom(σ) は、通常、実際に置き換えられる変数の集合として定義される。すなわち dom(σ) = テンプレート:Mset である。 代入は、その定義域のすべての変数をテンプレート:仮リンク項、すなわち変数を含まない項に写す場合、「基底」代入と呼ばれる。 基底代入の代入事例 tσ は、t のすべての変数が σ の定義域に含まれる場合、すなわち vars(t) ⊆ dom(σ) である場合、基底項である。 代入 σ は、σ の定義域の変数をちょうど含むある（したがってすべての）線形項 t について tσ が線形項であるとき、「線形」代入と呼ばれる。すなわち vars(t) = dom(σ) である場合である。 代入 σ は、すべての変数 x について xσ が変数であるとき、「平坦」代入と呼ばれる。 代入 σ は、それがすべての変数の集合上の置換であるとき、「改名」代入と呼ばれる。あらゆる置換と同様に、改名代入 σ は常に「逆」代入 σ⁻¹ を持ち、すべての項 t について tσσ⁻¹ = t = tσ⁻¹σ が成り立つ。しかし、任意の代入について逆を定義することは可能ではない。

例えば、テンプレート:Mset は基底代入であり、テンプレート:Mset は非基底かつ非平坦だが線形であり、 テンプレート:Mset は非線形かつ非平坦であり、テンプレート:Mset は平坦だが非線形であり、テンプレート:Mset は線形かつ平坦だが改名ではない。なぜなら、これは y と y₂ の両方を y₂ に写すからである。これらの代入はいずれも集合 テンプレート:Mset をその定義域として持つ。改名代入の例は テンプレート:Mset であり、これは逆 テンプレート:Mset を持つ。平坦代入 テンプレート:Mset は逆を持つことができない。なぜなら、例えば (x+y) テンプレート:Mset = z+z であり、後者の項は x+y に戻すことができないからである。これは、それぞれの z がどこから由来したかについての情報が失われているためである。基底代入 テンプレート:Mset も、たとえ定数を変数で置き換えることをある種の架空の「一般化された代入」によって許すとしても、例えば (x+2) テンプレート:Mset = 2+2 における由来情報の同様の喪失のために、逆を持つことができない。

2つの代入は、それらがそれぞれの変数を統語論的に等しい結果の項に写すとき、「等しい」とみなされる。形式的には、すべての変数 x ∈ V について xσ = xτ であるとき σ = τ である。 2つの代入 σ = テンプレート:Mset と τ = テンプレート:Mset の「合成」は、代入 テンプレート:Mset から、y_i ∈ テンプレート:Mset であるような対 y_i ↦ u_i を取り除くことによって得られる。 σ と τ の合成は στ と表される。合成は結合的な演算であり、代入の適用と両立する。すなわち、あらゆる代入 ρ、σ、τ、およびあらゆる項 t について、それぞれ (ρσ)τ = ρ(στ)、および (tσ)τ = t(στ) が成り立つ。 すべての変数をそれ自身に写す「恒等代入」は、代入の合成の単位元である。代入 σ は、σσ = σ であるとき、したがってすべての項 t について tσσ = tσ であるとき、「べき等」と呼ばれる。すべての i について x_i≠t_i であるとき、代入 テンプレート:Mset がべき等であるのは、変数 x_i のいずれもいかなる t_j にも出現しない場合、かつその場合に限る。代入の合成は可換ではない。すなわち、σ と τ がべき等であっても、στ は τσ と異なりうるテンプレート:Rpテンプレート:Rp。

例えば、テンプレート:Mset は テンプレート:Mset に等しいが、テンプレート:Mset とは異なる。代入 テンプレート:Mset はべき等である。例えば ((x+y) テンプレート:Mset) テンプレート:Mset = ((y+y)+y) テンプレート:Mset = (y+y)+y である。一方、代入 テンプレート:Mset は非べき等である。例えば ((x+y) テンプレート:Mset) テンプレート:Mset = ((x+y)+y) テンプレート:Mset = ((x+y)+y)+y である。可換でない代入の例は テンプレート:Mset テンプレート:Mset = テンプレート:Mset であるが、テンプレート:Mset テンプレート:Mset = テンプレート:Mset である。

数学

数学において、代入には2つの一般的な用法がある。すなわち、定数に対する変数の「代入」（その変数への割り当てとも呼ばれる）と、等しさの「代入性質」（ライプニッツの法則とも呼ばれる）である。

数学を形式言語とみなすと、変数とは、可能な値の範囲を表すアルファベットからの記号であり、通常は x、y、z のような文字である。ある変数が、与えられた表現あるいは論理式において自由であるならば、それはその範囲内の任意の値で置き換えることができる。ある種の束縛変数も代入することができる。例えば、（多項式の係数のような）表現のパラメータや、関数の引数である。さらに、全称量化されている変数は、その範囲内の任意の値で置き換えることができ、その結果は真の命題となる（これは普遍例化と呼ばれる）。

形式化されていない言語、すなわち数理論理学の外にあるほとんどの数学的文章では、個々の表現についてどの変数が自由でどれが束縛されているかを常に特定できるとは限らない。例えば、${\sum }_{i<k}{a}_{ik}$ において、文脈によっては変数 $i$ が自由で $k$ が束縛されている場合もあれば、その逆の場合もあるが、両方が自由であることはできない。どちらの値が自由であるとみなされるかは、文脈と意味論に依存する。

「等しさの代入性質」あるいは「ライプニッツの法則」（ただし後者の用語は通常哲学的な文脈のために用いられる）は、一般に、2つのものが等しいならば、一方のいかなる性質も他方の性質でなければならない、ということを述べる。これは、次のように論理記法で形式的に述べることができる。$$(a=b)⟹[\varphi (a)\Rightarrow \varphi (b)]$$ここで、任意の $a$ と $b$、および（自由変数 x を持つ）任意の整式 $\varphi (x)$ についてである。例えば、すべての実数 a と b について、もし a = b ならば、a ≥ 0 は b ≥ 0 を含意する（ここで、$\varphi (x)$ は x ≥ 0 である）。これは代数学、特に連立方程式を解く際に最もよく用いられる性質であるが、等しさを用いるほぼすべての数学の分野で応用される。これは、等しさの反射的性質と合わせて、一階論理における等号の公理を形成する。

代入は関数合成と関連しているが同一ではなく、ラムダ計算における β-簡約と密接に関連している。しかし、これらの概念とは対照的に、代数学における力点は、代入演算による代数的構造の保存、すなわち代入が問題となっている構造（多項式の場合は環構造）についての準同型を与えるという事実にある。

代数学

代入は代数学、特に計算機代数における基本的な演算である。

代入のよくある例には多項式が関わり、1変数多項式の不定元に対して数値（あるいは他の表現）を代入することは、その値における多項式の評価に相当する。実際、この演算は非常に頻繁に生じるため、多項式の記法はしばしばそれに合わせて調整される。他の数学的対象について行うように、多項式を P のような名前で表す代わりに、

$P(X)=X^5-3X^2+5X-17$

と定義することで、X への代入を「P(X)」内部での置き換えによって表すことができる。例えば

$P(2)=13$

あるいは

$P(X+1)=X^5+5X^4+10X^3+7X^2+4X-14.$

のようにである。代入は、記号から構成される他の種類の形式的対象、例えば自由群の元にも適用できる。代入が定義されるためには、不定元を特定の値へ写す一意的な準同型の存在を主張する適切な普遍性を持つ代数的構造が必要である。代入とは、そのような準同型のもとでのある元の像を見出すことに相当する。

ZFCにおける代入の証明

以下は、ガイシ・タケウチとウィルソン・M・ザーリングによる『Introduction to Axiomatic Set Theory』(1982)に基づく、（等号を持たない一階論理として定義された）ZFCにおける等しさの代入性質の証明である。 テンプレート:Math theorem

ZFCにおける論理式の定義については、ツェルメロ=フレンケル集合論 § 形式言語を参照。この定義は再帰的であるため、帰納法による証明が用いられる。等号を持たない一階論理におけるZFCでは、「集合の等しさ」は、2つの集合が同じ元を持つこと、記号的には「すべての z について、z が x に属することと z が y に属することは同値である」ということを意味するものとして定義される。すると、外延性の公理は、2つの集合が同じ元を持つならば、それらは同じ集合に属することを主張する。

関連項目

• 置換積分
• テンプレート:Section link
• 文字列の内挿
• 等しさの代入性質
• 三角関数による置換積分
• 普遍例化
• 主方程式形式

出典

• Crabbé, M. (2004). On the Notion of Substitution. Logic Journal of the IGPL, 12, 111–124.
• Curry, H. B. (1952) On the definition of substitution, replacement and allied notions in an abstract formal system. Revue philosophique de Louvain 50, 251–269.
• Kleene, S. C. (1967). Mathematical Logic. Reprinted 2002, Dover. テンプレート:ISBN
• Robinson, Alan J. A.; Voronkov, Andrei (2001-06-22). Handbook of Automated Reasoning. Elsevier. テンプレート:ISBN

外部リンク

• テンプレート:Nlab