置換（ロジック）

置換は、形式的な表現における構文変換です。表現に置換を適用するということは、その変数またはプレースホルダーのシンボルを一貫して他の表現に置き換えることを意味します。

結果として得られる式は、元の式の置換インスタンス、または 略して インスタンスと呼ばれます。

ψとφ が命題論理の式を表す場合、ψ がφの置換インスタンスとなるのは、φ内の命題変数を式で置換し、同じ変数が出現するたびに同じ式で置き換えることによってψをφから取得できる場合のみです。例:

(R → S) と (T → S)

は次の置換インスタンスです:

P&Q について

そして

(A ↔ A) ↔ (A ↔ A)

は次の置換インスタンスです:

（A↔A）

命題論理の演繹システムの中には、導出の前の行の置換インスタンスである場合に、新しい式（命題）を導出の行に入力できるものがある。 ^{[1] [検証失敗]これは、いくつかの}公理システムで新しい行が導入される方法である。変換規則を使用するシステムでは、規則に、導出に特定の変数を導入する目的で 置換インスタンスの使用が含まれることがある。

命題式は、述語記号のあらゆる評価（または解釈）において真である場合にトートロジーです。 Φ がトートロジーであり、Θ が Φ の置換インスタンスである場合、Θ もトートロジーです。 この事実は、前のセクションで説明した演繹規則の健全性を意味します。

一階述語論理では、置換は変数から項への完全な写像 σ : V → Tである。多くの^{[2] : 73  [3] : 445}だが、すべてではない^{[4] : 250}著者はさらに、有限個を除くすべての変数xに対してσ ( x ) = x を要求する。表記 { x ₁  ↦  t ₁ , …, x _k  ↦  t _k } ^{[note 1]は、各変数}x _iを対応する項t _i （ i =1,…, k ）に、他のすべての変数をそれ自身に 写像する置換を指す。 x _{i は、}ペアごとに異なる必要がある。ほとんどの著者はさらに、同じ置換に対して無限に多くの異なる表記法が存在するのを避けるために、各項t _{i が}x _iと構文的に異なることを要求している。その置換を項tに適用することは、接尾辞表記でt { x ₁  ↦  t ₁ , …, x _k  ↦  t _k }と記述される。これは、 t内の各x _iの出現すべてをt _iで（同時に）置き換えることを意味します。^{[注 2]}項tに置換σ を適用した結果tσは、その項tのインスタンスと呼ばれます。たとえば、項 t に置換 { x  ↦  z , z  ↦  h ( a , y ) } を 適用すると、

置換σのドメインdom ( σ )は、実際に置き換えられる変数の集合として一般的に定義されます。つまり、dom ( σ ) = { x ∈ V | xσ ≠ x }。置換は、そのドメインのすべての変数をグラウンド、つまり変数のない項にマップする場合、グラウンド置換と呼ばれます。グラウンド置換の置換インスタンスtσは、 tのすべての変数がσのドメインにある場合、つまりvars ( t ) ⊆ dom ( σ ) の場合、グラウンド項です。置換 σ は、 tσ が、σ のドメインの変数を正確に含むいくつかの (したがってすべての) 線形項 t の線形項である場合、つまり vars ( t ) = dom ( σ )である場合、線形置換と呼ばれます。置換σは、 xσがすべての変数xの変数である場合、フラット置換と呼ばれます。置換σ は、すべての変数の集合上の順列である場合、名前変更置換と呼ばれます。すべての順列と同様に、名前変更置換 σ には常に逆置換σ ⁻¹があり、すべての項tに対してtσσ ⁻¹ = t = tσ ⁻¹ σ が成り立ちます。ただし、任意の置換の逆を定義することはできません。

