代入 (論理学)

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

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

命題論理定義 ψ と φ が命題論理の論理式を表すとき、ψ が φ の「代入事例」であるとは、φ 中の命題変数に論理式を代入し、同一の変数の出現をすべて同一の論理式の出現で置き換えることによって ψ が得られる場合、かつその場合に限る（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) で置き換えることによって得られるからである。

命題論理のための一部の演繹体系では、ある導出の一行が導出の以前の行の代入事例であれば、新たな表現（命題）をその行に記入することができるHunter, G. (1996), p.118.。これは、一部の公理系において新しい行が導入される仕方である。変形規則を用いる体系では、規則がある導出に特定の変数を導入する目的で「代入事例」の使用を含むことがある。

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

一階論理

一階論理において、「代入」とは、変数から項への全域写像である。多くの著者は（ただしすべての著者ではない）、有限個を除くすべての変数 x について σ(x) = x であることをさらに要求する。記法一部の著者は、この代入を表すのに [ t1/x1, …, tk/xk ] を用いる。例えば , ここでは p. 682 を参照。は、それぞれの変数 xi（i=1,…,k）を対応する項 ti に写し、それ以外のすべての変数はそれ自身に写す代入を指す。xi は互いに相異なっていなければならない。多くの著者はさらに、同じ代入に対する無限に多くの異なる記法を避けるため、それぞれの項 ti が統語論的に xi と異なることを要求する。項 t にその代入を「適用する」ことは、後置記法で t と書かれる。これは、t 中のそれぞれの xi のすべての出現を（同時に）ti によって置き換えることを意味する項代数の観点からは、項の集合 T は変数の集合 V 上の自由項代数であり、したがって代入写像 σ: V → T のそれぞれについて、V ⊆ T 上で σ と一致する一意の準同型 : T → T が存在する。上記で定義された、項 t への σ の適用は、その後、関数を引数 t に適用することとみなされる。。項 t に代入 σ を適用した結果 tσ は、その項 t の「事例」と呼ばれる。例えば、代入を項

|| f( | style="text-align: center;" |z ||, a, g( || x || ), y) || に適用すると |- || f( || h(a,y) ||, a, g( || z || ), y) || が得られる。

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

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

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

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

数学数学において、代入には2つの一般的な用法がある。すなわち、定数に対する変数の「代入」（その変数への割り当てとも呼ばれる）と、等しさの「代入性質」（ライプニッツの法則とも呼ばれる）であるDeutsch, Harry and Pawel Garbacz, "Relative Identity", The Stanford Encyclopedia of Philosophy (Fall 2024 Edition), Edward N. Zalta & Uri Nodelman (eds.), forthcoming URL: https://plato.stanford.edu/entries/identity-relative/#StanAccoIden。

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

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

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

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

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

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

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

あるいは

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

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

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

代入 (論理学)

Źródło i licencja