たとえば、 { x  ↦ 2, y  ↦ 3+4 } は基底置換、 { x  ↦  x ₁ , y  ↦  y ₂ +4 } は基底でも平坦でもないが線形、 { x  ↦  y ₂ , y  ↦  y ₂ +4 } は非線形で平坦でもない、 { x  ↦  y ₂ , y  ↦  y ₂ } は平坦だが非線形、 { x  ↦  x ₁ , y  ↦  y _{2 } は線形かつ平坦だが、} yとy _{2の両方を}y ₂にマッピングするため、名前変更ではない、ということになります。これらの置換はそれぞれ、集合 { x , y } を定義域として持ちます。名前変更置換の例は { x  ↦  x ₁、x ₁  ↦  y、y  ↦  y ₂、y ₂  ↦  x } で、その逆は { x  ↦  y ₂、y ₂  ↦  y、y  ↦  x ₁、x ₁  ↦  x } です。フラット置換 { x  ↦  z、y  ↦  z } は逆を持つことができません。たとえば、 ( x + y ) { x  ↦  z、y  ↦  z } = z + zであるためです。また、後者の項は、 zの由来に関する情報が失われるため、 x + yに戻すことはできません。基底置換 { x  ↦ 2 } は、定数を変数に置き換えることが架空の種類の「一般化置換」によって許可されているとしても、たとえば ( x +2) { x  ↦ 2 } = 2+2 のように、同様の起源情報の損失により逆置換を持つことはできません。

2 つの置換は、各変数を構文的に等しい結果項にマッピングする場合に等しいとみなされます。正式には、各変数x ∈ Vについてxσ = xτ である場合、σ = τ です。2つの置換σ = { x ₁  ↦  t ₁、…、x _k  ↦  t _k } とτ = { y ₁  ↦  u ₁、…、y _l  ↦ u _l } の合成は、置換 { x ₁  ↦  t ₁ τ、…、x _k  ↦  t _k τ、 y ₁  ↦  u ₁、…、y _l  ↦  u _l } から、 y _i ∈ { x ₁、…、x _k }となるy _i  ↦  u _iのペアを除去すれば得られます。σとτの合成はστで表されます。合成は結合演算であり、置換の適用と互換性があります。つまり、すべての置換ρ、σ、 τ 、およびすべての項tに対して、それぞれ ( ρσ ) τ = ρ ( στ )、および( tσ ) τ = t ( στ ) です。すべての変数をそれ自身にマップする恒等置換は、置換合成の中立要素です。置換σ は、 σσ = σの場合、つまりすべての項tに対してtσσ = tσの場合、べき等と呼ばれます。すべてのiに対してx _i ≠ t _iの場合、置換 { x ₁  ↦  t ₁、…、x _k  ↦  t _k } は、変数のいずれもx _{i は}どのt _jにも現れる。置換合成は可換ではない。つまり、σとτが冪等であっても、στ はτσと異なる可能性がある。^{[2] : 73–74  [3] : 445–446}

たとえば、{ x  ↦ 2, y ↦ 3+4 } は { y  ↦ 3+4, x ↦ 2 } と等しいです が、{ x  ↦ 2, y  ↦ 7 } とは異なります。置換 { x  ↦  y + y } はべき等です。たとえば、 (( x + y ) { x ↦ y + y }) { x ↦ y + y } = (( y + y )+ y ) { x ↦ y + y } = ( y + y )+ yです。一方、置換 { x  ↦  x + y } はべき等ではありません。たとえば、 (( x + y ) { x ↦ x + y }) { x ↦ x + y } = (( x + y )+ y ) { x ↦ x + y } = (( x + y )+ y )+ y です。非可換置換の例としては、{ x  ↦  y } { y  ↦  z } = { x  ↦  z , y  ↦  z } ですが、{ y  ↦  z } { x  ↦  y } = { x  ↦  y , y  ↦  z } となります。

数学において、置換の一般的な用途は2つあります。定数を変数に置き換えること（その変数への代入とも呼ばれる）と、等式の置換特性（^[5]ライプニッツの法則とも呼ばれる）です。^[6]

数学を形式言語として考えると、変数はアルファベットの記号であり、通常はx、y、zなどの文字で、可能な値の範囲を示します。^[7]変数が特定の式または公式内で自由である場合、その範囲内の任意の値に置き換えることができます。^[8]特定の種類の束縛変数も置き換えることができます。たとえば、式のパラメーター（多項式の係数など）や関数の引数です。さらに、普遍的に量化されている変数は、その範囲内の任意の値に置き換えることができ、結果は真のステートメントになります。（これを普遍的インスタンス化と呼びます）

非形式化言語、つまり数理論理学以外のほとんどの数学テキストでは、個々の式について、どの変数が自由で束縛されているかを常に識別できるわけではありません。たとえば、では、コンテキストに応じて、変数は 自由かつ束縛されている場合もあれば、その逆の場合もありますが、両方が自由であることはできません。どの値が自由であると想定されるかは、コンテキストと意味に依存します。 ${\textstyle \sum _{i<k}a_{ik}}$${\textstyle i}$${\textstyle k}$

等式の置換特性、またはライプニッツの法則（後者の用語は通常哲学的な文脈でのみ使用される）は、一般に、2 つのものが等しい場合、一方の性質はいずれも他方の性質でなければならないと述べています。これは、論理表記法で正式には次のように記述できます。すべてのおよび、および任意の整形式の式（自由変数 x を含む）について。たとえば、すべての実数aとbについて、a = bの場合、a ≥ 0であればb ≥ 0を意味します（ここで、はx ≥ 0です）。これは、代数、特に連立方程式を解くときに最もよく使用される特性ですが、等式を使用する数学のほぼすべての分野で適用されています。これは、等式の反射特性とともに、一階述語論理における等式の公理を形成します。 ^[9]$${\displaystyle (a=b)\implies {\bigl [}\phi (a)\Rightarrow \phi (b){\bigr ]}}$$${\textstyle a}$${\textstyle b}$ ${\textstyle \phi (x)}$ ${\displaystyle \phi (x)}$

置換は関数合成と関連しているが、同一ではない。ラムダ計算におけるβ還元と密接に関連している。しかし、これらの概念とは対照的に、代数学では置換操作による代数構造の保存、つまり置換によって手元の構造の準同型性(多項式の場合は環構造) が得られるという事実に重点が置かれている。^{[引用が必要]}

代数、特にコンピュータ代数における基本的な演算は置換である。^{[10] [11]}

置換の一般的な例としては多項式が挙げられます。多項式では、一変数多項式の不定値を数値（または別の式）で置換すると、その値で多項式を評価することになります。実際、この操作は頻繁に行われるため、多項式の表記法はこれに合わせて変更されることがよくあります。他の数学的対象の場合のように多項式をPのような名前で指定する代わりに、次のように定義できます。

${\displaystyle P(X)=X^{5}-3X^{2}+5X-17}$

つまり、Xの置換は「 P ( X )」内の置換によって指定できる。

${\displaystyle P(2)=13}$

または

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

置換は、自由群の要素など、記号から構築された他の種類の形式オブジェクトにも適用できます。置換を定義するには、適切な普遍的性質を持つ代数構造が必要であり、これは不定値を特定の値に変換する一意の準同型の存在を主張します。置換は、そのような準同型の下での要素の像を見つけることに相当します。

• 置換による積分
• ラムダ計算 § 置換
• 文字列補間
• 等式の置換特性
• 三角関数の置換
• ユニバーサルインスタンス化

• Crabbé, M. (2004). 「置換の概念について」 Logic Journal of the IGPL, 12, 111–124.
• カリー、HB （1952）抽象形式システムにおける代用、置き換えおよび関連概念の定義についてルーヴァン哲学評論50、251-269。
• ハンター、G. (1971)。メタロジック：標準一階述語論理のメタ理論入門。カリフォルニア大学出版局。ISBN 0-520-01822-2 
• クリーネ、SC (1967)。数学論理学。2002年再版、ドーバー。ISBN 0-486-42533-9 

• nラボでの代替